[{"alternative_title":["LNCS"],"department":[{"_id":"KrCh"}],"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.","title":"The complexity of synthesis from probabilistic components","oa":1,"publication_status":"published","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","_id":"1609","month":"06","intvolume":"      9135","citation":{"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.","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>.","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>","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.","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>.","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>","short":"K. Chatterjee, L. Doyen, M. Vardi, in:, 42nd International Colloquium, Springer Nature, 2015, pp. 108–120."},"day":"20","abstract":[{"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.","lang":"eng"}],"status":"public","ec_funded":1,"author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee"},{"full_name":"Doyen, Laurent","first_name":"Laurent","last_name":"Doyen"},{"last_name":"Vardi","full_name":"Vardi, Moshe","first_name":"Moshe"}],"publication":"42nd International Colloquium","publist_id":"5557","date_published":"2015-06-20T00:00:00Z","conference":{"name":"ICALP: Automata, Languages and Programming","start_date":"2015-07-06","location":"Kyoto, Japan","end_date":"2015-07-10"},"oa_version":"Preprint","type":"conference","language":[{"iso":"eng"}],"publisher":"Springer Nature","doi":"10.1007/978-3-662-47666-6_9","scopus_import":"1","main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1502.04844"}],"publication_identifier":{"isbn":["978-3-662-47665-9"]},"article_processing_charge":"No","volume":9135,"date_updated":"2022-02-01T15:04:44Z","project":[{"call_identifier":"FWF","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory","grant_number":"S11407","call_identifier":"FWF"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"}],"quality_controlled":"1","page":"108 - 120","date_created":"2018-12-11T11:53:00Z","year":"2015"},{"pubrep_id":"321","alternative_title":["LNCS"],"department":[{"_id":"KrCh"},{"_id":"ToHe"}],"publication_status":"published","related_material":{"record":[{"id":"465","status":"public","relation":"later_version"},{"id":"5438","status":"public","relation":"earlier_version"}]},"oa":1,"title":"Edit distance for pushdown automata","_id":"1610","month":"07","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","citation":{"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>.","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.","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>","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>.","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.","short":"K. Chatterjee, T.A. Henzinger, R. Ibsen-Jensen, J. Otop, in:, 42nd International Colloquium, Springer Nature, 2015, pp. 121–133.","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>"},"intvolume":"      9135","day":"01","status":"public","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."}],"ec_funded":1,"publist_id":"5556","publication":"42nd International Colloquium","issue":"Part II","author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A"},{"last_name":"Ibsen-Jensen","first_name":"Rasmus","full_name":"Ibsen-Jensen, Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-4783-0389"},{"full_name":"Otop, Jan","first_name":"Jan","last_name":"Otop","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87"}],"external_id":{"arxiv":["1504.08259"]},"conference":{"name":"ICALP: Automata, Languages and Programming","start_date":"2015-07-06","location":"Kyoto, Japan","end_date":"2015-07-10"},"oa_version":"None","date_published":"2015-07-01T00:00:00Z","language":[{"iso":"eng"}],"arxiv":1,"type":"conference","doi":"10.1007/978-3-662-47666-6_10","publisher":"Springer Nature","publication_identifier":{"isbn":["978-3-662-47665-9"]},"main_file_link":[{"url":"https://arxiv.org/abs/1504.08259","open_access":"1"}],"scopus_import":"1","article_processing_charge":"No","volume":9135,"year":"2015","date_created":"2018-12-11T11:53:01Z","page":"121 - 133","quality_controlled":"1","project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","name":"Quantitative Reactive Modeling","call_identifier":"FP7"},{"name":"The Wittgenstein Prize","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF"},{"call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory","grant_number":"S11407"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"}],"date_updated":"2023-02-23T12:26:24Z"}]