Emerson-Lei and Manna-Pnueli Games for LTLf+ and PPLTL+ Synthesis

Recently, the Manna-Pnueli Hierarchy has been used to define the temporal logics LTLfp and PPLTLp, which allow to use finite-trace LTLf/PPLTL techniques in infinite-trace settings while achieving the expressiveness of full LTL. In this paper, we present the first actual solvers for reactive synthesis in these logics. These are based on games on graphs that leverage DFA-based techniques from LTLf/PPLTL to construct the game arena. We start with a symbolic solver based on Emerson-Lei games, which reduces lower-class properties (guarantee, safety) to higher ones (recurrence, persistence) before solving the game. We then introduce Manna-Pnueli games, which natively embed Manna-Pnueli objectives into the arena. These games are solved by composing solutions to a DAG of simpler Emerson-Lei games, resulting in a provably more efficient approach. We implemented the solvers and practically evaluated their performance on a range of representative formulas. The results show that Manna-Pnueli games often offer significant advantages, though not universally, indicating that combining both approaches could further enhance practical performance.

Correct-by-Construction Design of Contextual Robotic Missions Using Contracts

Effectively specifying and implementing robotic missions pose a set of challenges to software engineering for robotic systems, since they require formalizing and executing a robot's high-level tasks while considering various application scenarios and conditions, also known as contexts, in real-world operational environments. Writing correct mission specifications that explicitly account for multiple contexts can be a tedious and error-prone task. Moreover, as the number of context, hence the specification, becomes more complex, generating a correct-by-construction implementation, e.g., by using synthesis methods, can become intractable. A viable approach to address these issues is to decompose the mission specification into smaller sub-missions, with each sub-mission corresponding to a specific context. However, such a compositional approach would still pose challenges in ensuring the overall mission correctness. In this paper, we propose a new, compositional framework for the specification and implementation of contextual robotic missions using assume-guarantee contracts. The mission specification is captured in a hierarchical and modular way and each sub-mission is synthesized as a robot controller. We address the problem of dynamically switching between sub-mission controllers while ensuring correctness under certain conditions.

A Computational Framework for Adaptive Systems and its Verification

Modern computer systems are inherently distributed and feature autonomous and collaborative behaviour of multicomponent with global goals. These goals are expressed in terms of the combined behaviour of different components that are usually deployed in dynamic and evolving environments. It is therefore crucial to provide techniques to generate programs for collaborative and adaptive components, with guarantees of maintaining their designated global goals. To reach this endeavour, we need to extend modelling formalisms and specification languages to account for the specific features of these systems and to permit specifying both individual and system behaviour. We propose a computational framework to allow multiple components to interact in different modes, exchange information, adapt their behaviour, and reconfigure their communication interfaces. The framework permits a local interaction based on shared variables and a global one based on message passing. To be able to reason about local and global behaviour, we extend LTL to consider the exchanged messages and their constraints. Finally, we study the computational complexity of satisfiability and verification considering these extensions.