Supervisor

Suitable for

Abstract

Reactive synthesis, a branch of Formal Methods (FM), seeks to automatically construct systems that meet specified dynamic properties. The basic techniques for reactive synthesis share several similarities with Model Checking, another core FM problem, leveraging connections between Logics, Automata, and Games [6]. The most used specification language used in Computer Science and Artificial Intelligence is Linear Temporal Logic (LTL) [4].

 

Model Checking stands as a major success in FM, employed by companies like Intel and NASA on a daily basis. In contrast, reactive synthesis has not achieved comparable adoption, largely due to scalability challenges. In particular Reactive Synthesis for LTL involves: (1) having a specification φ of the desired system behaviour in LTL, in which one distinguishes controllable and uncontrollable variables; (2) extracting from the specification an equivalent automaton on infinite words, corresponding to the infinite traces satisfying φ; (3) (differently from Model Checking) determinizing the automaton to obtain an arena for a game between the system and the environment; (4) solving the game, by fixpoint computation, for an objective determined by the automaton’s accepting condition yielding a strategy for the system that fulfils the original specification φ. However, despite this, Step (3) remains a major performance obstacle. For LTL, this involves determinizing nondeterministic Buchi automata, which is notoriously difficult. This has held back the use of reactive synthesis in applications.

 

Recently, the AI community has shifted attention toward LTL on finite traces (LTLf) [1], which is better suited for typical Planning and AI scenarios where goals are specified over finite traces. In this setting, the agent receives a goal, “thinks” about how to achieve it, synthesizes a plan, executes the plan, and repeats. The advantage of focusing on finite traces is that in Step (3) one can rely on (classic) automata operating on finite traces, including deterministic finite automata (DFA), and use known determinization algorithms with good practical performance.

 

A recent breakthrough demonstrates that DFA-based techniques foundational to LTLf synthesis can be extended to LTL [1]. By leveraging the Pnueli-Manna hierarchy [2], which classifies properties into six categories (safety, guarantee, obligation, recurrence, persistence, and general reactivity), an extension of LTLf has been proposed that enables the expression of arbitrary LTL properties over infinite traces [1].

 

This project aims to solving reactive synthesis for LTL that builds upon these recent advancements by exploiting Emerson-Lei automata for adversarial environments, and Limit Deterministic Buchi Automata and Good for MDP Automata for Stochastic settings (MDPs).

References:

1. Benjamin Aminof, Giuseppe De Giacomo, Sasha Rubin, Moshe Y. Vardi. LTLf+ and PPLTL+: Extending LTLf and PPLTL to Infinite Traces. arXiv:2411.09366, 2024.
2. Giuseppe De Giacomo and Moshe Y. Vardi. Linear temporal logic and linear dynamic logic on finite traces. In IJCAI 2013.
3. Zohar Manna and Amir Pnueli. A hierarchy of temporal properties. In PODC 1990.
4. Amir Pnueli. The temporal logic of programs. In FOCS, 1977.
5. Daniel Hausmann, Mathieu Lehaut, Nir Piterman: Symbolic Solution of Emerson-Lei Games for Reactive Synthesis. In FoSSaCS 2024.
6. Fijalkow et al. Games on Graphs. Book, https://arxiv.org/abs/2305.10546