{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,20]],"date-time":"2026-01-20T11:19:24Z","timestamp":1768907964994,"version":"3.49.0"},"reference-count":73,"publisher":"Association for Computing Machinery (ACM)","issue":"4-5","license":[{"start":{"date-parts":[[2022,5,9]],"date-time":"2022-05-09T00:00:00Z","timestamp":1652054400000},"content-version":"vor","delay-in-days":281,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"},{"start":{"date-parts":[[2021,8,1]],"date-time":"2021-08-01T00:00:00Z","timestamp":1627776000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,8,1]],"date-time":"2021-08-01T00:00:00Z","timestamp":1627776000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["RTG 2236 \u201cUnRAVeL\u201d"],"award-info":[{"award-number":["RTG 2236 \u201cUnRAVeL\u201d"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]},{"name":"European Research Council","award":["Advanced Grant 787914 \u201cFRAPPANT\u201d"],"award-info":[{"award-number":["Advanced Grant 787914 \u201cFRAPPANT\u201d"]}]},{"DOI":"10.13039\/501100001824","name":"Czech Science Foundation","doi-asserted-by":"crossref","award":["GJ20-02328Y"],"award-info":[{"award-number":["GJ20-02328Y"]}],"id":[{"id":"10.13039\/501100001824","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1545126"],"award-info":[{"award-number":["1545126"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["Assured Autonomy"],"award-info":[{"award-number":["Assured Autonomy"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["SDCPS (Contract: FA8750-20-C-0156)"],"award-info":[{"award-number":["SDCPS (Contract: FA8750-20-C-0156)"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Berkeley Deep Drive"},{"DOI":"10.13039\/100004362","name":"Toyota USA","doi-asserted-by":"publisher","award":["the iCyPhy center"],"award-info":[{"award-number":["the iCyPhy center"]}],"id":[{"id":"10.13039\/100004362","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2021,8]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>\n            This paper presents counterexample-guided inductive synthesis (CEGIS) to automatically synthesise probabilistic models. The starting point is a family of finite-stateMarkov chains with related but distinct topologies. Such families can succinctly be described by a sketch of a probabilistic program. Program sketches are programs containing holes. Every hole has a finite repertoire of possible program snippets by which it can be filled.We study several synthesis problems\u2014feasibility, optimal synthesis, and complete partitioning\u2014for a given quantitative specification\n            <jats:inline-formula>\n              <jats:alternatives>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>\u03c6<\/mml:mi>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>\n            . Feasibility amounts to determine a family member satisfying\n            <jats:inline-formula>\n              <jats:alternatives>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>\u03c6<\/mml:mi>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>\n            , optimal synthesis amounts to find a family member that maximises the probability to satisfy\n            <jats:inline-formula>\n              <jats:alternatives>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>\u03c6<\/mml:mi>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>\n            , and complete partitioning splits the family in satisfying and refuting members. Each of these problems can be considered under the additional constraint of minimising the total cost of instantiations, e.g., what are all possible instantiations for\n            <jats:inline-formula>\n              <jats:alternatives>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>\u03c6<\/mml:mi>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>\n            that are within a certain budget? The synthesis problems are tackled using a CEGIS approach. The crux is to aggressively prune the search space by using counterexamples provided by a probabilistic model checker. Counterexamples can be viewed as sub-Markov chains that rule out all family members that share this sub-chain. Our CEGIS approach leverages efficient probabilisticmodel checking,modern SMT solving, and programsnippets as counterexamples. Experiments on case studies froma diverse nature\u2014controller synthesis, program sketching, and security\u2014show that synthesis among up to a million candidate designs can be done using a few thousand verification queries.\n          <\/jats:p>","DOI":"10.1007\/s00165-021-00547-2","type":"journal-article","created":{"date-parts":[[2021,5,9]],"date-time":"2021-05-09T16:02:19Z","timestamp":1620576139000},"page":"637-667","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Counterexample-guided inductive synthesis for probabilistic systems"],"prefix":"10.1145","volume":"33","author":[{"given":"Milan","family":"\u010ce\u0161ka","sequence":"first","affiliation":[{"name":"Brno University of Technology, Brno, Czech Republic"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christian","family":"Hensel","sequence":"additional","affiliation":[{"name":"RWTH Aachen University, Aachen, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0978-8466","authenticated-orcid":false,"given":"Sebastian","family":"Junges","sequence":"additional","affiliation":[{"name":"University of California, Berkeley, CA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[{"name":"RWTH Aachen University, Aachen, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"\u00c1brah\u00e1m E Becker B Dehnert C Jansen N Katoen J-P Wimmer R (2014) Counterexample generation for discrete-time Markov models: An introductory survey Springer vol 8483 of LNCS pp 65\u2013121","DOI":"10.1007\/978-3-319-07317-0_3"},{"key":"e_1_2_1_2_2_2","unstructured":"Alur R Bod\u00edk R Dallal E Fisman D Garg P Juniwal G Kress-Gazit H Madhusudan P Martin MMK Raghothaman M Saha S Seshia SA Singh R Solar-Lezama A Torlak E Udupa A (2015) Syntax-guided synthesis. In: Dependable software systems engineering IOS Press vol 40 of NATO Science for Peace and Security Series pp 1\u201325"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Abate A David C Kesseli P Kroening D Polgreen E (2018) Counterexample guided inductive synthesis modulo theories. In: CAV (1) Springer vol 10981 of LNCS pp 270\u2013288","DOI":"10.1007\/978-3-319-96145-3_15"},{"key":"e_1_2_1_2_4_2","first-page":"94","article-title":"20 years of modal and mixed specifications","volume":"95","author":"Antonik A","year":"2008","journal-title":"Bulletin of the EATCS"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/3208071"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"publisher","DOI":"10.1109\/43.766730"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Baier C de\u00a0Alfaro L Forejt V Kwiatkowska M (2018) Model checking probabilistic systems. In: Handbook of model checking Springer pp 963\u2013999","DOI":"10.1007\/978-3-319-10575-8_28"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Budde CE Dehnert C Hahn EM Hartmanns A Junges S Turrini A (2017) JANI: quantitative model and tool interaction. In: TACAS vol 10206 of LNCS pp 151\u2013168","DOI":"10.1007\/978-3-662-54580-5_9"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Bartocci E Grosu R Katsaros P Ramakrishnan CR Smolka SA (2011) Model repair for probabilistic systems. In: TACAS Springer vol 6605 of LNCS pp 326\u2013340","DOI":"10.1007\/978-3-642-19835-9_30"},{"key":"e_1_2_1_2_10_2","unstructured":"Biere A Heule M van Maaren H Walsh T (eds) (2009) Handbook of Satisfiability IOS Press vol 185 of Frontiers in artificial intelligence and applications"},{"key":"e_1_2_1_2_11_2","unstructured":"Baier C Katoen J-P (2008) Principles of model checking MIT Press"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Benes N K\u0159et\u00ednsk\u00fd J Larsen KG M\u00f8ller MH Srba J (2012) Dual-priced modal transition systems with time durations. In: LPAR Springer vol 7180 of LNCS pp 122\u2013137","DOI":"10.1007\/978-3-642-28717-6_12"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-015-0215-4"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Bornholt J Torlak E Grossman D Ceze L (2016) Optimizing synthesis with metasketches. In: POPL ACM pp 775\u2013788","DOI":"10.1145\/2914770.2837666"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Cardelli L \u010ce\u0161ka M Fr\u00e4nzle M Kwiatkowska M Laurenti L Paoletti N Whitby M (2017) Syntax-guided optimal synthesis for chemical reaction networks. In: CAV Springer vol 10427 of LNCS pp 375\u2013395","DOI":"10.1007\/978-3-319-63390-9_20"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"\u010cern\u00fd P Chatterjee K Henzinger TA Radhakrishna A Singh R (2011) Quantitative synthesis for concurrent programs. In: CAV Springer vol 6806 of LNCS pp 243\u2013259","DOI":"10.1007\/978-3-642-22110-1_20"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Chaudhuri S Clochard M Solar-Lezama A (2014) Bridging boolean and quantitative synthesis using smoothed proof search. In: POPL ACM pp 207\u2013220","DOI":"10.1145\/2578855.2535859"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-017-0432-4"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-016-0265-2"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"publisher","DOI":"10.1109\/TR.2015.2452931"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/2330667.2330686"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"Chen T Hahn EM Han T Kwiatkowska MZ Qu H Zhang L (2013) Model repair for Markov decision processes. In: TASE IEEE pp 85\u201392","DOI":"10.1109\/TASE.2013.20"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"\u010ce\u0161ka M Hensel C Junges S Katoen J-P (2019) Counterexample-driven synthesis for probabilistic program sketches. In: Formal methods \u2013 the next 30 years Springer International Publishing vol 11800 of LNCS pp 101\u2013120","DOI":"10.1007\/978-3-030-30942-8_8"},{"key":"e_1_2_1_2_24_2","unstructured":"Chonev V (2017) Reachability in augmented interval Markov chains. CoRR abs\/1701.02996"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"crossref","unstructured":"\u010ce\u0161ka M Jansen N Junges S Katoen J-P (2019) Shepherding hordes of Markov chains. In: TACAS Springer vol 11428 of LNCS","DOI":"10.1007\/978-3-030-17465-1_10"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"crossref","unstructured":"Calinescu R \u010ce\u0161ka M Gerasimou S Kwiatkowska M Paoletti N (2017) Designing robust software systems through parametric Markov chain synthesis. In: ICSA IEEE pp 131\u2013140","DOI":"10.1109\/ICSA.2017.16"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Calinescu R \u010ce\u0161ka M Gerasimou S Kwiatkowska M Paoletti N (2017) RODES: A robust-design synthesis tool for probabilistic systems. In: QEST Springer pp 304\u2013308","DOI":"10.1007\/978-3-319-66335-7_20"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2018.05.013"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"Dehnert C Junges S Katoen J-P Volk M (2017) A storm is coming: A modern probabilistic model checker. In: CAV Springer vol 10427 of LNCS pp 592\u2013600","DOI":"10.1007\/978-3-319-63390-9_31"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","unstructured":"Dehnert C Jansen N Wimmer R \u00c1brah\u00e1m E Katoen J-P (2014) Fast debugging of PRISM models. In ATVA Springer vol 8837 of LNCS pp 146\u2013162","DOI":"10.1007\/978-3-319-11936-6_11"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2013.10.002"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura LM Bj\u00f8rner N (2008) Z3: an efficient SMT solver. In: TACAS Springer vol 4963 of LNCS pp 337\u2013340","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"crossref","unstructured":"Dureja R Rozier KY (2018) More scalable LTL model checking via discovering design-space dependencies. In: TACAS (1) Springer vol 10805 of LNCS pp 309\u2013327","DOI":"10.1007\/978-3-319-89960-2_17"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2015.2421318"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"publisher","DOI":"10.1561\/2500000010"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.infsof.2012.07.017"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"crossref","unstructured":"Gerasimou S Tamburrelli G Calinescu R (2015) Search-based synthesis of probabilistic models for quality-of-service software engineering. In: ASE IEEE Computer Society pp 319\u2013330","DOI":"10.1109\/ASE.2015.22"},{"issue":"4","key":"e_1_2_1_2_38_2","first-page":"331","article-title":"Quantitative reactive modeling and verification","volume":"28","author":"Henzinger TA","year":"2013","journal-title":"Comput Sci - R&D"},{"key":"e_1_2_1_2_39_2","unstructured":"Hensel C (2018) The probabilistic model checker storm: Symbolic methods for probabilistic model checking. PhD thesis RWTH Aachen University Germany"},{"key":"e_1_2_1_2_40_2","doi-asserted-by":"crossref","unstructured":"Hartmanns A Hermanns H (2014) The modest toolset: An integrated environment for quantitative modelling and verification. In: TACAS Springer pp 593\u2013598","DOI":"10.1007\/978-3-642-54862-8_51"},{"key":"e_1_2_1_2_41_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-010-0146-x"},{"key":"e_1_2_1_2_42_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2009.5"},{"key":"e_1_2_1_2_43_2","doi-asserted-by":"crossref","unstructured":"Hartmanns A Klauck M Parker D Quatmann T Ruijters E (2019) The quantitative verification benchmark set. In: TACAS (1) Springer vol 11427 of Lecture Notes in Computer Science pp 344\u2013350","DOI":"10.1007\/978-3-030-17462-0_20"},{"key":"e_1_2_1_2_44_2","doi-asserted-by":"crossref","unstructured":"Jansen N Humphrey L Tumova J Topcu U (2019) Structured synthesis for probabilistic systems. In: NFM Springer vol 11460 of LNCS pp 237\u2013254","DOI":"10.1007\/978-3-030-20652-9_16"},{"key":"e_1_2_1_2_45_2","doi-asserted-by":"crossref","unstructured":"Junges S Jansen N Dehnert C Topcu U Katoen J-P (2016) Safety-constrained reinforcement learning for MDPs. In: TACAS Springer vol 9636 of LNCS pp 130\u2013146","DOI":"10.1007\/978-3-662-49674-9_8"},{"key":"e_1_2_1_2_46_2","unstructured":"Junges S Jansen N Wimmer R Quatmann T Winterer L Katoen J-P Becker B (2018) Finite-state controllers of POMDPs using parameter synthesis. In: UAI AUAI Press pp 519\u2013529"},{"key":"e_1_2_1_2_47_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-017-0294-5"},{"key":"e_1_2_1_2_48_2","unstructured":"Junges S (2020) Parameter synthesis in Markov models. PhD thesis RWTH Aachen University Germany to appear"},{"key":"e_1_2_1_2_49_2","doi-asserted-by":"crossref","unstructured":"Katoen J-P (2016) The probabilistic model checking landscape. In: LICS ACM pp 31\u201345","DOI":"10.1145\/2933575.2934574"},{"key":"e_1_2_1_2_50_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0004-3702(98)00023-X"},{"key":"e_1_2_1_2_51_2","doi-asserted-by":"crossref","unstructured":"Kwiatkowska M Norman G Parker D (2011) Prism 4.0: Verification of probabilistic real-time systems. In: CAV vol 6806 of LNCS Springer pp 585\u2013591","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"e_1_2_1_2_52_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2008.12.058"},{"key":"e_1_2_1_2_53_2","doi-asserted-by":"crossref","unstructured":"Kret\u00ednsk\u00fd J (2017) 30 years of modal transition systems: Survey of extensions and analysis. In: Models algorithms logics and tools Springer vol 10460 of LNCS pp 36\u201374","DOI":"10.1007\/978-3-319-63121-9_3"},{"key":"e_1_2_1_2_54_2","doi-asserted-by":"crossref","first-page":"59","DOI":"10.1016\/j.infsof.2017.10.001","article-title":"Feature-family-based reliability analysis of software product lines","volume":"94","author":"Lanna A","year":"2018","journal-title":"Inform Softw Technol"},{"key":"e_1_2_1_2_55_2","unstructured":"Larsen KG Thomsen B (1988) A modal process logic. In: LICS IEEE Computer Society pp 203\u2013210"},{"key":"e_1_2_1_2_56_2","unstructured":"Meuleau N Kim K-E Kaelbling LP Cassandra AR (1999) Solving POMDPs by searching the space of finite policies. In: UAI Morgan Kaufmann Publishers Inc. pp 417\u2013426"},{"key":"e_1_2_1_2_57_2","doi-asserted-by":"publisher","DOI":"10.1145\/229542.229547"},{"key":"e_1_2_1_2_58_2","doi-asserted-by":"crossref","unstructured":"Nori AV Ozair S Rajamani SK Vijaykeerthy D (2015) Efficient synthesis of probabilistic programs. In: PLDI ACM pp 208\u2013217","DOI":"10.1145\/2813885.2737982"},{"key":"e_1_2_1_2_59_2","doi-asserted-by":"crossref","unstructured":"Quatmann T Dehnert C Jansen N Junges S Katoen J-P (2016) Parameter synthesis for Markov models: Faster than ever. In: ATVA vol 9938 of LNCS pp 50\u201367","DOI":"10.1007\/978-3-319-46520-3_4"},{"key":"e_1_2_1_2_60_2","doi-asserted-by":"crossref","unstructured":"Quatmann T Jansen N Dehnert C Wimmer R \u00c1brah\u00e1m E Katoen J-P Becker B (2015) Counterexamples for expected rewards. In: FM Springer vol 9109 of LNCS pp 435\u2013452","DOI":"10.1007\/978-3-319-19249-9_27"},{"key":"e_1_2_1_2_61_2","doi-asserted-by":"crossref","unstructured":"Rodrigues GN Alves V Nunes V Lanna A Cordy M Schobbens P-Y Sharifloo AM Legay A (2015) Modeling and verification for probabilistic properties in software product lines. In: HASE IEEE pp 173\u2013180","DOI":"10.1109\/HASE.2015.34"},{"key":"e_1_2_1_2_62_2","doi-asserted-by":"crossref","unstructured":"Rosenblum DS (2016) The power of probabilistic thinking. In: ASE ACM p 3","DOI":"10.1145\/2970276.2985780"},{"key":"e_1_2_1_2_63_2","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2007.911342"},{"key":"e_1_2_1_2_64_2","doi-asserted-by":"crossref","unstructured":"Solar-Lezama A Jones CG Bodik R (2008) Sketching concurrent data structures. In: PLDI ACM pp 136\u2013148","DOI":"10.1145\/1379022.1375599"},{"key":"e_1_2_1_2_65_2","doi-asserted-by":"crossref","unstructured":"Solar-Lezama A Tancau L Bodik R Seshia S Saraswat V (2006) Combinatorial sketching for finite programs. In: ASPLOS ACM pp 404\u2013415","DOI":"10.1145\/1168918.1168907"},{"issue":"5","key":"e_1_2_1_2_66_2","first-page":"475","volume":"15","author":"Solar-Lezama A","year":"2013","journal-title":"Program sketching. STTT"},{"key":"e_1_2_1_2_67_2","doi-asserted-by":"crossref","unstructured":"Solar-Lezama A Rabbah RM Bod\u00edk R Ebcioglu K (2005) Programming by sketching for bit-streaming programs. In: PLDI ACM pp 281\u2013294","DOI":"10.1145\/1064978.1065045"},{"key":"e_1_2_1_2_68_2","doi-asserted-by":"crossref","unstructured":"Varshosaz M Khosravi R (2013) Discrete time Markov chain families: modeling and verification of probabilistic software product lines. In: SPLC Workshops ACM pp 34\u201341","DOI":"10.1145\/2499777.2500725"},{"key":"e_1_2_1_2_69_2","doi-asserted-by":"crossref","unstructured":"Vandin A ter Beek MH Legay A Lluch-Lafuente A (2018) Qflan: A tool for the quantitative analysis of highly reconfigurable systems. In: FM Springer vol 10951 of LNCS pp 329\u2013337","DOI":"10.1007\/978-3-319-95582-7_19"},{"key":"e_1_2_1_2_70_2","doi-asserted-by":"crossref","unstructured":"Wimmer R Jansen N \u00c1brah\u00e1m E Becker B Katoen J-P (2012) Minimal critical subsystems for discrete-time Markov models. In TACAS Springer vol 7214 of LNCS pp 299\u2013314","DOI":"10.1007\/978-3-642-28756-5_21"},{"key":"e_1_2_1_2_71_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2014.06.020"},{"key":"e_1_2_1_2_72_2","doi-asserted-by":"crossref","unstructured":"Wimmer R. Jansen N. Vorpahl A. \u00c1brah\u00e1m E. Katoen J.-P. Becker B.: High-level counterexamples for probabilistic automata. Log Methods Comput Sci 11 (1) (2015)","DOI":"10.2168\/LMCS-11(1:15)2015"},{"key":"e_1_2_1_2_73_2","doi-asserted-by":"crossref","unstructured":"Zhou W Li W (2018) Safety-aware apprenticeship learning. In CAV'18 Springer vol 10981 of LNCS pp 662\u2013680","DOI":"10.1007\/978-3-319-96145-3_38"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-021-00547-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00165-021-00547-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-021-00547-2","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-021-00547-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-021-00547-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T16:25:04Z","timestamp":1641486304000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-021-00547-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,8]]},"references-count":73,"journal-issue":{"issue":"4-5","published-print":{"date-parts":[[2021,8]]}},"alternative-id":["10.1007\/s00165-021-00547-2"],"URL":"https:\/\/doi.org\/10.1007\/s00165-021-00547-2","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,8]]},"assertion":[{"value":"3 March 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"5 March 2021","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"24 March 2021","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"9 May 2021","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}