City Research Online

Abstract

In this communication we present recent advances in the field of synthesis for agent goals specified in Linear Temporal Logic on finite traces under environment specifications. In synthesis, environment specifications are constraints on the environments that rule out certain environment behavior. To solve synthesis of LTLf goals under environment specifications, we could reduce the problem to LTL synthesis. Unfortunately, while synthesis in LTLf and in LTL have the same worst-case complexity (both are 2EXPTIME-complete), the algorithms available for LTL synthesis are much harder in practice than those for LTLf synthesis. We report recent results showing that when the environment specifications are in form of fairness, stability, or GR(1) formulas, we can avoid such a detour to LTL and keep the simplicity of LTLf synthesis. Furthermore, even when the environment specifications are specified in full LTL we can partially avoid this detour.

Publication Type:	Conference or Workshop Item (Paper)
Additional Information:	© 2022 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
Publisher Keywords:	Linear Temporal Logic on Finite Traces, Synthesis, Automata-Theoretic Approach
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