---
_id: '1609'
abstract:
- lang: eng
  text: The synthesis problem asks for the automatic construction of a system from
    its specification. In the traditional setting, the system is “constructed from
    scratch” rather than composed from reusable components. However, this is rare
    in practice, and almost every non-trivial software system relies heavily on the
    use of libraries of reusable components. Recently, Lustig and Vardi introduced
    dataflow and controlflow synthesis from libraries of reusable components. They
    proved that dataflow synthesis is undecidable, while controlflow synthesis is
    decidable. The problem of controlflow synthesis from libraries of probabilistic
    components was considered by Nain, Lustig and Vardi, and was shown to be decidable
    for qualitative analysis (that asks that the specification be satisfied with probability
    1). Our main contribution for controlflow synthesis from probabilistic components
    is to establish better complexity bounds for the qualitative analysis problem,
    and to show that the more general quantitative problem is undecidable. For the
    qualitative analysis, we show that the problem (i) is EXPTIME-complete when the
    specification is given as a deterministic parity word automaton, improving the
    previously known 2EXPTIME upper bound; and (ii) belongs to UP ∩ coUP and is parity-games
    hard, when the specification is given directly as a parity condition on the components,
    improving the previously known EXPTIME upper bound.
acknowledgement: 'This research was supported by Austrian Science Fund (FWF) Grant
  No P23499- N23, FWF NFN Grant No S11407-N23 (SHiNE), ERC Start grant (279307: Graph
  Games), EU FP7 Project Cassting, NSF grants CNS 1049862 and CCF-1139011, by NSF
  Expeditions in Computing project “ExCAPE: Expeditions in Computer Augmented Program
  Engineering”, by BSF grant 9800096, and by gift from Intel.'
alternative_title:
- LNCS
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: Laurent
  full_name: Doyen, Laurent
  last_name: Doyen
- first_name: Moshe
  full_name: Vardi, Moshe
  last_name: Vardi
citation:
  ama: 'Chatterjee K, Doyen L, Vardi M. The complexity of synthesis from probabilistic
    components. In: <i>42nd International Colloquium</i>. Vol 9135. Springer Nature;
    2015:108-120. doi:<a href="https://doi.org/10.1007/978-3-662-47666-6_9">10.1007/978-3-662-47666-6_9</a>'
  apa: 'Chatterjee, K., Doyen, L., &#38; Vardi, M. (2015). The complexity of synthesis
    from probabilistic components. In <i>42nd International Colloquium</i> (Vol. 9135,
    pp. 108–120). Kyoto, Japan: Springer Nature. <a href="https://doi.org/10.1007/978-3-662-47666-6_9">https://doi.org/10.1007/978-3-662-47666-6_9</a>'
  chicago: Chatterjee, Krishnendu, Laurent Doyen, and Moshe Vardi. “The Complexity
    of Synthesis from Probabilistic Components.” In <i>42nd International Colloquium</i>,
    9135:108–20. Springer Nature, 2015. <a href="https://doi.org/10.1007/978-3-662-47666-6_9">https://doi.org/10.1007/978-3-662-47666-6_9</a>.
  ieee: K. Chatterjee, L. Doyen, and M. Vardi, “The complexity of synthesis from probabilistic
    components,” in <i>42nd International Colloquium</i>, Kyoto, Japan, 2015, vol.
    9135, pp. 108–120.
  ista: 'Chatterjee K, Doyen L, Vardi M. 2015. The complexity of synthesis from probabilistic
    components. 42nd International Colloquium. ICALP: Automata, Languages and Programming,
    LNCS, vol. 9135, 108–120.'
  mla: Chatterjee, Krishnendu, et al. “The Complexity of Synthesis from Probabilistic
    Components.” <i>42nd International Colloquium</i>, vol. 9135, Springer Nature,
    2015, pp. 108–20, doi:<a href="https://doi.org/10.1007/978-3-662-47666-6_9">10.1007/978-3-662-47666-6_9</a>.
  short: K. Chatterjee, L. Doyen, M. Vardi, in:, 42nd International Colloquium, Springer
    Nature, 2015, pp. 108–120.
conference:
  end_date: 2015-07-10
  location: Kyoto, Japan
  name: 'ICALP: Automata, Languages and Programming'
  start_date: 2015-07-06
date_created: 2018-12-11T11:53:00Z
date_published: 2015-06-20T00:00:00Z
date_updated: 2022-02-01T15:04:44Z
day: '20'
department:
- _id: KrCh
doi: 10.1007/978-3-662-47666-6_9
ec_funded: 1
intvolume: '      9135'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: http://arxiv.org/abs/1502.04844
month: '06'
oa: 1
oa_version: Preprint
page: 108 - 120
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: P 23499-N23
  name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S11407
  name: Game Theory
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '279307'
  name: 'Quantitative Graph Games: Theory and Applications'
publication: 42nd International Colloquium
publication_identifier:
  isbn:
  - 978-3-662-47665-9
publication_status: published
publisher: Springer Nature
publist_id: '5557'
quality_controlled: '1'
scopus_import: '1'
status: public
title: The complexity of synthesis from probabilistic components
type: conference
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
volume: 9135
year: '2015'
...
---
_id: '1610'
abstract:
- lang: eng
  text: The edit distance between two words w1, w2 is the minimal number of word operations
    (letter insertions, deletions, and substitutions) necessary to transform w1 to
    w2. The edit distance generalizes to languages L1,L2, where the edit distance
    is the minimal number k such that for every word from L1 there exists a word in
    L2 with edit distance at most k. We study the edit distance computation problem
    between pushdown automata and their subclasses. The problem of computing edit
    distance to pushdown automata is undecidable, and in practice, the interesting
    question is to compute the edit distance from a pushdown automaton (the implementation,
    a standard model for programs with recursion) to a regular language (the specification).
    In this work, we present a complete picture of decidability and complexity for
    deciding whether, for a given threshold k, the edit distance from a pushdown automaton
    to a finite automaton is at most k.
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
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: Rasmus
  full_name: Ibsen-Jensen, Rasmus
  id: 3B699956-F248-11E8-B48F-1D18A9856A87
  last_name: Ibsen-Jensen
  orcid: 0000-0003-4783-0389
- first_name: Jan
  full_name: Otop, Jan
  id: 2FC5DA74-F248-11E8-B48F-1D18A9856A87
  last_name: Otop
citation:
  ama: 'Chatterjee K, Henzinger TA, Ibsen-Jensen R, Otop J. Edit distance for pushdown
    automata. In: <i>42nd International Colloquium</i>. Vol 9135. Springer Nature;
    2015:121-133. doi:<a href="https://doi.org/10.1007/978-3-662-47666-6_10">10.1007/978-3-662-47666-6_10</a>'
  apa: 'Chatterjee, K., Henzinger, T. A., Ibsen-Jensen, R., &#38; Otop, J. (2015).
    Edit distance for pushdown automata. In <i>42nd International Colloquium</i> (Vol.
    9135, pp. 121–133). Kyoto, Japan: Springer Nature. <a href="https://doi.org/10.1007/978-3-662-47666-6_10">https://doi.org/10.1007/978-3-662-47666-6_10</a>'
  chicago: Chatterjee, Krishnendu, Thomas A Henzinger, Rasmus Ibsen-Jensen, and Jan
    Otop. “Edit Distance for Pushdown Automata.” In <i>42nd International Colloquium</i>,
    9135:121–33. Springer Nature, 2015. <a href="https://doi.org/10.1007/978-3-662-47666-6_10">https://doi.org/10.1007/978-3-662-47666-6_10</a>.
  ieee: K. Chatterjee, T. A. Henzinger, R. Ibsen-Jensen, and J. Otop, “Edit distance
    for pushdown automata,” in <i>42nd International Colloquium</i>, Kyoto, Japan,
    2015, vol. 9135, no. Part II, pp. 121–133.
  ista: 'Chatterjee K, Henzinger TA, Ibsen-Jensen R, Otop J. 2015. Edit distance for
    pushdown automata. 42nd International Colloquium. ICALP: Automata, Languages and
    Programming, LNCS, vol. 9135, 121–133.'
  mla: Chatterjee, Krishnendu, et al. “Edit Distance for Pushdown Automata.” <i>42nd
    International Colloquium</i>, vol. 9135, no. Part II, Springer Nature, 2015, pp.
    121–33, doi:<a href="https://doi.org/10.1007/978-3-662-47666-6_10">10.1007/978-3-662-47666-6_10</a>.
  short: K. Chatterjee, T.A. Henzinger, R. Ibsen-Jensen, J. Otop, in:, 42nd International
    Colloquium, Springer Nature, 2015, pp. 121–133.
conference:
  end_date: 2015-07-10
  location: Kyoto, Japan
  name: 'ICALP: Automata, Languages and Programming'
  start_date: 2015-07-06
date_created: 2018-12-11T11:53:01Z
date_published: 2015-07-01T00:00:00Z
date_updated: 2023-02-23T12:26:24Z
day: '01'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1007/978-3-662-47666-6_10
ec_funded: 1
external_id:
  arxiv:
  - '1504.08259'
intvolume: '      9135'
issue: Part II
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://arxiv.org/abs/1504.08259
month: '07'
oa: 1
oa_version: None
page: 121 - 133
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '267989'
  name: Quantitative Reactive Modeling
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: Z211
  name: The Wittgenstein Prize
- _id: 2584A770-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: P 23499-N23
  name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S11407
  name: Game Theory
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '279307'
  name: 'Quantitative Graph Games: Theory and Applications'
- _id: 2587B514-B435-11E9-9278-68D0E5697425
  name: Microsoft Research Faculty Fellowship
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
publication: 42nd International Colloquium
publication_identifier:
  isbn:
  - 978-3-662-47665-9
publication_status: published
publisher: Springer Nature
publist_id: '5556'
pubrep_id: '321'
quality_controlled: '1'
related_material:
  record:
  - id: '465'
    relation: later_version
    status: public
  - id: '5438'
    relation: earlier_version
    status: public
scopus_import: '1'
status: public
title: Edit distance for pushdown automata
type: conference
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
volume: 9135
year: '2015'
...