Distributed synthesis for parameterized temporal logics

Jacobs, Swen, Tentrup, Leander and Zimmermann, Martin ORCID: 0000-0002-8038-2453
(2018) Distributed synthesis for parameterized temporal logics. INFORMATION AND COMPUTATION, 262. pp. 311-328.

[img] Text
main.pdf - Author Accepted Manuscript

Download (465kB)


We consider the synthesis of distributed implementations for specifications in parameterized temporal logics such as PROMPT-LTL, which extends LTL by temporal operators equipped with parameters that bound their scope. For single process synthesis it is well-established that such parametric extensions do not increase worst-case complexities. For synchronous distributed systems we show that, despite being more powerful, the realizability problem for PROMPT-LTL is not harder than its LTL counterpart. For asynchronous systems we have to express scheduling assumptions and therefore consider an assume-guarantee synthesis problem. As asynchronous distributed synthesis is already undecidable for LTL, we give a semi-decision procedure for the PROMPT-LTL assume-guarantee synthesis problem based on bounded synthesis. Finally, we show that our results extend to the stronger logics PLTL and PLDL.

Item Type: Article
Additional Information: Extended version of arXiv:1509.05144. Preprint submitted to Information and Computation
Uncontrolled Keywords: Distributed synthesis, Distributed realizability, Incomplete information, Parametric linear temporal logic, Parametric linear dynamic logic
Depositing User: Symplectic Admin
Date Deposited: 21 Nov 2018 10:52
Last Modified: 19 Jan 2023 01:12
DOI: 10.1016/j.ic.2018.09.009
Related URLs:
URI: https://livrepository.liverpool.ac.uk/id/eprint/3028984