Assume-Guarantee Synthesis for Prompt Linear Temporal Logic

Nathanaël Fijalkow; Bastien Maubert; Aniello Murano; Moshe Vardi

IJCAI 2020poster0 citations

Assume-Guarantee Synthesis for Prompt Linear Temporal Logic

Nathanaël Fijalkow, Bastien Maubert, Aniello Murano, Moshe Vardi

Abstract

Prompt-LTL extends Linear Temporal Logic with a bounded version of the ``eventually'' operator to express temporal requirements such as bounding waiting times. We study assume-guarantee synthesis for prompt-LTL: the goal is to construct a system such that for all environments satisfying a first prompt-LTL formula (the assumption) the system composed with this environment satisfies a second prompt-LTL formula (the guarantee). This problem has been open for a decade. We construct an algorithm for solving it and show that, like classical LTL synthesis, it is 2-EXPTIME-complete.

Agent-based and Multi-agent Systems: Formal Verification, Validation and SynthesisAgent-based and Multi-agent Systems: Algorithmic Game Theory

BibTeX

@inproceedings{ijcai2020p17,
  title     = {Assume-Guarantee Synthesis for Prompt Linear Temporal Logic},
  author    = {Fijalkow, Nathanaël and Maubert, Bastien and Murano, Aniello and Vardi, Moshe},
  booktitle = {Proceedings of the Twenty-Ninth International Joint Conference on
               Artificial Intelligence, {IJCAI-20}},
  publisher = {International Joint Conferences on Artificial Intelligence Organization},
  editor    = {Christian Bessiere},
  pages     = {117--123},
  year      = {2020},
  month     = {7},
  note      = {Main track},
  doi       = {10.24963/ijcai.2020/17},
  url       = {https://doi.org/10.24963/ijcai.2020/17},
}