Assume-Guarantee Synthesis for Prompt Linear Temporal Logic
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.
Cite
Text
Fijalkow et al. "Assume-Guarantee Synthesis for Prompt Linear Temporal Logic." International Joint Conference on Artificial Intelligence, 2020. doi:10.24963/IJCAI.2020/17Markdown
[Fijalkow et al. "Assume-Guarantee Synthesis for Prompt Linear Temporal Logic." International Joint Conference on Artificial Intelligence, 2020.](https://mlanthology.org/ijcai/2020/fijalkow2020ijcai-assume/) doi:10.24963/IJCAI.2020/17BibTeX
@inproceedings{fijalkow2020ijcai-assume,
title = {{Assume-Guarantee Synthesis for Prompt Linear Temporal Logic}},
author = {Fijalkow, Nathanaël and Maubert, Bastien and Murano, Aniello and Vardi, Moshe Y.},
booktitle = {International Joint Conference on Artificial Intelligence},
year = {2020},
pages = {117-123},
doi = {10.24963/IJCAI.2020/17},
url = {https://mlanthology.org/ijcai/2020/fijalkow2020ijcai-assume/}
}