{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,30]],"date-time":"2026-04-30T03:22:44Z","timestamp":1777519364401,"version":"3.51.4"},"publisher-location":"Cham","reference-count":45,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031757778","type":"print"},{"value":"9783031757785","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,11,18]],"date-time":"2024-11-18T00:00:00Z","timestamp":1731888000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,11,18]],"date-time":"2024-11-18T00:00:00Z","timestamp":1731888000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-3-031-75778-5_15","type":"book-chapter","created":{"date-parts":[[2024,11,17]],"date-time":"2024-11-17T12:08:57Z","timestamp":1731845337000},"page":"309-337","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["(de-)Composed And More: Eager and\u00a0Lazy Specifications (CAMELS) for\u00a0Stochastic Hybrid Systems"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0418-9854","authenticated-orcid":false,"given":"Lisa","family":"Willemsen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5912-4767","authenticated-orcid":false,"given":"Anne","family":"Remke","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5647-6134","authenticated-orcid":false,"given":"Erika","family":"\u00c1brah\u00e1m","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,11,18]]},"reference":[{"key":"15_CR1","doi-asserted-by":"publisher","unstructured":"Abate, A., et al.: Arch-comp23 category report: stochastic models. In: Proceedings of 10th International Workshop on Applied Verification of Continuous and Hybrid Systems. EPiC Series in Computing, vol.\u00a096, pp. 126\u2013150. EasyChair (2023). https:\/\/doi.org\/10.29007\/k7s6","DOI":"10.29007\/k7s6"},{"key":"15_CR2","doi-asserted-by":"publisher","unstructured":"Abate, A., et al.: Arch-comp22 category report: stochastic models. In: Proceedings of the 9th International Workshop on Applied Verification of Continuous and Hybrid Systems. EPiC Series in Computing, vol.\u00a090, pp. 113\u2013141. EasyChair (2022). https:\/\/doi.org\/10.29007\/lsvc","DOI":"10.29007\/lsvc"},{"issue":"6","key":"15_CR3","doi-asserted-by":"publisher","first-page":"624","DOI":"10.3166\/EJC.16.624-641","volume":"16","author":"A Abate","year":"2010","unstructured":"Abate, A., Katoen, J., Lygeros, J., Prandini, M.: Approximate model checking of stochastic hybrid systems. Eur. J. Control. 16(6), 624\u2013641 (2010). https:\/\/doi.org\/10.3166\/EJC.16.624-641","journal-title":"Eur. J. Control."},{"key":"15_CR4","doi-asserted-by":"publisher","unstructured":"Abate, A., Katoen, J., Mereacre, A.: Quantitative automata model checking of autonomous stochastic hybrid systems. In: Proceedings of the 14th ACM International Conference on Hybrid Systems: Computation and Control, pp. 83\u201392. ACM (2011). https:\/\/doi.org\/10.1145\/1967701.1967715","DOI":"10.1145\/1967701.1967715"},{"issue":"11","key":"15_CR5","doi-asserted-by":"publisher","first-page":"2724","DOI":"10.1016\/j.automatica.2008.03.027","volume":"44","author":"A Abate","year":"2008","unstructured":"Abate, A., Prandini, M., Lygeros, J., Sastry, S.: Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems. Automatica 44(11), 2724\u20132734 (2008). https:\/\/doi.org\/10.1016\/j.automatica.2008.03.027","journal-title":"Automatica"},{"key":"15_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1007\/978-3-319-07317-0_3","volume-title":"Formal Methods for Executable Software Models","author":"E \u00c1brah\u00e1m","year":"2014","unstructured":"\u00c1brah\u00e1m, E., Becker, B., Dehnert, C., Jansen, N., Katoen, J.-P., Wimmer, R.: Counterexample generation for discrete-time Markov models: an introductory survey. In: Bernardo, M., Damiani, F., H\u00e4hnle, R., Johnsen, E.B., Schaefer, I. (eds.) SFM 2014. LNCS, vol. 8483, pp. 65\u2013121. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-07317-0_3"},{"key":"15_CR7","doi-asserted-by":"publisher","unstructured":"\u00c1brah\u00e1m, E., Jansen, N., Wimmer, R., Katoen, J., Becker, B.: DTMC model checking by SCC reduction. In: Proceedings of the 7th International Conference on Quantitative Evaluation of Systems (QEST\u201910), pp. 37\u201346. IEEE Computer Society (2010). https:\/\/doi.org\/10.1109\/QEST.2010.13","DOI":"10.1109\/QEST.2010.13"},{"key":"15_CR8","doi-asserted-by":"publisher","unstructured":"Bertrand, N., et al.: Stochastic timed automata. Logical Meth. Comput. Sci. 10(4) (2014). https:\/\/doi.org\/10.2168\/LMCS-10(4:6)2014","DOI":"10.2168\/LMCS-10(4:6)2014"},{"key":"15_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/3-540-36580-X_12","volume-title":"Hybrid Systems: Computation and Control","author":"ML Bujorianu","year":"2003","unstructured":"Bujorianu, M.L., Lygeros, J.: Reachability questions in piecewise deterministic Markov processes. In: Maler, O., Pnueli, A. (eds.) HSCC 2003. LNCS, vol. 2623, pp. 126\u2013140. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-36580-X_12"},{"key":"15_CR10","doi-asserted-by":"publisher","unstructured":"Davis, M.H.: Markov Models & Optimization, 1st edn. Routledge (1993). https:\/\/doi.org\/10.1201\/9780203748039","DOI":"10.1201\/9780203748039"},{"key":"15_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/978-3-319-11936-6_11","volume-title":"Automated Technology for Verification and Analysis","author":"C Dehnert","year":"2014","unstructured":"Dehnert, C., Jansen, N., Wimmer, R., \u00c1brah\u00e1m, E., Katoen, J.-P.: Fast debugging of PRISM models. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 146\u2013162. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-11936-6_11"},{"key":"15_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/978-3-319-21690-4_13","volume-title":"Computer Aided Verification","author":"C Dehnert","year":"2015","unstructured":"Dehnert, C., et al.: PROPhESY: a PRObabilistic ParamEter SYnthesis tool. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 214\u2013231. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_13"},{"key":"15_CR13","doi-asserted-by":"publisher","unstructured":"Delicaris, J., Schupp, S., \u00c1brah\u00e1m, E., Remke, A.: Maximizing reachability probabilities in rectangular automata with random clocks. In: David, C., Sun, M. (eds.) TASE 2023. LNCS, vol. 13931, pp. 164\u2013182. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-35257-7_10","DOI":"10.1007\/978-3-031-35257-7_10"},{"key":"15_CR14","doi-asserted-by":"publisher","unstructured":"Eisentraut, C., Hermanns, H., Zhang, L.: On probabilistic automata in continuous time. In: Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science, pp. 342\u2013351 (2010). https:\/\/doi.org\/10.1109\/LICS.2010.41","DOI":"10.1109\/LICS.2010.41"},{"issue":"6","key":"15_CR15","doi-asserted-by":"publisher","first-page":"1952","DOI":"10.1137\/S0363012996299302","volume":"35","author":"MK Ghosh","year":"1997","unstructured":"Ghosh, M.K., Arapostathis, A., Marcus, S.I.: Ergodic control of switching diffusions. SIAM J. Control. Optim. 35(6), 1952\u20131988 (1997). https:\/\/doi.org\/10.1137\/S0363012996299302","journal-title":"SIAM J. Control. Optim."},{"key":"15_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/978-3-642-40196-1_5","volume-title":"Quantitative Evaluation of Systems","author":"D Guck","year":"2013","unstructured":"Guck, D., Hatefi, H., Hermanns, H., Katoen, J.-P., Timmer, M.: Modelling, reduction and analysis of Markov automata. In: Joshi, K., Siegle, M., Stoelinga, M., D\u2019Argenio, P.R. (eds.) QEST 2013. LNCS, vol. 8054, pp. 55\u201371. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40196-1_5"},{"issue":"2","key":"15_CR17","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/s10703-012-0167-z","volume":"43","author":"EM Hahn","year":"2013","unstructured":"Hahn, E.M., Hartmanns, A., Hermanns, H., Katoen, J.: A compositional modelling and analysis framework for stochastic hybrid systems. Formal Meth. Syst. Des. 43(2), 191\u2013232 (2013). https:\/\/doi.org\/10.1007\/s10703-012-0167-z","journal-title":"Formal Meth. Syst. Des."},{"issue":"4","key":"15_CR18","doi-asserted-by":"publisher","first-page":"589","DOI":"10.1007\/s10009-021-00633-z","volume":"24","author":"C Hensel","year":"2022","unstructured":"Hensel, C., Junges, S., Katoen, J.P., Quatmann, T., Volk, M.: The probabilistic model checker storm. Int. J. Softw. Tools Technol. Transfer 24(4), 589\u2013610 (2022). https:\/\/doi.org\/10.1007\/s10009-021-00633-z","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"15_CR19","doi-asserted-by":"publisher","unstructured":"Henzinger, T.A.: The theory of hybrid automata. In: Inan, M.K., Kurshan, R.P. (eds.) Verification of Digital and Hybrid Systems, pp. 265\u2013292. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/978-3-642-59615-5_13,https:\/\/doi.org\/10\/dpjwvs","DOI":"10.1007\/978-3-642-59615-5_13"},{"issue":"1","key":"15_CR20","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1006\/jcss.1998.1581","volume":"57","author":"TA Henzinger","year":"1998","unstructured":"Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What\u2019s decidable about hybrid automata? J. Comput. Syst. Sci. 57(1), 94\u2013124 (1998). https:\/\/doi.org\/10.1006\/jcss.1998.1581","journal-title":"J. Comput. Syst. Sci."},{"key":"15_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1007\/978-3-642-24372-1_33","volume-title":"Automated Technology for Verification and Analysis","author":"N Jansen","year":"2011","unstructured":"Jansen, N., \u00c1brah\u00e1m, E., Katelaan, J., Wimmer, R., Katoen, J.-P., Becker, B.: Hierarchical counterexamples for discrete-time Markov Chains. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 443\u2013452. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-24372-1_33"},{"key":"15_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1007\/978-3-642-33386-6_27","volume-title":"Automated Technology for Verification and Analysis","author":"N Jansen","year":"2012","unstructured":"Jansen, N., \u00c1brah\u00e1m, E., Volk, M., Wimmer, R., Katoen, J.-P., Becker, B.: The COMICS tool \u2013 computing minimal counterexamples for DTMCs. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, pp. 349\u2013353. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33386-6_27"},{"key":"15_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/978-3-642-35861-6_9","volume-title":"Formal Aspects of Component Software","author":"N Jansen","year":"2013","unstructured":"Jansen, N., et al.: Symbolic counterexample generation for discrete-time Markov Chains. In: P\u0103s\u0103reanu, C.S., Sala\u00fcn, G. (eds.) FACS 2012. LNCS, vol. 7684, pp. 134\u2013151. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-35861-6_9"},{"key":"15_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"404","DOI":"10.1007\/978-3-319-10696-0_31","volume-title":"Quantitative Evaluation of Systems","author":"N Jansen","year":"2014","unstructured":"Jansen, N., Corzilius, F., Volk, M., Wimmer, R., \u00c1brah\u00e1m, E., Katoen, J.-P., Becker, B.: Accelerating parametric probabilistic verification. In: Norman, G., Sanders, W. (eds.) QEST 2014. LNCS, vol. 8657, pp. 404\u2013420. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-10696-0_31"},{"key":"15_CR25","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1016\/J.SCICO.2014.02.001","volume":"91","author":"N Jansen","year":"2014","unstructured":"Jansen, N., et al.: Symbolic counterexample generation for large discrete-time Markov chains. Sci. Comput. Program. 91, 90\u2013114 (2014). https:\/\/doi.org\/10.1016\/J.SCICO.2014.02.001","journal-title":"Sci. Comput. Program."},{"issue":"1","key":"15_CR26","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/S10703-023-00442-X","volume":"62","author":"S Junges","year":"2024","unstructured":"Junges, S., et al.: Parameter synthesis for Markov models: covering the parameter space. Formal Meth. Syst. Des. 62(1), 181\u2013259 (2024). https:\/\/doi.org\/10.1007\/S10703-023-00442-X","journal-title":"Formal Meth. Syst. Des."},{"key":"15_CR27","doi-asserted-by":"publisher","unstructured":"Klenke, A.: Probability Theory: A Comprehensive Course. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-1-4471-5361-0_1","DOI":"10.1007\/978-1-4471-5361-0_1"},{"issue":"2","key":"15_CR28","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1016\/j.peva.2010.04.002","volume":"68","author":"D Klink","year":"2011","unstructured":"Klink, D., Remke, A., Haverkort, B.R., Katoen, J.P.: Time-bounded reachability in tree-structured QBDs by abstraction. Perform. Eval. 68(2), 105\u2013125 (2011). https:\/\/doi.org\/10.1016\/j.peva.2010.04.002","journal-title":"Perform. Eval."},{"issue":"6","key":"15_CR29","doi-asserted-by":"publisher","first-page":"583","DOI":"10.3166\/ejc.16.583-594","volume":"16","author":"J Lygeros","year":"2010","unstructured":"Lygeros, J., Prandini, M.: Stochastic hybrid systems: a powerful framework for complex, large scale applications. Eur. J. Control. 16(6), 583\u2013594 (2010). https:\/\/doi.org\/10.3166\/ejc.16.583-594","journal-title":"Eur. J. Control."},{"key":"15_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/978-3-319-17524-9_21","volume-title":"NASA Formal Methods","author":"S Pathak","year":"2015","unstructured":"Pathak, S., \u00c1brah\u00e1m, E., Jansen, N., Tacchella, A., Katoen, J.-P.: A greedy approach for the efficient repair of stochastic models. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 295\u2013309. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-17524-9_21"},{"key":"15_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"435","DOI":"10.1007\/978-3-030-85172-9_23","volume-title":"Quantitative Evaluation of Systems","author":"C Pilch","year":"2021","unstructured":"Pilch, C., Schupp, S., Remke, A.: Optimizing reachability probabilities for a restricted class of stochastic hybrid automata via flowpipe-construction. In: Abate, A., Marin, A. (eds.) QEST 2021. LNCS, vol. 12846, pp. 435\u2013456. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-85172-9_23"},{"key":"15_CR32","doi-asserted-by":"publisher","unstructured":"Pola, G., Bujorianu, M., Lygeros, J., Benedetto, M.D.D.: Stochastic hybrid models: An overview. In: Proceedings of the IFAC Conference on Analysis and Design of Hybrid Systems. IFAC Proceedings Volumes, vol.\u00a036, pp. 45\u201350. Elsevier (2003). https:\/\/doi.org\/10.1016\/S1474-6670(17)36405-4","DOI":"10.1016\/S1474-6670(17)36405-4"},{"key":"15_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"435","DOI":"10.1007\/978-3-319-19249-9_27","volume-title":"FM 2015: Formal Methods","author":"T Quatmann","year":"2015","unstructured":"Quatmann, T., et al.: Counterexamples for expected rewards. In: Bj\u00f8rner, N., de Boer, F. (eds.) FM 2015. LNCS, vol. 9109, pp. 435\u2013452. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-19249-9_27"},{"key":"15_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/978-3-540-31980-1_16","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Remke","year":"2005","unstructured":"Remke, A., Haverkort, B.R., Cloth, L.: Model checking infinite-state Markov chains. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 237\u2013252. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-31980-1_16"},{"issue":"1","key":"15_CR35","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1016\/J.TCS.2007.05.007","volume":"382","author":"A Remke","year":"2007","unstructured":"Remke, A., Haverkort, B.R., Cloth, L.: CSL model checking algorithms for QBDs. Theoret. Comput. Sci. 382(1), 24\u201341 (2007). https:\/\/doi.org\/10.1016\/J.TCS.2007.05.007","journal-title":"Theoret. Comput. Sci."},{"key":"15_CR36","doi-asserted-by":"publisher","unstructured":"Shmarov, F., Zuliani, P.: ProbReach: verified probabilistic $$\\delta $$-reachability for stochastic hybrid systems. In: Proc. of the 18th ACM International Conference on Hybrid Systems: Computation and Control. HSCC \u201915, pp. 134\u2013139. ACM (2015). https:\/\/doi.org\/10.1145\/2728606.2728625","DOI":"10.1145\/2728606.2728625"},{"key":"15_CR37","doi-asserted-by":"publisher","DOI":"10.1145\/3607197","author":"C da Silva","year":"2023","unstructured":"da Silva, C., Schupp, S., Remke, A.: Optimizing reachability probabilities for a restricted class of stochastic hybrid automata via flowpipe-construction. Trans. Model. Comput. Simul. (2023). https:\/\/doi.org\/10.1145\/3607197","journal-title":"Trans. Model. Comput. Simul."},{"key":"15_CR38","doi-asserted-by":"publisher","first-page":"921","DOI":"10.1137\/120871456","volume":"12","author":"SEZ Soudjani","year":"2013","unstructured":"Soudjani, S.E.Z., Abate, A.: Adaptive and sequential gridding procedures for the abstraction and verification of stochastic processes. SIAM J. Appl. Dyn. Syst. 12, 921\u2013956 (2013). https:\/\/doi.org\/10.1137\/120871456","journal-title":"SIAM J. Appl. Dyn. Syst."},{"key":"15_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/3-540-45352-0_5","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"J Sproston","year":"2000","unstructured":"Sproston, J.: Decidable model checking of probabilistic hybrid automata. In: Joseph, M. (ed.) FTRTFT 2000. LNCS, vol. 1926, pp. 31\u201345. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-45352-0_5"},{"key":"15_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/978-3-642-32940-1_26","volume-title":"CONCUR 2012 \u2013 Concurrency Theory","author":"M Timmer","year":"2012","unstructured":"Timmer, M., Katoen, J.-P., van de Pol, J., Stoelinga, M.I.A.: Efficient modelling and generation of Markov automata. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol. 7454, pp. 364\u2013379. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-32940-1_26"},{"key":"15_CR41","doi-asserted-by":"publisher","unstructured":"Willemsen, L., Remke, A., \u00c1brah\u00e1m, E.: Comparing two approaches to include stochasticity in hybrid automata. In: Jansen, N., Tribastone, M. (eds.) QEST 2023. LNCS, vol. 14287, pp. 238\u2013254. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-43835-6_17","DOI":"10.1007\/978-3-031-43835-6_17"},{"key":"15_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/978-3-642-28756-5_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Wimmer","year":"2012","unstructured":"Wimmer, R., Jansen, N., \u00c1brah\u00e1m, E., Becker, B., Katoen, J.-P.: Minimal critical subsystems for discrete-time Markov models. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 299\u2013314. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28756-5_21"},{"key":"15_CR43","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1016\/J.TCS.2014.06.020","volume":"549","author":"R Wimmer","year":"2014","unstructured":"Wimmer, R., Jansen, N., \u00c1brah\u00e1m, E., Katoen, J., Becker, B.: Minimal counterexamples for linear-time probabilistic verification. Theoret. Comput. Sci. 549, 61\u2013100 (2014). https:\/\/doi.org\/10.1016\/J.TCS.2014.06.020","journal-title":"Theoret. Comput. Sci."},{"key":"15_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/978-3-642-40196-1_4","volume-title":"Quantitative Evaluation of Systems","author":"R Wimmer","year":"2013","unstructured":"Wimmer, R., Jansen, N., Vorpahl, A., \u00c1brah\u00e1m, E., Katoen, J.-P., Becker, B.: High-level counterexamples for probabilistic automata. In: Joshi, K., Siegle, M., Stoelinga, M., D\u2019Argenio, P.R. (eds.) QEST 2013. LNCS, vol. 8054, pp. 39\u201354. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40196-1_4"},{"key":"15_CR45","doi-asserted-by":"publisher","unstructured":"Wimmer, R., Jansen, N., Vorpahl, A., \u00c1brah\u00e1m, E., Katoen, J., Becker, B.: High-level counterexamples for probabilistic automata. Logical Meth. Comput. Sci. 11(1) (2015). https:\/\/doi.org\/10.2168\/LMCS-11(1:15)2015","DOI":"10.2168\/LMCS-11(1:15)2015"}],"container-title":["Lecture Notes in Computer Science","Principles of Verification: Cycling the Probabilistic Landscape"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-75778-5_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,17]],"date-time":"2024-11-17T13:03:12Z","timestamp":1731848592000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-75778-5_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,11,18]]},"ISBN":["9783031757778","9783031757785"],"references-count":45,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-75778-5_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,11,18]]},"assertion":[{"value":"18 November 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}