Finite-Trace and Generalized-Reactivity Specifications in Temporal Synthesis

De Giacomo, Giuseppe; Stasio, Antonio Di; Tabajara, Lucas M.; Vardi, Moshe; Zhu, Shufang

doi:10.24963/ijcai.2021/255

Finite-Trace and Generalized-Reactivity Specifications in Temporal Synthesis

Giuseppe De Giacomo, Antonio Di Stasio, Lucas M. Tabajara, Moshe Vardi, Shufang Zhu

Download BibTeX Cite

Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence. Main Track. Pages 1852-1858.

https://doi.org/10.24963/ijcai.2021/255

Keywords

Planning and Scheduling: Theoretical Foundations of Planning
Knowledge Representation and Reasoning: Action, Change and Causality
Agent-based and Multi-agent Systems: Formal Verification, Validation and Synthesis

Abstract

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.

Giuseppe De Giacomo, Antonio Di Stasio, Lucas M. Tabajara, Moshe Vardi, and Shufang Zhu. 2021. Finite-Trace and Generalized-Reactivity Specifications in Temporal Synthesis. In Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence, IJCAI-21. IJCAI, 1852–1858. https://doi.org/10.24963/ijcai.2021/255

@inproceedings{ijcai2021p255,
  title     = {Finite-Trace and Generalized-Reactivity Specifications in Temporal Synthesis},
  author    = {De Giacomo, Giuseppe and Stasio, Antonio Di and Tabajara, Lucas M. and Vardi, Moshe and Zhu, Shufang},
  booktitle = {Proceedings of the Thirtieth International Joint Conference on
               Artificial Intelligence, {IJCAI-21}},
  publisher = {International Joint Conferences on Artificial Intelligence Organization},
  editor    = {Prof. Zhi-Hua Zhou},
  pages     = {1852--1858},
  year      = {2021},
  month     = {8},
  note      = {Main Track},
  doi       = {10.24963/ijcai.2021/255},
  url       = {https://doi.org/10.24963/ijcai.2021/255},
}

TY  - CPAPER
TI  - Finite-Trace and Generalized-Reactivity Specifications in Temporal Synthesis
AU  - De Giacomo, Giuseppe
AU  - Stasio, Antonio Di
AU  - Tabajara, Lucas M.
AU  - Vardi, Moshe
AU  - Zhu, Shufang
T2  - Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence, IJCAI-21
PB  - International Joint Conferences on Artificial Intelligence Organization
PY  - 2021
SP  - 1852
EP  - 1858
DO  - 10.24963/ijcai.2021/255
UR  - https://doi.org/10.24963/ijcai.2021/255
ER  -