conference paper published yes Krishnendu Chatterjee author 2E5DCA20-F248-11E8-B48F-1D18A9856A870000-0002-4561-241X Thomas A Henzinger author 40876CD8-F248-11E8-B48F-1D18A9856A870000−0002−2985−7724 Jan Otop author 2FC5DA74-F248-11E8-B48F-1D18A9856A87 Andreas Pavlogiannis author 49704004-F248-11E8-B48F-1D18A9856A870000-0002-8943-0722 KrCh department ToHe department FMCAD: Formal Methods in Computer-Aided Design Modern Graph Algorithmic Techniques in Formal Verification project Rigorous Systems Engineering project Quantitative Graph Games: Theory and Applications project Quantitative Reactive Modeling project Microsoft Research Faculty Fellowship project 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. IEEE2013Portland, OR, United States eng 10.1109/FMCAD.2013.6679386 18 - 25 https://research-explorer.ista.ac.at/record/5406 Chatterjee K, Henzinger TA, Otop J, Pavlogiannis A. 2013. Distributed synthesis for LTL fragments. 13th International Conference on Formal Methods in Computer-Aided Design. FMCAD: Formal Methods in Computer-Aided Design, 18–25. K. Chatterjee, T.A. Henzinger, J. Otop, A. Pavlogiannis, in:, 13th International Conference on Formal Methods in Computer-Aided Design, IEEE, 2013, pp. 18–25. K. Chatterjee, T. A. Henzinger, J. Otop, and A. Pavlogiannis, “Distributed synthesis for LTL fragments,” in <i>13th International Conference on Formal Methods in Computer-Aided Design</i>, Portland, OR, United States, 2013, pp. 18–25. Chatterjee, Krishnendu, et al. “Distributed Synthesis for LTL Fragments.” <i>13th International Conference on Formal Methods in Computer-Aided Design</i>, IEEE, 2013, pp. 18–25, doi:<a href="https://doi.org/10.1109/FMCAD.2013.6679386">10.1109/FMCAD.2013.6679386</a>. Chatterjee, Krishnendu, Thomas A Henzinger, Jan Otop, and Andreas Pavlogiannis. “Distributed Synthesis for LTL Fragments.” In <i>13th International Conference on Formal Methods in Computer-Aided Design</i>, 18–25. IEEE, 2013. <a href="https://doi.org/10.1109/FMCAD.2013.6679386">https://doi.org/10.1109/FMCAD.2013.6679386</a>. Chatterjee K, Henzinger TA, Otop J, Pavlogiannis A. Distributed synthesis for LTL fragments. In: <i>13th International Conference on Formal Methods in Computer-Aided Design</i>. IEEE; 2013:18-25. doi:<a href="https://doi.org/10.1109/FMCAD.2013.6679386">10.1109/FMCAD.2013.6679386</a> Chatterjee, K., Henzinger, T. A., Otop, J., &#38; Pavlogiannis, A. (2013). Distributed synthesis for LTL fragments. In <i>13th International Conference on Formal Methods in Computer-Aided Design</i> (pp. 18–25). Portland, OR, United States: IEEE. <a href="https://doi.org/10.1109/FMCAD.2013.6679386">https://doi.org/10.1109/FMCAD.2013.6679386</a> 13762018-12-11T11:51:40Z2025-06-26T08:33:43Z