Formal Verification for Trustworthy Human-Robot Collaboration

27^th May 2025, 13:00 Ashton Lecture Theatre
Pian Yu
University College London

Abstract

Robotic systems are inherently complex, integrating heterogeneous components and operating in dynamic environments — posing unique challenges for safety assurance. In this talk, I explore how formal methods can address these challenges to support the design of trustworthy human-robot collaborative systems. Key topics include formal modelling of human-robot interactions and uncertainty sources, formal specification of desired robot behaviours and constraints, and formal verification/synthesis techniques to enhance system safety and trustworthiness.

In collaborative human-robot scenarios, we model trust-based human-robot interaction using a partially observable Markov decision process (POMDP). Within this framework, data-driven techniques are employed to model human internal states and adaptive conformal prediction, a statistical machine learning method, is utilised to quantify uncertainty. For scenarios where human intention cannot be directly quantified, we propose Markov Decision Processes with Set-Valued Transitions (MDPSTs) as the modelling framework to capture unpredictable human intentions. In both settings, we reason about actions and planning for temporally extended goals expressed in Linear Temporal Logic (LTL) or Linear Distribution Temporal Logic (LDTL). We present novel algorithms for optimal policy synthesis and validate our approach through various case studies, which demonstrate promising results.

Biography

Pian Yu is a Lecturer (Assistant Professor) in Robotics & AI at Department of Computer Science, University College London (UCL). Prior to this position, she was a Postdoctoral Researcher at Department of Computer Science, University of Oxford supervised by Prof. Marta Kwiatkowska (August 2022 to October 2024) and a Postdoctoral Researcher at KTH Royal Institute of Technology, supervised by Prof. Dimos V. Dimarogonas (April 2021 to July 2022). She received her PhD in Electrical Engineering from KTH Royal Institute of Technology in Feb. 2021. She was a Student Best Paper Award finalist at the 2020 American Control Conference in Denver. She was selected as a Future Digileader by Digital Futures, Sweden in 2023 and a DAAD AInet fellow, Germany in 2023.