On-the-fly Synthesis for LTL over Finite Traces
06 May 2021
When: Thursday, May 6, 2021, 12pm (CEST).
Where: Zoom online, check the address in the Google Calendar Event.
Topic: On-the-fly Synthesis for LTL over Finite Traces.
Speaker: Jianwen Li, Youth Research Professor, East
China Normal University, Shanghai.
Abstract
We present a new synthesis framework based on the on-the-fly DFA construction for LTL over finite traces (LTLf ). Extant
approaches rely heavily on the construction of the complete DFA w.r.t. the input LTLf formula, whose size can be doubly
exponential to the size of the formula in the worst case. Under those approaches, the synthesis cannot be conducted
unless the whole DFA is completely constructed, which is not only inefficient but also not scalable in practice. Indeed,
the DFA construction is the main bottleneck of LTLf synthesis in prior work. To mitigate this challenge, we follow two
steps in this paper: Firstly, we present several light-weight preprocessing techniques such that the synthesis result
can be obtained even without DFA construction; Secondly, we propose to achieve the synthesis together with the
on-the-fly DFA construction such that the synthesis result can be obtained before constructing the whole DFA. The
on-the-fly DFA construction is implemented using the SAT-based techniques for automata generation. We compared our new
approach with the traditional ones on extensive LTLf synthesis benchmarks. Experimental results showed that the
preprocessing techniques have a significant advantage on the synthesis performance in terms of scalability, and the
on-the-fly synthesis is able to complement extant approaches on both realizable and unrealizable cases.
Material
Mission Planning for Mobile Robots with Probabilistic Performance Guarantees
29 Apr 2021
When: Thursday, April 29, 2021, 3pm (CEST).
Where: Zoom online, check the address in the Google Calendar Event.
Topic: Mission Planning for Mobile Robots with Probabilistic Performance Guarantees.
Speaker: Bruno Lacerda, Senior Researcher in Robotics, University of Oxford.
Abstract
Robust mission planning algorithms for autonomous robots typically require explicit reasoning and prediction of the
inherent uncertainty of environmental features. For example, service robots need to consider the behaviour of humans
around them; autonomous underwater vehicles require models of underwater currents; and robots in a multi-robot system
need to reason about how interaction with other robots can affect their performance.
In this talk, I will provide an overview of our recent research on the synthesis of robust and intelligent robot
behaviour using a range of techniques from probabilistic planning and formal methods. I will highlight two strands of
work: planning with learnt models and planning for multi-robot coordination. For the former, I will cover our work on
Gaussian process modelling on environmental features and on regret minimisation for uncertain Markov decision processes.
For the latter, I will describe our efforts to model and reason about uncertain action durations in a principled fashion.
Short Bio
Bruno Lacerda received his Ph.D. in Electrical and Computing Engineering from the Instituto Superior Técnico, University
of Lisbon, Portugal, in 2013. Between 2013 and 2017, he was a Research Fellow at the School of Computer Science,
University of Birmingham, UK. Currently, he is a Senior Researcher at the Oxford Robotics Institute, University of
Oxford, UK. His research focuses on the intersection of decision making under uncertainty, formal methods, and mobile
robotics. In particular, he is interested in the use of a combination of techniques from learning, planning and model
checking to synthesise intelligent, robust and verifiable behaviour, for both single and multi-robot systems.
Material
- Video
(Passcode: mA#XG!^3)
Synthesis Problems for Prompt Linear Temporal Logic
11 Mar 2021
When: Thursday, March 11, 2021, 3pm (GMT+1).
Where: Zoom online, check the address in the Google Calendar Event.
Topic: Synthesis Problems for Prompt Linear Temporal Logic.
Speaker: Bastien Maubert, Postdoctoral Fellow at the Università degli Studi di Napoli Federico II
Abstract
In LTL, formula F p ensures that p will eventually be true at some point in the future, but it does not tell us anything
about how far this moment may be. And formula G request -> F granted tells us that every request will eventually be
granted, which is a classic requirement for a correct system (think of a printing server for instance); but the waiting
time between the moment in which a request is made and the moment it is satisfied may grow arbitrarily large and still
the formula would hold. There is no way in LTL to prevent this kind of behaviour. Prompt-LTL extends LTL with an
operator of “bounded eventuality” that serves this purpose. In this talk I will present recent results concerning
synthesis problems for Prompt LTL. In particular I will first focus on the problem of Assume-Guarantee Synthesis for
Prompt-LTL, which remained open for a decade, and that we solved last year. Then I will move to logics for strategic
reasoning, in particular Strategy Logic (SL), whose model-checking problem subsumes a number of synthesis problems.
I will present extensions of SL with operators to bound the waiting time and operators to bound the number of “bad”
executions, and give an idea of how we can model-check this logic. I will also briefly present cost functions and cost
automata, which are a central tool to solve both problems.
Short Bio
Bastien Maubert obtained his PhD in 2014 at Université de Rennes 1. It was prepared in the team LogicA at IRISA,
under the supervision of Sophie Pinchinat and Guillaume Aucher. He has then been a postdoctoral fellow at LORIA in
Nancy, in Hans van Ditmarsch’ team CELLO (Computational Epistemic Logic in Lorraine), working on his ERC project
Epistemic Protocol Synthesis. In 2016 he moved to Università degli Studi di Napoli “Federico II”, in Aniello Murano’s
group, to work on the project LoGIcInMAS (Logics and Games for Imperfect Information in Multi-Agent Systems), for which
he obtained a Marie-Curie Individual Fellowship. He is currently still working in Napoli as a postdoctoral fellow.
His research interests include logics dealing with knowledge and strategic abilities (epistemic, temporal, dynamic,
alternating, strategic logics…), game theory, in particular games with imperfect information, automatic and rational
structures, automata theory, and in general he is interested in problems dealing with the security of systems (program
verification, program synthesis…).
Learning a Symbolic Planning Domain through the Interaction with Continuous Environments
25 Feb 2021
When: Thursday, February 25, 2021, 3pm (GMT+1).
Where: Zoom online, check the address in the Google Calendar Event.
Topic: Learning a Symbolic Planning Domain through the Interaction with Continuous Environments.
Speaker: Elena Umili
Abstract
Learning a Symbolic Planning Domain through the Interaction with Continuous Environments.
Material
Efficient PAC Reinforcement Learning in Regular Decision Processes
18 Feb 2021
When: Thursday, February 18, 2021, 3pm (GMT+1).
Where: Zoom online, check the address in the Google Calendar Event.
Topic: Efficient PAC Reinforcement Learning in Regular Decision Processes.
Speaker: Alessandro Ronca
Abstract
Efficient PAC Reinforcement Learning in Regular Decision Processes.
Material
Understanding RPNs
11 Feb 2021
When: Thursday, February 11, 2021, 3pm (GMT+1).
Where: Zoom online, check the address in the Google Calendar Event.
Topic: Understanding RPNs.
Speaker: Mohamad Hosein Danesh
Abstract
Understanding RPNs.
Material