BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//University of Liverpool Computer Science Seminar System//v2//EN
BEGIN:VEVENT
DTSTAMP:20260922T121712Z
UID:Seminar-dept-1273@lxserverM.csc.liv.ac.uk
ORGANIZER:CN=Lutz Oettershagen:MAILTO:Lutz.Oettershagen@liverpool.ac.uk
DTSTART:20250527T130000
DTEND:20250527T140000
SUMMARY:School Seminar Series
DESCRIPTION:Pian Yu: Formal Verification for Trustworthy Human-Robot Collaboration\n\nRobotic 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. \n\n\n\nIn 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.\n\n\n\nhttps://www.csc.liv.ac.uk/research/seminars/abstract.php?id=1273
LOCATION:Ashton Lecture Theatre
END:VEVENT
END:VCALENDAR