Earlier Version
Distributed synthesis for LTL Fragments
Chatterjee K, Henzinger TA, Otop J, Pavlogiannis A. 2013. Distributed synthesis for LTL Fragments, IST Austria, 11p.
Download
Technical Report
| Published
| English
Author
Department
Series Title
IST Austria Technical Report
Abstract
We consider the distributed synthesis problem fortemporal logic specifications. Traditionally, the problem has been studied for LTL, and the previous results show that the problem is decidable iff there is no information fork in the architecture. We consider the problem for fragments of LTLand our main results are as follows: (1) We show that the problem is undecidable for architectures with information forks even for the fragment of LTL with temporal operators restricted to next and eventually. (2) For specifications restricted to globally along with non-nested next operators, we establish decidability (in EXPSPACE) for star architectures where the processes receive disjoint inputs, whereas we establish undecidability for architectures containing an information fork-meet structure. (3)Finally, we consider LTL without the next operator, and establish decidability (NEXPTIME-complete) for all architectures for a fragment that consists of a set of safety assumptions, and a set of guarantees where each guarantee is a safety, reachability, or liveness condition.
Publishing Year
Date Published
2013-07-08
Publisher
IST Austria
Page
11
ISSN
IST-REx-ID
Cite this
Chatterjee K, Henzinger TA, Otop J, Pavlogiannis A. Distributed Synthesis for LTL Fragments. IST Austria; 2013. doi:10.15479/AT:IST-2013-130-v1-1
Chatterjee, K., Henzinger, T. A., Otop, J., & Pavlogiannis, A. (2013). Distributed synthesis for LTL Fragments. IST Austria. https://doi.org/10.15479/AT:IST-2013-130-v1-1
Chatterjee, Krishnendu, Thomas A Henzinger, Jan Otop, and Andreas Pavlogiannis. Distributed Synthesis for LTL Fragments. IST Austria, 2013. https://doi.org/10.15479/AT:IST-2013-130-v1-1.
K. Chatterjee, T. A. Henzinger, J. Otop, and A. Pavlogiannis, Distributed synthesis for LTL Fragments. IST Austria, 2013.
Chatterjee K, Henzinger TA, Otop J, Pavlogiannis A. 2013. Distributed synthesis for LTL Fragments, IST Austria, 11p.
Chatterjee, Krishnendu, et al. Distributed Synthesis for LTL Fragments. IST Austria, 2013, doi:10.15479/AT:IST-2013-130-v1-1.
All files available under the following license(s):
Copyright Statement:
This Item is protected by copyright and/or related rights. [...]
Main File(s)
File Name
Access Level
Open Access
Date Uploaded
2018-12-12
MD5 Checksum
855513ebaf6f72228800c5fdb522f93c