Assume-Guarantee Synthesis for Prompt Linear Temporal Logic
Assume-Guarantee Synthesis for Prompt Linear Temporal Logic
Nathanaël Fijalkow, Bastien Maubert, Aniello Murano, Moshe Vardi
Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence
Main track. Pages 117-123.
https://doi.org/10.24963/ijcai.2020/17
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.
Keywords:
Agent-based and Multi-agent Systems: Formal Verification, Validation and Synthesis
Agent-based and Multi-agent Systems: Algorithmic Game Theory