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.

Text main.pdf - Author Accepted Manuscript Download (465kB)

Abstract

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:	Author Publisher
URI:	https://livrepository.liverpool.ac.uk/id/eprint/3028984