• DocumentCode
    651302
  • Title

    Distributed synthesis for LTL fragments

  • Author

    Chatterjee, Krishnendu ; Henzinger, Thomas A. ; Otop, Jan ; Pavlogiannis, Andreas

  • Author_Institution
    IST Austria, Klosterneuburg, Austria
  • fYear
    2013
  • fDate
    20-23 Oct. 2013
  • Firstpage
    18
  • Lastpage
    25
  • 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
    decidability; temporal logic; LTL fragments; decidability; disjoint inputs; distributed synthesis problem; information fork-meet structure; star architectures; temporal logic specifications; temporal operators; Computer architecture; Input variables; Law; Safety; Turing machines;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Formal Methods in Computer-Aided Design (FMCAD), 2013
  • Conference_Location
    Portland, OR
  • Type

    conf

  • DOI
    10.1109/FMCAD.2013.6679386
  • Filename
    6679386