Finite-Trace and Generalized-Reactivity Specifications in Temporal Synthesis
Finite-Trace and Generalized-Reactivity Specifications in Temporal Synthesis
Giuseppe De Giacomo, Antonio Di Stasio, Lucas M. Tabajara, Moshe Vardi, Shufang Zhu
Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence
Main Track. Pages 1852-1858.
https://doi.org/10.24963/ijcai.2021/255
Linear Temporal Logic (LTL) synthesis aims at automatically synthesizing a program that complies with desired properties expressed in LTL. Unfortunately it has been proved to be too difficult computationally to perform full LTL synthesis. There have been two success stories with LTL synthesis, both having to do with the form of the specification. The first is the GR(1) approach: use safety conditions to determine the possible transitions in a game between the environment and the agent, plus one powerful notion of fairness, Generalized Reactivity(1), or GR(1). The second, inspired by AI planning, is focusing on finite-trace temporal synthesis, with LTLf (LTL on finite traces) as the specification language. In this paper we take these two lines of work and bring them together. We first study the case in which we have an LTLf agent goal and a GR(1) assumption. We then add to the framework safety conditions for both the environment and the agent, obtaining a highly expressive yet still scalable form of LTL synthesis.
Keywords:
Knowledge Representation and Reasoning: Action, Change and Causality
Planning and Scheduling: Theoretical Foundations of Planning
Agent-based and Multi-agent Systems: Formal Verification, Validation and Synthesis