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