City Research Online

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.

Publication Type:	Conference or Workshop Item (Paper)
Additional Information:	Copyright © 2021 International Joint Conferences on Artificial Intelligence. The final version of this paper has been published in Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence and it's available online at: https://doi.org/10.24963/ijcai.2021/255
Publisher 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
Subjects:	Q Science > QA Mathematics > QA75 Electronic computers. Computer science
Departments:	School of Science & Technology School of Science & Technology > Computer Science
SWORD Depositor:	Symplectic Administrator

Export

Downloads