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.
Assume-guarantee synthesis for prompt linear temporal logic / Fijalkow, N.; Maubert, B.; Murano, A.; Vardi, M.. - In: IJCAI. - ISSN 1045-0823. - 2021-:(2020), pp. 117-123. (Intervento presentato al convegno 29th International Joint Conference on Artificial Intelligence, IJCAI 2020 nel 2021) [10.24963/ijcai.2020/17].
Assume-guarantee synthesis for prompt linear temporal logic
Maubert B.;Murano A.;
2020
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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
