Supervisor

Suitable for

Abstract

This project focuses on developing an algorithmic solution for solving obligation games as part of reactive synthesis. Obligation properties, a unique class within the safety-progress hierarchy of property specifications [2], play a foundational role in specifying complex system behaviors, particularly when a system interacts with an unpredictable or adversarial environment. Expressed through Linear Temporal Logic (LTL) [1] and its finite variant (LTLf) [3]—the most widely used logical languages in Computer Science and Artificial Intelligence for specifying temporal properties—obligation properties combine safety and guarantee elements to outline conditions for conditional behaviors based on both desired and undesired events.

Safety properties ensure that “nothing bad happens,” requiring specific conditions to hold at every instant of the system's operation. For example, a safety property might dictate that a robot must avoid obstacles continuously. Violations of safety properties are identifiable in finite time, meaning the system or observer can detect and respond to any bad state immediately. Guarantee properties, in contrast, specify that “something good eventually happens.” These properties represent goals that the system should fulfill at least once within a finite timeframe, such as ensuring that a network packet eventually reaches its destination. Together, safety and guarantee properties define comprehensive behavioral expectations for systems operating in dynamic or adversarial settings.

Obligation properties, introduced as part of the safety-progress hierarchy by Lichtenstein, Pnueli, and Zuck (1985) and further developed by Manna and Pnueli [2], represent Boolean combinations of safety and guarantee properties. Reactive synthesis is the problem of automatically synthesizing a system that meets desired dynamical properties in a partially controllable environment. The environment is typically adversarial; however, in case it is stochastic, reactive synthesis becomes MDP solving for temporal specification. This project aims to devise novel synthesis techniques that address obligation properties in either adversarial or stochastic environments.

References:

1. Giuseppe De Giacomo and Moshe Y. Vardi. Linear temporal logic and linear dynamic logic on finite traces. In IJCAI 2013.
2. Zohar Manna and Amir Pnueli. A hierarchy of temporal properties. In PODC 1990.
3. Amir Pnueli. The temporal logic of programs. In FOCS, 1977.