Synthesizing Good-Enough Strategies for LTLf Specifications
Synthesizing Good-Enough Strategies for LTLf Specifications
Yong Li, Andrea Turrini, Moshe Y. Vardi, Lijun Zhang
Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence
Main Track. Pages 4144-4151.
https://doi.org/10.24963/ijcai.2021/570
We consider the problem of synthesizing good-enough (GE)-strategies for linear temporal logic (LTL) over finite traces or LTLf for short.
The problem of synthesizing GE-strategies for an LTL formula φ over infinite traces reduces to the problem of synthesizing winning strategies for the formula (∃Oφ)⇒φ where O is the set of propositions controlled by the system.
We first prove that this reduction does not work for LTLf formulas.
Then we show how to synthesize GE-strategies for LTLf formulas via the Good-Enough (GE)-synthesis of LTL formulas.
Unfortunately, this requires to construct deterministic parity automata on infinite words, which is computationally expensive.
We then show how to synthesize GE-strategies for LTLf formulas by a reduction to solving games played on deterministic Büchi automata, based on an easier construction of deterministic automata on finite words.
We show empirically that our specialized synthesis algorithm for GE-strategies outperforms the algorithms going through GE-synthesis of LTL formulas by orders of magnitude.
Keywords:
Planning and Scheduling: Applications of Planning
Planning and Scheduling: Planning and Scheduling
Planning and Scheduling: Temporal and Hybrid Planning