---
OA_place: repository
OA_type: green
_id: '1376'
abstract:
- lang: eng
  text: '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.'
article_processing_charge: No
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Jan
  full_name: Otop, Jan
  id: 2FC5DA74-F248-11E8-B48F-1D18A9856A87
  last_name: Otop
- first_name: Andreas
  full_name: Pavlogiannis, Andreas
  id: 49704004-F248-11E8-B48F-1D18A9856A87
  last_name: Pavlogiannis
  orcid: 0000-0002-8943-0722
citation:
  ama: '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>'
  apa: '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>'
  chicago: 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>.
  ieee: 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.
  ista: '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.'
  mla: 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>.
  short: 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.
conference:
  end_date: 2013-10-23
  location: Portland, OR, United States
  name: 'FMCAD: Formal Methods in Computer-Aided Design'
  start_date: 2013-10-20
corr_author: '1'
date_created: 2018-12-11T11:51:40Z
date_published: 2013-12-11T00:00:00Z
date_updated: 2025-06-26T08:33:43Z
day: '11'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1109/FMCAD.2013.6679386
ec_funded: 1
fulldoi: https://doi.org/10.1109/FMCAD.2013.6679386
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://doi.org/10.15479/AT:IST-2013-130-v1-1
month: '12'
oa: 1
oa_version: Preprint
page: 18 - 25
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: P 23499-N23
  name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '279307'
  name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '267989'
  name: Quantitative Reactive Modeling
- _id: 2587B514-B435-11E9-9278-68D0E5697425
  name: Microsoft Research Faculty Fellowship
publication: 13th International Conference on Formal Methods in Computer-Aided Design
publication_status: published
publisher: IEEE
publist_id: '5835'
quality_controlled: '1'
related_material:
  record:
  - id: '5406'
    relation: earlier_version
    status: public
scopus_import: '1'
status: public
title: Distributed synthesis for LTL fragments
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2013'
...