Best-Effort Synthesis: Doing Your Best Is Not Harder than Giving up

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.

Cite

Text

Aminof et al. "Best-Effort Synthesis: Doing Your Best Is Not Harder than Giving up." International Joint Conference on Artificial Intelligence, 2021. doi:10.24963/IJCAI.2021/243

Markdown

[Aminof et al. "Best-Effort Synthesis: Doing Your Best Is Not Harder than Giving up." International Joint Conference on Artificial Intelligence, 2021.](https://mlanthology.org/ijcai/2021/aminof2021ijcai-best/) doi:10.24963/IJCAI.2021/243

BibTeX

@inproceedings{aminof2021ijcai-best,
  title     = {{Best-Effort Synthesis: Doing Your Best Is Not Harder than Giving up}},
  author    = {Aminof, Benjamin and De Giacomo, Giuseppe and Rubin, Sasha},
  booktitle = {International Joint Conference on Artificial Intelligence},
  year      = {2021},
  pages     = {1766-1772},
  doi       = {10.24963/IJCAI.2021/243},
  url       = {https://mlanthology.org/ijcai/2021/aminof2021ijcai-best/}
}