Best-Effort Synthesis: Doing Your Best Is Not Harder Than Giving Up

Benjamin Aminof; Giuseppe De Giacomo; Sasha Rubin

IJCAI 2021poster31 citations

Best-Effort Synthesis: Doing Your Best Is Not Harder Than Giving Up

Benjamin Aminof, Giuseppe De Giacomo, Sasha Rubin

Abstract

We study best-effort synthesis under environment assumptions specified in LTL, and show that this problem has exactly the same computational complexity of standard LTL synthesis: 2EXPTIME-complete. We provide optimal algorithms for computing best-effort strategies, both in the case of LTL over infinite traces and LTL over finite traces (i.e., LTLf). The latter are particularly well suited for implementation.

Knowledge Representation and Reasoning: Action, Change and CausalityPlanning and Scheduling: Theoretical Foundations of PlanningAgent-based and Multi-agent Systems: Formal Verification, Validation and Synthesis

BibTeX

@inproceedings{ijcai2021p243,
  title     = {Best-Effort Synthesis: Doing Your Best Is Not Harder Than Giving Up},
  author    = {Aminof, Benjamin and De Giacomo, Giuseppe and Rubin, Sasha},
  booktitle = {Proceedings of the Thirtieth International Joint Conference on
               Artificial Intelligence, {IJCAI-21}},
  publisher = {International Joint Conferences on Artificial Intelligence Organization},
  editor    = {Zhi-Hua Zhou},
  pages     = {1766--1772},
  year      = {2021},
  month     = {8},
  note      = {Main Track},
  doi       = {10.24963/ijcai.2021/243},
  url       = {https://doi.org/10.24963/ijcai.2021/243},
}