Distributed synthesis for LTL fragments Conference Paper


Author(s): Chatterjee, Krishnendu; Henzinger, Thomas A; Otop, Jan; Pavlogiannis, Andreas
Title: Distributed synthesis for LTL fragments
Affiliation IST Austria
Abstract: 2013 Formal Methods in Computer-Aided Design, FMCAD 2013 2013, Article number 6679386, Pages 18-25 13th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2013; Portland, OR; United States; 20 October 2013 through 23 October 2013; Code 102425 Distributed synthesis for LTL fragments (Conference Paper) Chatterjee, K. , Henzinger, T.A. , Otop, J. , Pavlogiannis, A. IST, Austria View references (21) Abstract We consider the distributed synthesis problem for temporal 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 LTL and 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.
Keywords: temporal operators; liveness; reachability; Temporal logic specifications; Undecidability; Information forks; Synthesis problems
Conference Title: FMCAD: Formal Methods in Computer-Aided Design
Conference Dates: October 20 - 23, 2013
Conference Location: Portland, OR, USA
Publisher: Springer  
Date Published: 2013-01-01
Start Page: 18
End Page: 25
DOI: 10.1109/FMCAD.2013.6679386
Notes: The research was supported by Austrian Science Fund (FWF) Grant No P 23499- N23, FWF NFN Grant No S11407-N23 (RiSE), ERC Start grant (279307: Graph Games), Microsoft faculty fellows award, the Austrian Science Fund NFN RiSE (Rigorous Systems Engineering), the ERC Advanced Grant QUAREM (Quantitative Reactive Modeling). A Technical Report of this paper is available at: https://repository.ist.ac.at/id/eprint/130.
Open access: yes (repository)
IST Austria Authors
  1. Thomas A. Henzinger
    415 Henzinger
  2. Jan Otop
    16 Otop
Related IST Austria Work