Jacobs, Swen, Tentrup, Leander and Zimmermann, Martin 
ORCID: 0000-0002-8038-2453
(2016)
Distributed PROMPT-LTL Synthesis.
.
|
Text
jtz.pdf - Published version Download (158kB) | Preview |
Abstract
We consider the synthesis of distributed implementations for specifications in Prompt Linear Temporal Logic (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 systems, we show that, despite being more powerful, the distributed realizability problem for PROMPT-LTL is not harder than its LTL counterpart. For asynchronous systems we have to consider an assume-guarantee synthesis problem, as we have to express scheduling assumptions. 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.
| Item Type: | Conference or Workshop Item (Unspecified) |
|---|---|
| Additional Information: | In Proceedings GandALF 2016, arXiv:1609.03648 |
| Uncontrolled Keywords: | cs.LO, cs.LO, cs.GT |
| Depositing User: | Symplectic Admin |
| Date Deposited: | 15 Jul 2019 13:03 |
| Last Modified: | 24 Jan 2023 20:30 |
| DOI: | 10.4204/EPTCS.226.16 |
| Related URLs: | |
| URI: | https://livrepository.liverpool.ac.uk/id/eprint/3049693 |
Dimensions
Dimensions
