Synthesizing Good-Enough Strategies for LTLf Specifications

Li, Yong; Turrini, Andrea; Vardi, Moshe Y.; Zhang, Lijun

doi:10.24963/ijcai.2021/570

Synthesizing Good-Enough Strategies for LTLf Specifications

Yong Li, Andrea Turrini, Moshe Y. Vardi, Lijun Zhang

Download BibTeX Cite

Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence. Main Track. Pages 4144-4151.

https://doi.org/10.24963/ijcai.2021/570

Keywords

Planning and Scheduling: Applications of Planning
Planning and Scheduling: Temporal and Hybrid Planning
Planning and Scheduling: Planning and Scheduling

Abstract

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.

Yong Li, Andrea Turrini, Moshe Y. Vardi, and Lijun Zhang. 2021. Synthesizing Good-Enough Strategies for LTLf Specifications. In Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence, IJCAI-21. IJCAI, 4144–4151. https://doi.org/10.24963/ijcai.2021/570

@inproceedings{ijcai2021p570,
  title     = {Synthesizing Good-Enough Strategies for LTLf Specifications},
  author    = {Li, Yong and Turrini, Andrea and Vardi, Moshe Y. and Zhang, Lijun},
  booktitle = {Proceedings of the Thirtieth International Joint Conference on
               Artificial Intelligence, {IJCAI-21}},
  publisher = {International Joint Conferences on Artificial Intelligence Organization},
  editor    = {Prof. Zhi-Hua Zhou},
  pages     = {4144--4151},
  year      = {2021},
  month     = {8},
  note      = {Main Track},
  doi       = {10.24963/ijcai.2021/570},
  url       = {https://doi.org/10.24963/ijcai.2021/570},
}

TY  - CPAPER
TI  - Synthesizing Good-Enough Strategies for LTLf Specifications
AU  - Li, Yong
AU  - Turrini, Andrea
AU  - Vardi, Moshe Y.
AU  - Zhang, Lijun
T2  - Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence, IJCAI-21
PB  - International Joint Conferences on Artificial Intelligence Organization
PY  - 2021
SP  - 4144
EP  - 4151
DO  - 10.24963/ijcai.2021/570
UR  - https://doi.org/10.24963/ijcai.2021/570
ER  -