Finite-Trace and Generalized-Reactivity Specifications in Temporal Synthesis
Giuseppe De Giacomo, Antonio Di Stasio, Lucas M. Tabajara, Moshe Vardi, Shufang Zhu
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.
BibTeX
@inproceedings{ijcai2021p255,
title = {Finite-Trace and Generalized-Reactivity Specifications in Temporal Synthesis},
author = {De Giacomo, Giuseppe and Di Stasio, Antonio and M. Tabajara, Lucas 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 = {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},
}