{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,18]],"date-time":"2026-04-18T03:15:12Z","timestamp":1776482112422,"version":"3.51.2"},"publisher-location":"Cham","reference-count":223,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031676949","type":"print"},{"value":"9783031676956","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,11,1]],"date-time":"2024-11-01T00:00:00Z","timestamp":1730419200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,11,1]],"date-time":"2024-11-01T00:00:00Z","timestamp":1730419200000},"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-67695-6_4","type":"book-chapter","created":{"date-parts":[[2024,10,31]],"date-time":"2024-10-31T14:03:04Z","timestamp":1730383384000},"page":"90-146","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Tools at\u00a0the\u00a0Frontiers of\u00a0Quantitative Verification"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1286-934X","authenticated-orcid":false,"given":"Roman","family":"Andriushchenko","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7026-228X","authenticated-orcid":false,"given":"Alexander","family":"Bork","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8807-1548","authenticated-orcid":false,"given":"Carlos E.","family":"Budde","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0300-9727","authenticated-orcid":false,"given":"Milan","family":"\u010ce\u0161ka","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4575-1302","authenticated-orcid":false,"given":"Kush","family":"Grover","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9348-7684","authenticated-orcid":false,"given":"Ernst Moritz","family":"Hahn","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3268-8674","authenticated-orcid":false,"given":"Arnd","family":"Hartmanns","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9537-2645","authenticated-orcid":false,"given":"Bryant","family":"Israelsen","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1318-8973","authenticated-orcid":false,"given":"Nils","family":"Jansen","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8269-9489","authenticated-orcid":false,"given":"Joshua","family":"Jeppson","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0978-8466","authenticated-orcid":false,"given":"Sebastian","family":"Junges","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2551-2814","authenticated-orcid":false,"given":"Maximilian A.","family":"K\u00f6hl","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5183-5452","authenticated-orcid":false,"given":"Bettina","family":"K\u00f6nighofer","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8122-2881","authenticated-orcid":false,"given":"Jan","family":"K\u0159et\u00ednsk\u00fd","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1712-2165","authenticated-orcid":false,"given":"Tobias","family":"Meggendorfer","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4137-8862","authenticated-orcid":false,"given":"David","family":"Parker","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0000-6011-9925","authenticated-orcid":false,"given":"Stefan","family":"Pranger","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2843-5511","authenticated-orcid":false,"given":"Tim","family":"Quatmann","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5855-5282","authenticated-orcid":false,"given":"Enno","family":"Ruijters","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4071-3625","authenticated-orcid":false,"given":"Landon","family":"Taylor","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3810-4185","authenticated-orcid":false,"given":"Matthias","family":"Volk","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0163-2152","authenticated-orcid":false,"given":"Maximilian","family":"Weininger","sequence":"additional","affiliation":[]},{"given":"Zhen","family":"Zhang","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,11,1]]},"reference":[{"key":"4_CR1","doi-asserted-by":"publisher","DOI":"10.1016\/j.peva.2021.102207","volume":"148","author":"A Abate","year":"2021","unstructured":"Abate, A., Andriushchenko, R., Ceska, M., Kwiatkowska, M.: Adaptive formal approximations of Markov chains. Perform. Eval. 148, 102207 (2021). https:\/\/doi.org\/10.1016\/j.peva.2021.102207","journal-title":"Perform. Eval."},{"key":"4_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-031-13188-2_1","volume-title":"CAV 2022","author":"C Agarwal","year":"2022","unstructured":"Agarwal, C., Guha, S., Kret\u00ednsk\u00fd, J., Muruganandham, P.: PAC statistical model checking of mean payoff in discrete- and continuous-time MDP. In: Shoham, S., Vizel, Y. (eds.) CAV 2022. LNCS, vol. 13372, pp. 3\u201325. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-13188-2_1"},{"key":"4_CR3","doi-asserted-by":"publisher","unstructured":"Agha, G., Palmskog, K.: A survey of statistical model checking. ACM Trans. Model. Comput. Simul. 28(1), 6:1\u20136:39 (2018). https:\/\/doi.org\/10.1145\/3158668","DOI":"10.1145\/3158668"},{"issue":"2","key":"4_CR4","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183\u2013235 (1994). https:\/\/doi.org\/10.1016\/0304-3975(94)90010-8","journal-title":"Theor. Comput. Sci."},{"issue":"5","key":"4_CR5","doi-asserted-by":"publisher","first-page":"672","DOI":"10.1145\/585265.585270","volume":"49","author":"R Alur","year":"2002","unstructured":"Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. J. ACM 49(5), 672\u2013713 (2002). https:\/\/doi.org\/10.1145\/585265.585270","journal-title":"J. ACM"},{"key":"4_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"552","DOI":"10.1007\/978-3-030-81685-8_26","volume-title":"Computer Aided Verification","author":"\u00c9 Andr\u00e9","year":"2021","unstructured":"Andr\u00e9, \u00c9.: IMITATOR 3: synthesis of timing parameters beyond decidability. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12759, pp. 552\u2013565. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_26"},{"key":"4_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/978-3-030-79379-1_3","volume-title":"Tests and Proofs","author":"\u00c9 Andr\u00e9","year":"2021","unstructured":"Andr\u00e9, \u00c9., Marinho, D., van de Pol, J.: A benchmarks library for extended parametric timed automata. In: Loulergue, F., Wotawa, F. (eds.) TAP 2021. LNCS, vol. 12740, pp. 39\u201350. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-79379-1_3"},{"key":"4_CR8","unstructured":"Andriushchenko, R., Ceska, M., Junges, S., Katoen, J.P.: Inductive synthesis of finite-state controllers for POMDPs. In: Cussens, J., Zhang, K. (eds.) 38th Conference on Uncertainty in Artificial Intelligence (UAI). Proceedings of Machine Learning Research, vol.\u00a0180, pp. 85\u201395. PMLR (2022)"},{"key":"4_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"856","DOI":"10.1007\/978-3-030-81685-8_40","volume-title":"Computer Aided Verification","author":"R Andriushchenko","year":"2021","unstructured":"Andriushchenko, R., \u010ce\u0161ka, M., Junges, S., Katoen, J.-P., Stupinsk\u00fd, \u0160: PAYNT: a tool for inductive synthesis of probabilistic programs. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12759, pp. 856\u2013869. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_40"},{"key":"4_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/978-3-319-99154-2_4","volume-title":"Quantitative Evaluation of Systems","author":"S Arming","year":"2018","unstructured":"Arming, S., Bartocci, E., Chatterjee, K., Katoen, J.-P., Sokolova, A.: Parameter-independent strategies for pMDPs via POMDPs. In: McIver, A., Horvath, A. (eds.) QEST 2018. LNCS, vol. 11024, pp. 53\u201370. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-99154-2_4"},{"key":"4_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"322","DOI":"10.1007\/978-3-030-03421-4_21","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Verification","author":"P Ashok","year":"2018","unstructured":"Ashok, P., Br\u00e1zdil, T., K\u0159et\u00ednsk\u00fd, J., Sl\u00e1me\u010dka, O.: Monte Carlo tree search for verifying reachability in Markov decision processes. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11245, pp. 322\u2013335. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-03421-4_21"},{"key":"4_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/978-3-319-63387-9_10","volume-title":"Computer Aided Verification","author":"P Ashok","year":"2017","unstructured":"Ashok, P., Chatterjee, K., Daca, P., K\u0159et\u00ednsk\u00fd, J., Meggendorfer, T.: Value iteration for long-run average reward in Markov decision processes. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 201\u2013221. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_10"},{"key":"4_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1007\/978-3-031-19992-9_18","volume-title":"ATVA 2022","author":"M Azeem","year":"2022","unstructured":"Azeem, M., Evangelidis, A., Kret\u00ednsk\u00fd, J., Slivinskiy, A., Weininger, M.: Optimistic and topological value iteration for simple stochastic games. In: Bouajjani, A., Hol\u00edk, L., Wu, Z. (eds.) ATVA 2022. LNCS, vol. 13505, pp. 285\u2013302. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-19992-9_18"},{"issue":"1","key":"4_CR14","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1145\/343369.343402","volume":"1","author":"A Aziz","year":"2000","unstructured":"Aziz, A., Sanwal, K., Singhal, V., Brayton, R.K.: Model-checking continous-time Markov chains. ACM Trans. Comput. Log. 1(1), 162\u2013170 (2000). https:\/\/doi.org\/10.1145\/343369.343402","journal-title":"ACM Trans. Comput. Log."},{"key":"4_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"479","DOI":"10.1007\/978-3-319-21690-4_31","volume-title":"Computer Aided Verification","author":"T Babiak","year":"2015","unstructured":"Babiak, T., et al.: The Hanoi omega-automata format. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 479\u2013486. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_31"},{"key":"4_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1007\/978-3-030-85172-9_19","volume-title":"Quantitative Evaluation of Systems","author":"M Backenk\u00f6hler","year":"2021","unstructured":"Backenk\u00f6hler, M., Bortolussi, L., Gro\u00dfmann, G., Wolf, V.: Abstraction-guided truncations for\u00a0stationary distributions of Markov population models. In: Abate, A., Marin, A. (eds.) QEST 2021. LNCS, vol. 12846, pp. 351\u2013371. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-85172-9_19"},{"key":"4_CR17","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-023-00704-3","author":"T Badings","year":"2023","unstructured":"Badings, T., Sim\u00e3o, T.D., Suilen, M., Jansen, N.: Decision-making under uncertainty: beyond probabilities. Int. J. Softw. Tools Technol. Transf. (2023). https:\/\/doi.org\/10.1007\/s10009-023-00704-3","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"5","key":"4_CR18","doi-asserted-by":"publisher","first-page":"803","DOI":"10.1007\/s10009-022-00673-z","volume":"24","author":"TS Badings","year":"2022","unstructured":"Badings, T.S., Cubuktepe, M., Jansen, N., Junges, S., Katoen, J.P., Topcu, U.: Scenario-based verification of uncertain parametric MDPs. Int. J. Softw. Tools Technol. Transf. 24(5), 803\u2013819 (2022). https:\/\/doi.org\/10.1007\/s10009-022-00673-z","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"4_CR19","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1613\/jair.1.14253","volume":"76","author":"TS Badings","year":"2023","unstructured":"Badings, T.S., et al.: Robust control for dynamical systems with non-Gaussian noise via formal abstractions. J. Artif. Intell. Res. 76, 341\u2013391 (2023). https:\/\/doi.org\/10.1613\/jair.1.14253","journal-title":"J. Artif. Intell. Res."},{"key":"4_CR20","doi-asserted-by":"publisher","first-page":"963","DOI":"10.1007\/978-3-319-10575-8_28","volume-title":"Handbook of Model Checking","author":"C Baier","year":"2018","unstructured":"Baier, C., de Alfaro, L., Forejt, V., Kwiatkowska, M.: Model checking probabilistic systems. In: Handbook of Model Checking, pp. 963\u2013999. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_28"},{"issue":"6","key":"4_CR21","doi-asserted-by":"publisher","first-page":"524","DOI":"10.1109\/TSE.2003.1205180","volume":"29","author":"C Baier","year":"2003","unstructured":"Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.P.: Model-checking algorithms for continuous-time Markov chains. IEEE Trans. Software Eng. 29(6), 524\u2013541 (2003). https:\/\/doi.org\/10.1109\/TSE.2003.1205180","journal-title":"IEEE Trans. Software Eng."},{"key":"4_CR22","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2019.104504","volume":"272","author":"C Baier","year":"2020","unstructured":"Baier, C., Hensel, C., Hutschenreiter, L., Junges, S., Katoen, J.P., Klein, J.: Parametric Markov chains: PCTL complexity and fraction-free Gaussian elimination. Inf. Comput. 272, 104504 (2020). https:\/\/doi.org\/10.1016\/j.ic.2019.104504","journal-title":"Inf. Comput."},{"key":"4_CR23","doi-asserted-by":"publisher","unstructured":"Bals, S., Evangelidis, A., Grover, K., Kret\u00ednsk\u00fd, J., Waibel, J.: MULTIGAIN 2.0: MDP controller synthesis for multiple mean-payoff, LTL and steady-state constraints. CoRR abs\/2305.16752 (2023). https:\/\/doi.org\/10.48550\/arXiv.2305.16752","DOI":"10.48550\/arXiv.2305.16752"},{"key":"4_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/978-3-642-28756-5_23","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"B Barbot","year":"2012","unstructured":"Barbot, B., Haddad, S., Picaronny, C.: Coupling and importance sampling for statistical model checking. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 331\u2013346. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28756-5_23"},{"key":"4_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-17502-3_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Bartocci","year":"2019","unstructured":"Bartocci, E., et al.: TOOLympics 2019: an overview of competitions in formal methods. In: Beyer, D., Huisman, M., Kordon, F., Steffen, B. (eds.) TACAS 2019. LNCS, vol. 11429, pp. 3\u201324. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17502-3_1"},{"key":"4_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/978-3-642-19835-9_30","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Bartocci","year":"2011","unstructured":"Bartocci, E., Grosu, R., Katsaros, P., Ramakrishnan, C.R., Smolka, S.A.: Model repair for probabilistic systems. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 326\u2013340. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-19835-9_30"},{"key":"4_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1007\/978-3-662-46681-0_22","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"N Basset","year":"2015","unstructured":"Basset, N., Kwiatkowska, M., Topcu, U., Wiltsche, C.: Strategy synthesis for stochastic games with multiple long-run objectives. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 256\u2013271. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_22"},{"key":"4_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/978-3-030-53291-8_27","volume-title":"Computer Aided Verification","author":"K Batz","year":"2020","unstructured":"Batz, K., Junges, S., Kaminski, B.L., Katoen, J.-P., Matheja, C., Schr\u00f6er, P.: PrIC3: property directed reachability for MDPs. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12225, pp. 512\u2013538. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_27"},{"issue":"5","key":"4_CR29","first-page":"679","volume":"6","author":"R Bellman","year":"1957","unstructured":"Bellman, R.: A Markovian decision process. J. Math. Mech. 6(5), 679\u2013684 (1957)","journal-title":"J. Math. Mech."},{"issue":"10","key":"4_CR30","doi-asserted-by":"publisher","first-page":"812","DOI":"10.1109\/TSE.2006.104","volume":"32","author":"HC Bohnenkamp","year":"2006","unstructured":"Bohnenkamp, H.C., D\u2019Argenio, P.R., Hermanns, H., Katoen, J.P.: MoDeST: a compositional modeling formalism for hard and softly timed systems. IEEE Trans. Software Eng. 32(10), 812\u2013830 (2006). https:\/\/doi.org\/10.1109\/TSE.2006.104","journal-title":"IEEE Trans. Software Eng."},{"key":"4_CR31","doi-asserted-by":"publisher","unstructured":"Bork, A.: Replication package QComp 2023 \u2013 POMDP analysis (2023). https:\/\/doi.org\/10.5281\/zenodo.8215337","DOI":"10.5281\/zenodo.8215337"},{"key":"4_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"288","DOI":"10.1007\/978-3-030-59152-6_16","volume-title":"Automated Technology for Verification and Analysis","author":"A Bork","year":"2020","unstructured":"Bork, A., Junges, S., Katoen, J.-P., Quatmann, T.: Verification of indefinite-horizon POMDPs. In: Hung, D.V., Sokolsky, O. (eds.) ATVA 2020. LNCS, vol. 12302, pp. 288\u2013304. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-59152-6_16"},{"key":"4_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/978-3-030-99527-0_2","volume-title":"TACAS 2022","author":"A Bork","year":"2022","unstructured":"Bork, A., Katoen, J.P., Quatmann, T.: Under-approximating expected total rewards in POMDPs. In: Fisman, D., Rosu, G. (eds.) TACAS 2022. LNCS, vol. 13244, pp. 22\u201340. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99527-0_2"},{"key":"4_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"396","DOI":"10.1007\/978-3-319-89963-3_23","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Bortolussi","year":"2018","unstructured":"Bortolussi, L., Silvetti, S.: Bayesian statistical parameter synthesis for linear temporal properties of\u00a0stochastic models. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10806, pp. 396\u2013413. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89963-3_23"},{"key":"4_CR35","doi-asserted-by":"publisher","unstructured":"Br\u00e1zdil, T., Brozek, V., Chatterjee, K., Forejt, V., Kucera, A.: Two views on multiple mean-payoff objectives in Markov decision processes. Log. Methods Comput. Sci. 10(1) (2014). https:\/\/doi.org\/10.2168\/LMCS-10(1:13)2014","DOI":"10.2168\/LMCS-10(1:13)2014"},{"key":"4_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/978-3-319-11936-6_8","volume-title":"Automated Technology for Verification and Analysis","author":"T Br\u00e1zdil","year":"2014","unstructured":"Br\u00e1zdil, T., et al.: Verification of Markov decision processes using learning algorithms. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 98\u2013114. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-11936-6_8"},{"key":"4_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/978-3-662-46681-0_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T Br\u00e1zdil","year":"2015","unstructured":"Br\u00e1zdil, T., Chatterjee, K., Forejt, V., Ku\u010dera, A.: MultiGain: a controller synthesis tool for MDPs with multiple mean-payoff objectives. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 181\u2013187. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_12"},{"key":"4_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-642-39799-8_7","volume-title":"Computer Aided Verification","author":"L Brim","year":"2013","unstructured":"Brim, L., \u010ce\u0161ka, M., Dra\u017ean, S., \u0160afr\u00e1nek, D.: Exploring parameter space of stochastic biochemical systems using quantitative model checking. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 107\u2013123. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_7"},{"key":"4_CR39","doi-asserted-by":"publisher","unstructured":"Bry, A., Roy, N.: Rapidly-exploring random belief trees for motion planning under uncertainty. In: 2011 IEEE International Conference on Robotics and Automation (ICRA), pp. 723\u2013730. IEEE (2011). https:\/\/doi.org\/10.1109\/ICRA.2011.5980508","DOI":"10.1109\/ICRA.2011.5980508"},{"key":"4_CR40","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1016\/j.scico.2019.01.006","volume":"174","author":"CE Budde","year":"2019","unstructured":"Budde, C.E., D\u2019Argenio, P.R., Hartmanns, A.: Automated compositional importance splitting. Sci. Comput. Program. 174, 90\u2013108 (2019). https:\/\/doi.org\/10.1016\/j.scico.2019.01.006","journal-title":"Sci. Comput. Program."},{"issue":"6","key":"4_CR41","doi-asserted-by":"publisher","first-page":"759","DOI":"10.1007\/s10009-020-00563-2","volume":"22","author":"CE Budde","year":"2020","unstructured":"Budde, C.E., D\u2019Argenio, P.R., Hartmanns, A., Sedwards, S.: An efficient statistical model checker for nondeterminism and rare events. Int. J. Softw. Tools Technol. Transf. 22(6), 759\u2013780 (2020). https:\/\/doi.org\/10.1007\/s10009-020-00563-2","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"4_CR42","doi-asserted-by":"publisher","unstructured":"Budde, C.E., D\u2019Argenio, P.R., Monti, R.E.: Compositional construction of importance functions in fully automated importance splitting. In: Puliafito, A., Trivedi, K.S., Tuffin, B., Scarpa, M., Machida, F., Alonso, J. (eds.) 10th EAI International Conference on Performance Evaluation Methodologies and Tools (VALUETOOLS). ACM (2016). https:\/\/doi.org\/10.4108\/eai.25-10-2016.2266501","DOI":"10.4108\/eai.25-10-2016.2266501"},{"issue":"5","key":"4_CR43","doi-asserted-by":"publisher","first-page":"821","DOI":"10.1007\/s10009-022-00675-x","volume":"24","author":"CE Budde","year":"2022","unstructured":"Budde, C.E., D\u2019Argenio, P.R., Monti, R.E., Stoelinga, M.: Analysis of non-Markovian repairable fault trees through rare event simulation. Int. J. Softw. Tools Technol. Transf. 24(5), 821\u2013841 (2022). https:\/\/doi.org\/10.1007\/s10009-022-00675-x","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"4_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-662-54580-5_9","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"CE Budde","year":"2017","unstructured":"Budde, C.E., Dehnert, C., Hahn, E.M., Hartmanns, A., Junges, S., Turrini, A.: JANI: quantitative model and tool interaction. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10206, pp. 151\u2013168. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54580-5_9"},{"key":"4_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"373","DOI":"10.1007\/978-3-030-72013-1_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"CE Budde","year":"2021","unstructured":"Budde, C.E., Hartmanns, A.: Replicating $$Restart$$ with prolonged retrials: an experimental report. In: TACAS 2021. LNCS, vol. 12652, pp. 373\u2013380. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72013-1_21"},{"key":"4_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1007\/978-3-030-83723-5_15","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Tools and Trends","author":"CE Budde","year":"2021","unstructured":"Budde, C.E., et al.: On correctness, precision, and performance in quantitative verification. In: Margaria, T., Steffen, B. (eds.) ISoLA 2020. LNCS, vol. 12479, pp. 216\u2013241. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-83723-5_15"},{"key":"4_CR47","doi-asserted-by":"publisher","DOI":"10.6084\/m9.figshare.23818395","author":"CE Budde","year":"2023","unstructured":"Budde, C.E., et al.: QComp 2023: formal tools for rare events (experimental reproduction package). Figshare (2023). https:\/\/doi.org\/10.6084\/m9.figshare.23818395","journal-title":"Figshare"},{"key":"4_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-030-59854-9_17","volume-title":"Quantitative Evaluation of Systems","author":"CE Budde","year":"2020","unstructured":"Budde, C.E., Ruijters, E., Stoelinga, M.: The dynamic fault tree rare event simulator. In: Gribaudo, M., Jansen, D.N., Remke, A. (eds.) QEST 2020. LNCS, vol. 12289, pp. 233\u2013238. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-59854-9_17"},{"key":"4_CR49","unstructured":"Buecherl, L., et al.: A collection of biological models for the development of infinite-state stochastic model checking tools. In: 15th International Workshop on Bio-Design Automation (IWBDA), pp. 44\u201347 (2023)"},{"key":"4_CR50","doi-asserted-by":"publisher","unstructured":"Burns, B., Brock, O.: Sampling-based motion planning with sensing uncertainty. In: 2007 IEEE International Conference on Robotics and Automation (ICRA), pp. 3313\u20133318. IEEE (2007). https:\/\/doi.org\/10.1109\/ROBOT.2007.363984","DOI":"10.1109\/ROBOT.2007.363984"},{"key":"4_CR51","doi-asserted-by":"publisher","unstructured":"Butkova, Y., Hartmanns, A., Hermanns, H.: A modest approach to Markov automata. ACM Trans. Model. Comput. Simul. 31(3), 14:1\u201314:34 (2021). https:\/\/doi.org\/10.1145\/3449355","DOI":"10.1145\/3449355"},{"key":"4_CR52","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/978-3-662-54580-5_11","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Y Butkova","year":"2017","unstructured":"Butkova, Y., Wimmer, R., Hermanns, H.: Long-run rewards for Markov automata. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10206, pp. 188\u2013203. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54580-5_11"},{"key":"4_CR53","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-319-45177-0_10","volume-title":"Computational Methods in Systems Biology","author":"L Cardelli","year":"2016","unstructured":"Cardelli, L., Kwiatkowska, M., Laurenti, L.: A stochastic hybrid approximation for chemical kinetics based on the linear noise approximation. In: Bartocci, E., Lio, P., Paoletti, N. (eds.) CMSB 2016. LNCS, vol. 9859, pp. 147\u2013167. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-45177-0_10"},{"key":"4_CR54","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"653","DOI":"10.1007\/978-3-030-53288-8_32","volume-title":"Computer Aided Verification","author":"M \u010ce\u0161ka","year":"2020","unstructured":"\u010ce\u0161ka, M., Chau, C., K\u0159et\u00ednsk\u00fd, J.: SeQuaiA: a scalable tool for semi-quantitative analysis of chemical reaction networks. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12224, pp. 653\u2013666. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53288-8_32"},{"key":"4_CR55","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"475","DOI":"10.1007\/978-3-030-25540-4_28","volume-title":"Computer Aided Verification","author":"M \u010ce\u0161ka","year":"2019","unstructured":"\u010ce\u0161ka, M., K\u0159et\u00ednsk\u00fd, J.: Semi-quantitative abstraction and analysis of chemical reaction networks. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 475\u2013496. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_28"},{"key":"4_CR56","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"559","DOI":"10.1007\/978-3-642-39799-8_37","volume-title":"Computer Aided Verification","author":"K Chatterjee","year":"2013","unstructured":"Chatterjee, K., Gaiser, A., K\u0159et\u00ednsk\u00fd, J.: Automata with generalized Rabin pairs for probabilistic model checking and LTL synthesis. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 559\u2013575. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_37"},{"issue":"2","key":"4_CR57","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1016\/j.jcss.2011.05.002","volume":"78","author":"K Chatterjee","year":"2012","unstructured":"Chatterjee, K., Henzinger, T.A.: A survey of stochastic $$\\omega $$-regular games. J. Comput. Syst. Sci. 78(2), 394\u2013413 (2012). https:\/\/doi.org\/10.1016\/j.jcss.2011.05.002","journal-title":"J. Comput. Syst. Sci."},{"key":"4_CR58","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"665","DOI":"10.1007\/978-3-642-14295-6_57","volume-title":"Computer Aided Verification","author":"K Chatterjee","year":"2010","unstructured":"Chatterjee, K., Henzinger, T.A., Jobstmann, B., Radhakrishna, A.: Gist: a solver for probabilistic games. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 665\u2013669. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_57"},{"key":"4_CR59","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-023-00411-4","author":"K Chatterjee","year":"2023","unstructured":"Chatterjee, K., Katoen, J.P., Mohr, S., Weininger, M., Winkler, T.: Stochastic games with lexicographic objectives. Formal Methods Syst. Des. (2023). https:\/\/doi.org\/10.1007\/s10703-023-00411-4","journal-title":"Formal Methods Syst. Des."},{"key":"4_CR60","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"398","DOI":"10.1007\/978-3-030-53291-8_21","volume-title":"Computer Aided Verification","author":"K Chatterjee","year":"2020","unstructured":"Chatterjee, K., Katoen, J.-P., Weininger, M., Winkler, T.: Stochastic games with lexicographic reachability-safety objectives. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12225, pp. 398\u2013420. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_21"},{"key":"4_CR61","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Kret\u00ednsk\u00e1, Z., Kret\u00ednsk\u00fd, J.: Unifying two views on multiple mean-payoff objectives in Markov decision processes. Log. Methods Comput. Sci. 13(2) (2017). https:\/\/doi.org\/10.23638\/LMCS-13(2:15)2017","DOI":"10.23638\/LMCS-13(2:15)2017"},{"key":"4_CR62","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/11672142_26","volume-title":"STACS 2006","author":"K Chatterjee","year":"2006","unstructured":"Chatterjee, K., Majumdar, R., Henzinger, T.A.: Markov decision processes with multiple objectives. In: Durand, B., Thomas, W. (eds.) STACS 2006. LNCS, vol. 3884, pp. 325\u2013336. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11672142_26"},{"key":"4_CR63","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1007\/978-3-642-28756-5_22","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T Chen","year":"2012","unstructured":"Chen, T., Forejt, V., Kwiatkowska, M., Parker, D., Simaitis, A.: Automatic verification of competitive stochastic systems. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 315\u2013330. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28756-5_22"},{"key":"4_CR64","doi-asserted-by":"publisher","unstructured":"Chen, T., Hahn, E.M., Han, T., Kwiatkowska, M.Z., Qu, H., Zhang, L.: Model repair for Markov decision processes. In: Seventh International Symposium on Theoretical Aspects of Software Engineering (TASE), pp. 85\u201392. IEEE Computer Society (2013). https:\/\/doi.org\/10.1109\/TASE.2013.20","DOI":"10.1109\/TASE.2013.20"},{"key":"4_CR65","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-642-19835-9_22","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C-H Cheng","year":"2011","unstructured":"Cheng, C.-H., Knoll, A., Luttenberger, M., Buckl, C.: GAVS+: an open platform for the research of algorithmic game solving. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 258\u2013261. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-19835-9_22"},{"key":"4_CR66","doi-asserted-by":"publisher","unstructured":"Condon, A.: On algorithms for simple stochastic games. In: Cai, J.Y. (ed.) Advances in Computational Complexity Theory, Proceedings of a DIMACS Workshop. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol.\u00a013, pp. 51\u201371. DIMACS\/AMS (1990). https:\/\/doi.org\/10.1090\/dimacs\/013\/04","DOI":"10.1090\/dimacs\/013\/04"},{"issue":"12","key":"4_CR67","doi-asserted-by":"publisher","first-page":"6333","DOI":"10.1109\/TAC.2021.3133265","volume":"67","author":"M Cubuktepe","year":"2022","unstructured":"Cubuktepe, M., Jansen, N., Junges, S., Katoen, J.P., Topcu, U.: Convex optimization for parameter synthesis in MDPs. IEEE Trans. Autom. Control 67(12), 6333\u20136348 (2022). https:\/\/doi.org\/10.1109\/TAC.2021.3133265","journal-title":"IEEE Trans. Autom. Control"},{"key":"4_CR68","doi-asserted-by":"publisher","unstructured":"Cubuktepe, M., Jansen, N., Junges, S., Marandi, A., Suilen, M., Topcu, U.: Robust finite-state controllers for uncertain POMDPs. In: 35th AAAI Conference on Artificial Intelligence (AAAI), pp. 11792\u201311800. AAAI Press (2021). https:\/\/doi.org\/10.1609\/aaai.v35i13.17401","DOI":"10.1609\/aaai.v35i13.17401"},{"key":"4_CR69","doi-asserted-by":"publisher","unstructured":"Daigle, Bernie\u00a0J., J., Roh, M.K., Gillespie, D.T., Petzold, L.R.: Automated estimation of rare event probabilities in biochemical systems. J. Chem. Phys. 134(4) (2011). https:\/\/doi.org\/10.1063\/1.3522769","DOI":"10.1063\/1.3522769"},{"key":"4_CR70","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-319-33693-0_7","volume-title":"Integrated Formal Methods","author":"PR D\u2019Argenio","year":"2016","unstructured":"D\u2019Argenio, P.R., Hartmanns, A., Legay, A., Sedwards, S.: Statistical approximation of optimal schedulers for probabilistic timed automata. In: \u00c1brah\u00e1m, E., Huisman, M. (eds.) IFM 2016. LNCS, vol. 9681, pp. 99\u2013114. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-33693-0_7"},{"key":"4_CR71","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1007\/978-3-030-02508-3_8","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2018","author":"PR D\u2019Argenio","year":"2018","unstructured":"D\u2019Argenio, P.R., Monti, R.E.: Input\/Output stochastic automata with urgency: confluence and weak determinism. In: Fischer, B., Uustalu, T. (eds.) ICTAC 2018. LNCS, vol. 11187, pp. 132\u2013152. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-02508-3_8"},{"key":"4_CR72","doi-asserted-by":"publisher","unstructured":"David, A., Jensen, P.G., Larsen, K.G., Mikucionis, M., Taankvist, J.H.: Uppaal Stratego. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol.\u00a09035, pp. 206\u2013211. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_16","DOI":"10.1007\/978-3-662-46681-0_16"},{"key":"4_CR73","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1007\/978-3-540-31862-0_21","volume-title":"Theoretical Aspects of Computing - ICTAC 2004","author":"C Daws","year":"2005","unstructured":"Daws, C.: Symbolic and parametric model checking of discrete-time Markov chains. In: Liu, Z., Araki, K. (eds.) ICTAC 2004. LNCS, vol. 3407, pp. 280\u2013294. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-31862-0_21"},{"key":"4_CR74","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1007\/978-3-030-45190-5_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"F Delgrange","year":"2020","unstructured":"Delgrange, F., Katoen, J.-P., Quatmann, T., Randour, M.: Simple strategies in multi-objective MDPs. In: TACAS 2020. LNCS, vol. 12078, pp. 346\u2013364. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-45190-5_19"},{"issue":"6","key":"4_CR75","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1007\/s10009-016-0433-2","volume":"19","author":"T van Dijk","year":"2017","unstructured":"van Dijk, T., van de Pol, J.: Sylvan: multi-core framework for decision diagrams. Int. J. Softw. Tools Technol. Transf. 19(6), 675\u2013696 (2017). https:\/\/doi.org\/10.1007\/s10009-016-0433-2","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"4_CR76","doi-asserted-by":"publisher","unstructured":"Donovan, R.M., Sedgewick, A.J., Faeder, J.R., Zuckerman, D.M.: Efficient stochastic simulation of chemical kinetics networks using a weighted ensemble of trajectories. J. Chem. Phys. 139(11) (2013). https:\/\/doi.org\/10.1063\/1.4821167","DOI":"10.1063\/1.4821167"},{"key":"4_CR77","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-031-13188-2_9","volume-title":"CAV 2022","author":"A Duret-Lutz","year":"2022","unstructured":"Duret-Lutz, A., et al.: From Spot 2.0 to Spot 2.10: What\u2019s new? In: Shoham, S., Vizel, Y. (eds.) CAV 2022. LNCS, vol. 13372, pp. 174\u2013187. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-13188-2_9"},{"key":"4_CR78","unstructured":"Egorov, M., Sunberg, Z.N., Balaban, E., Wheeler, T.A., Gupta, J.K., Kochenderfer, M.J.: POMDPs.jl: a framework for sequential decision making under uncertainty. J. Mach. Learn. Res. 18, 26:1\u201326:5 (2017)"},{"key":"4_CR79","doi-asserted-by":"publisher","unstructured":"Eisentraut, C., Hermanns, H., Zhang, L.: On probabilistic automata in continuous time. In: 25th Annual IEEE Symposium on Logic in Computer Science (LICS), pp. 342\u2013351. IEEE Computer Society (2010). https:\/\/doi.org\/10.1109\/LICS.2010.41","DOI":"10.1109\/LICS.2010.41"},{"key":"4_CR80","doi-asserted-by":"publisher","unstructured":"Eisentraut, J., Kelmendi, E., Kret\u00ednsk\u00fd, J., Weininger, M.: Value iteration for simple stochastic games: stopping criterion and learning algorithm. Inf. Comput. 285(Part), 104886 (2022). https:\/\/doi.org\/10.1016\/j.ic.2022.104886","DOI":"10.1016\/j.ic.2022.104886"},{"key":"4_CR81","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"192","DOI":"10.1007\/978-3-319-08867-9_13","volume-title":"Computer Aided Verification","author":"J Esparza","year":"2014","unstructured":"Esparza, J., K\u0159et\u00ednsk\u00fd, J.: From LTL to deterministic automata: a safraless compositional approach. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 192\u2013208. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_13"},{"key":"4_CR82","doi-asserted-by":"publisher","unstructured":"Esparza, J., Kret\u00ednsk\u00fd, J., Sickert, S.: A unified translation of linear temporal logic to $$\\omega $$-automata. J. ACM 67(6), 33:1\u201333:61 (2020). https:\/\/doi.org\/10.1145\/3417995","DOI":"10.1145\/3417995"},{"key":"4_CR83","doi-asserted-by":"publisher","unstructured":"Etessami, K., Kwiatkowska, M.Z., Vardi, M.Y., Yannakakis, M.: Multi-objective model checking of Markov decision processes. Log. Methods Comput. Sci. 4(4) (2008). https:\/\/doi.org\/10.2168\/LMCS-4(4:8)2008","DOI":"10.2168\/LMCS-4(4:8)2008"},{"key":"4_CR84","doi-asserted-by":"publisher","unstructured":"Fedyukovich, G., Mover, S.: TACAS 23 artifact evaluation VM \u2013 Ubuntu 22.04 LTS (2022). https:\/\/doi.org\/10.5281\/zenodo.7113223","DOI":"10.5281\/zenodo.7113223"},{"issue":"1","key":"4_CR85","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1109\/TSE.2015.2421318","volume":"42","author":"A Filieri","year":"2016","unstructured":"Filieri, A., Tamburrelli, G., Ghezzi, C.: Supporting self-adaptation via quantitative verification and sensitivity analysis at run time. IEEE Trans. Software Eng. 42(1), 75\u201399 (2016). https:\/\/doi.org\/10.1109\/TSE.2015.2421318","journal-title":"IEEE Trans. Software Eng."},{"issue":"9","key":"4_CR86","doi-asserted-by":"publisher","first-page":"2324","DOI":"10.1021\/acssynbio.0c00055","volume":"9","author":"P Fontanarrosa","year":"2020","unstructured":"Fontanarrosa, P., Doosthosseini, H., Borujeni, A.E., Dorfan, Y., Voigt, C.A., Myers, C.: Genetic circuit dynamics: hazard and glitch analysis. ACS Synth. Biol. 9(9), 2324\u20132338 (2020). https:\/\/doi.org\/10.1021\/acssynbio.0c00055","journal-title":"ACS Synth. Biol."},{"key":"4_CR87","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/978-3-642-19835-9_11","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"V Forejt","year":"2011","unstructured":"Forejt, V., Kwiatkowska, M., Norman, G., Parker, D., Qu, H.: Quantitative multi-objective verification for probabilistic systems. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 112\u2013127. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-19835-9_11"},{"key":"4_CR88","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/978-3-642-33386-6_25","volume-title":"Automated Technology for Verification and Analysis","author":"V Forejt","year":"2012","unstructured":"Forejt, V., Kwiatkowska, M., Parker, D.: Pareto curves for probabilistic model checking. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, pp. 317\u2013332. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33386-6_25"},{"key":"4_CR89","doi-asserted-by":"publisher","unstructured":"Fr\u00e4nzle, M., Hahn, E.M., Hermanns, H., Wolovick, N., Zhang, L.: Measurability and safety verification for stochastic hybrid systems. In: Caccamo, M., Frazzoli, E., Grosu, R. (eds.) 14th ACM International Conference on Hybrid Systems: Computation and Control (HSCC), pp. 43\u201352. ACM (2011). https:\/\/doi.org\/10.1145\/1967701.1967710","DOI":"10.1145\/1967701.1967710"},{"key":"4_CR90","unstructured":"Frehse, G., Althoff, M. (eds.): 4th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH), EPiC Series in Computing, vol.\u00a048. EasyChair (2017). https:\/\/easychair.org\/publications\/volume\/ARCH17"},{"key":"4_CR91","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-030-94583-1_5","volume-title":"VMCAI 2022","author":"C Fu","year":"2022","unstructured":"Fu, C., Hahn, E.M., Li, Y., Schewe, S., Sun, M., Turrini, A., Zhang, L.: EPMC gets knowledge in multi-agent systems. In: Finkbeiner, B., Wies, T. (eds.) VMCAI 2022. LNCS, vol. 13182, pp. 93\u2013107. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-94583-1_5"},{"key":"4_CR92","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"300","DOI":"10.1007\/978-3-030-01090-4_18","volume-title":"Automated Technology for Verification and Analysis","author":"P Gainer","year":"2018","unstructured":"Gainer, P., Hahn, E.M., Schewe, S.: Accelerated model checking of parametric Markov chains. In: Lahiri, S.K., Wang, C. (eds.) ATVA 2018. LNCS, vol. 11138, pp. 300\u2013316. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-01090-4_18"},{"issue":"25","key":"4_CR93","doi-asserted-by":"publisher","first-page":"2340","DOI":"10.1021\/j100540a008","volume":"81","author":"DT Gillespie","year":"1977","unstructured":"Gillespie, D.T.: Exact stochastic simulation of coupled chemical reactions. J. Phys. Chem. 81(25), 2340\u20132361 (1977). https:\/\/doi.org\/10.1021\/j100540a008","journal-title":"J. Phys. Chem."},{"key":"4_CR94","unstructured":"Goldberg, F., Vesely, W.: Fault Tree Handbook. NUREG-0492, Systems and Reliability Research, Office of Nuclear Regulatory Research, U.S. Nuclear Regulatory Commission (1981)"},{"key":"4_CR95","doi-asserted-by":"publisher","unstructured":"Goutsias, J.: Quasiequilibrium approximation of fast reaction kinetics in stochastic biochemical systems. J. Chem. Phys. 122(18) (2005). https:\/\/doi.org\/10.1063\/1.1889434","DOI":"10.1063\/1.1889434"},{"issue":"1","key":"4_CR96","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1287\/moor.2022.1259","volume":"48","author":"V Goyal","year":"2023","unstructured":"Goyal, V., Grand-Cl\u00e9ment, J.: Robust Markov decision processes: beyond rectangularity. Math. Oper. Res. 48(1), 203\u2013226 (2023). https:\/\/doi.org\/10.1287\/moor.2022.1259","journal-title":"Math. Oper. Res."},{"key":"4_CR97","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"430","DOI":"10.1007\/978-3-031-13188-2_21","volume-title":"CAV 2022","author":"TP Gros","year":"2022","unstructured":"Gros, T.P., Hermanns, H., Hoffmann, J., Klauck, M., K\u00f6hl, M.A., Wolf, V.: MoGym: using formal models for training and verifying decision-making agents. In: Shoham, S., Vizel, Y. (eds.) CAV 2022. LNCS, vol. 13372, pp. 430\u2013443. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-13188-2_21"},{"key":"4_CR98","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1007\/978-3-030-50086-3_6","volume-title":"Formal Techniques for Distributed Objects, Components, and Systems","author":"TP Gros","year":"2020","unstructured":"Gros, T.P., Hermanns, H., Hoffmann, J., Klauck, M., Steinmetz, M.: Deep statistical model checking. In: Gotsman, A., Sokolova, A. (eds.) FORTE 2020. LNCS, vol. 12136, pp. 96\u2013114. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-50086-3_6"},{"key":"4_CR99","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-031-21213-0_3","volume-title":"SETTA 2022","author":"D Gross","year":"2022","unstructured":"Gross, D., Jansen, N., Junges, S., P\u00e9rez, G.A.: COOL-MC: a comprehensive tool for reinforcement learning and model checking. In: Dong, W., Talpin, J.P. (eds.) SETTA 2022. LNCS, vol. 13649, pp. 41\u201349. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-21213-0_3"},{"key":"4_CR100","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.8219191","author":"K Grover","year":"2023","unstructured":"Grover, K.: QComp LRA results (2023). https:\/\/doi.org\/10.5281\/zenodo.8219191","journal-title":"QComp LRA results"},{"key":"4_CR101","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-319-11936-6_13","volume-title":"Automated Technology for Verification and Analysis","author":"D Guck","year":"2014","unstructured":"Guck, D., Timmer, M., Hatefi, H., Ruijters, E., Stoelinga, M.: Modelling and analysis of Markov reward automata. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 168\u2013184. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-11936-6_13"},{"key":"4_CR102","doi-asserted-by":"publisher","unstructured":"Hahn, E.M., Hartmanns, A.: Symblicit exploration and elimination for probabilistic model checking. In: Hung, C.C., Hong, J., Bechini, A., Song, E. (eds.) 36th ACM\/SIGAPP Symposium on Applied Computing (SAC), pp. 1798\u20131806. ACM (2021). https:\/\/doi.org\/10.1145\/3412841.3442052","DOI":"10.1145\/3412841.3442052"},{"key":"4_CR103","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-3-030-17502-3_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"EM Hahn","year":"2019","unstructured":"Hahn, E.M., et al.: The 2019 comparison of tools for the analysis of quantitative formal models. In: Beyer, D., Huisman, M., Kordon, F., Steffen, B. (eds.) TACAS 2019. LNCS, vol. 11429, pp. 69\u201392. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17502-3_5"},{"key":"4_CR104","doi-asserted-by":"publisher","unstructured":"Hahn, E.M., Hartmanns, A., Hermanns, H.: Reachability and reward checking for stochastic timed automata. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 70 (2014). https:\/\/doi.org\/10.14279\/tuj.eceasst.70.968","DOI":"10.14279\/tuj.eceasst.70.968"},{"issue":"2","key":"4_CR105","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.P.: A compositional modelling and analysis framework for stochastic hybrid systems. Formal Methods Syst. Des. 43(2), 191\u2013232 (2013). https:\/\/doi.org\/10.1007\/s10703-012-0167-z","journal-title":"Formal Methods Syst. Des."},{"key":"4_CR106","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"641","DOI":"10.1007\/978-3-642-02658-4_49","volume-title":"Computer Aided Verification","author":"EM Hahn","year":"2009","unstructured":"Hahn, E.M., Hermanns, H., Wachter, B., Zhang, L.: INFAMY: an infinite-state Markov model checker. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 641\u2013647. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_49"},{"issue":"1","key":"4_CR107","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s10009-010-0146-x","volume":"13","author":"EM Hahn","year":"2011","unstructured":"Hahn, E.M., Hermanns, H., Zhang, L.: Probabilistic reachability for parametric Markov models. Int. J. Softw. Tools Technol. Transf. 13(1), 3\u201319 (2011). https:\/\/doi.org\/10.1007\/s10009-010-0146-x","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"4_CR108","doi-asserted-by":"publisher","unstructured":"Hahn, E.M., Li, G., Schewe, S., Turrini, A., Zhang, L.: Lazy probabilistic model checking without determinisation. In: Aceto, L., de\u00a0Frutos-Escrig, D. (eds.) 26th International Conference on Concurrency Theory (CONCUR). LIPIcs, vol.\u00a042, pp. 354\u2013367. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik (2015). https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2015.354","DOI":"10.4230\/LIPIcs.CONCUR.2015.354"},{"key":"4_CR109","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1007\/978-3-319-06410-9_22","volume-title":"FM 2014: Formal Methods","author":"EM Hahn","year":"2014","unstructured":"Hahn, E.M., Li, Y., Schewe, S., Turrini, A., Zhang, L.: iscasMc: a web-based probabilistic model checker. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 312\u2013317. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-06410-9_22"},{"key":"4_CR110","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1007\/978-3-030-45190-5_17","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"EM Hahn","year":"2020","unstructured":"Hahn, E.M., Perez, M., Schewe, S., Somenzi, F., Trivedi, A., Wojtczak, D.: Good-for-MDPs automata for probabilistic analysis and reinforcement learning. In: TACAS 2020. LNCS, vol. 12078, pp. 306\u2013323. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-45190-5_17"},{"key":"4_CR111","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-030-99527-0_3","volume-title":"TACAS 2022","author":"A Hartmanns","year":"2022","unstructured":"Hartmanns, A.: Correct probabilistic model checking with floating-point arithmetic. In: Fisman, D., Rosu, G. (eds.) TACAS 2022. LNCS, vol. 13244, pp. 41\u201359. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99527-0_3"},{"key":"4_CR112","doi-asserted-by":"publisher","unstructured":"Hartmanns, A., Hermanns, H.: A Modest approach to checking probabilistic timed automata. In: 6th International Conference on the Quantitative Evaluation of Systems (QEST), pp. 187\u2013196. IEEE Computer Society (2009). https:\/\/doi.org\/10.1109\/QEST.2009.41","DOI":"10.1109\/QEST.2009.41"},{"key":"4_CR113","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"593","DOI":"10.1007\/978-3-642-54862-8_51","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Hartmanns","year":"2014","unstructured":"Hartmanns, A., Hermanns, H.: The modest toolset: an integrated environment for quantitative modelling and verification. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 593\u2013598. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_51"},{"key":"4_CR114","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-319-24953-7_10","volume-title":"Automated Technology for Verification and Analysis","author":"A Hartmanns","year":"2015","unstructured":"Hartmanns, A., Hermanns, H.: Explicit model checking of very large MDP using partitioning and secondary storage. In: Finkbeiner, B., Pu, G., Zhang, L. (eds.) ATVA 2015. LNCS, vol. 9364, pp. 131\u2013147. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-24953-7_10"},{"issue":"7","key":"4_CR115","doi-asserted-by":"publisher","first-page":"1483","DOI":"10.1007\/s10817-020-09574-9","volume":"64","author":"A Hartmanns","year":"2020","unstructured":"Hartmanns, A., Junges, S., Katoen, J.P., Quatmann, T.: Multi-cost bounded tradeoff analysis in MDP. J. Autom. Reason. 64(7), 1483\u20131522 (2020). https:\/\/doi.org\/10.1007\/s10817-020-09574-9","journal-title":"J. Autom. Reason."},{"key":"4_CR116","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"469","DOI":"10.1007\/978-3-031-30823-9_24","volume-title":"TACAS 2023","author":"A Hartmanns","year":"2023","unstructured":"Hartmanns, A., Junges, S., Quatmann, T., Weininger, M.: A practitioner\u2019s guide to MDP model checking algorithms. In: Sankaranarayanan, S., Sharygina, N. (eds.) TACAS 2023. LNCS, vol. 13993, pp. 469\u2013488. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-30823-9_24"},{"key":"4_CR117","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"488","DOI":"10.1007\/978-3-030-53291-8_26","volume-title":"Computer Aided Verification","author":"A Hartmanns","year":"2020","unstructured":"Hartmanns, A., Kaminski, B.L.: Optimistic value iteration. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12225, pp. 488\u2013511. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_26"},{"key":"4_CR118","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/978-3-030-85172-9_3","volume-title":"Quantitative Evaluation of Systems","author":"A Hartmanns","year":"2021","unstructured":"Hartmanns, A., Katoen, J.-P., Kohlen, B., Spel, J.: Tweaking the odds in probabilistic timed automata. In: Abate, A., Marin, A. (eds.) QEST 2021. LNCS, vol. 12846, pp. 39\u201358. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-85172-9_3"},{"key":"4_CR119","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"344","DOI":"10.1007\/978-3-030-17462-0_20","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Hartmanns","year":"2019","unstructured":"Hartmanns, A., Klauck, M., Parker, D., Quatmann, T., Ruijters, E.: The quantitative verification benchmark set. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11427, pp. 344\u2013350. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17462-0_20"},{"key":"4_CR120","doi-asserted-by":"publisher","unstructured":"Hartmanns, A., Sedwards, S., D\u2019Argenio, P.R.: Efficient simulation-based verification of probabilistic timed automata. In: 2017 Winter Simulation Conference (WSC), pp. 1419\u20131430. IEEE (2017). https:\/\/doi.org\/10.1109\/WSC.2017.8247885","DOI":"10.1109\/WSC.2017.8247885"},{"issue":"3","key":"4_CR121","doi-asserted-by":"publisher","first-page":"687","DOI":"10.1007\/s00285-013-0711-5","volume":"69","author":"J Hasenauer","year":"2013","unstructured":"Hasenauer, J., Wolf, V., Kazeroonian, A., Theis, F.J.: Method of conditional moments (MCM) for the chemical master equation. J. Math. Biol. 69(3), 687\u2013735 (2013). https:\/\/doi.org\/10.1007\/s00285-013-0711-5","journal-title":"J. Math. Biol."},{"key":"4_CR122","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/978-3-030-94583-1_7","volume-title":"VMCAI 2022","author":"L Heck","year":"2022","unstructured":"Heck, L., Spel, J., Junges, S., Moerman, J., Katoen, J.P.: Gradient-descent for randomized controllers under partial observability. In: Finkbeiner, B., Wies, T. (eds.) VMCAI 2022. LNCS, vol. 13182, pp. 127\u2013150. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-94583-1_7"},{"key":"4_CR123","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1007\/BFb0013853","volume-title":"Performance Evaluation of Computer and Communication Systems","author":"P Heidelberger","year":"1993","unstructured":"Heidelberger, P.: Fast simulation of rare events in queueing and reliability models. In: Donatiello, L., Nelson, R. (eds.) Performance\/SIGMETRICS -1993. LNCS, vol. 729, pp. 165\u2013202. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/BFb0013853"},{"key":"4_CR124","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-031-15034-0_3","volume-title":"CMSB 2022","author":"M Helfrich","year":"2022","unstructured":"Helfrich, M., Ceska, M., Kret\u00ednsk\u00fd, J., Marticek, S.: Abstraction-based segmental simulation of chemical reaction networks. In: Petre, I., Paun, A. (eds.) CMSB 2022. LNCS, vol. 13447, pp. 41\u201360. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-15034-0_3"},{"issue":"4","key":"4_CR125","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. Transf. 24(4), 589\u2013610 (2022). https:\/\/doi.org\/10.1007\/s10009-021-00633-z","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"4_CR126","doi-asserted-by":"publisher","unstructured":"Henzinger, T.A., Mikeev, L., Mateescu, M., Wolf, V.: Hybrid numerical solution of the chemical master equation. In: Quaglia, P. (ed.) 8th International Conference on Computational Methods in Systems Biology (CMSB), pp. 55\u201365. ACM (2010). https:\/\/doi.org\/10.1145\/1839764.1839772","DOI":"10.1145\/1839764.1839772"},{"key":"4_CR127","unstructured":"Hermanns, H., Meyer-Kayser, J., Siegle, M.: Multi terminal binary decision diagrams to represent and analyse continuous time Markov chains. In: Plateau, B., Stewart, W., Silva, M. (eds.) 3rd International Workshop on Numerical Solution of Markov Chains (NSMC), pp. 188\u2013207. Prensas Universitarias de Zaragoza (1999)"},{"key":"4_CR128","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"577","DOI":"10.1007\/978-3-030-81688-9_27","volume-title":"Computer Aided Verification","author":"S Holtzen","year":"2021","unstructured":"Holtzen, S., Junges, S., Vazquez-Chanlatte, M., Millstein, T., Seshia, S.A., Van den Broeck, G.: Model checking finite-horizon Markov chains with probabilistic inference. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12760, pp. 577\u2013601. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_27"},{"key":"4_CR129","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/978-3-031-32157-3_5","volume-title":"SPIN 2023","author":"B Israelsen","year":"2023","unstructured":"Israelsen, B., Taylor, L., Zhang, Z.: Efficient trace generation for rare-event analysis in chemical reaction networks. In: Caltais, G., Schilling, C. (eds.) SPIN 2023. LNCS, vol. 13872, pp. 83\u2013102. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-32157-3_5"},{"issue":"8\u20139","key":"4_CR130","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1016\/j.artint.2007.03.004","volume":"171","author":"H Itoh","year":"2007","unstructured":"Itoh, H., Nakamura, K.: Partially observable Markov decision processes with imprecise parameters. Artif. Intell. 171(8\u20139), 453\u2013490 (2007). https:\/\/doi.org\/10.1016\/j.artint.2007.03.004","journal-title":"Artif. Intell."},{"key":"4_CR131","doi-asserted-by":"publisher","first-page":"518","DOI":"10.1287\/opre.5.4.518","volume":"5","author":"JR Jackson","year":"1957","unstructured":"Jackson, J.R.: Networks of waiting lines. Oper. Res. 5, 518\u2013521 (1957)","journal-title":"Oper. Res."},{"key":"4_CR132","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"407","DOI":"10.1007\/978-3-031-22337-2_20","volume-title":"Principles of Systems Design","author":"N Jansen","year":"2022","unstructured":"Jansen, N., Junges, S., Katoen, J.P.: Parameter synthesis in Markov models: a gentle survey. In: Raskin, J.F., Chatterjee, K., Doyen, L., Majumdar, R. (eds.) Principles of Systems Design. LNCS, vol. 13660, pp. 407\u2013437. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-22337-2_20"},{"key":"4_CR133","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.tcs.2016.08.009","volume":"649","author":"C J\u00e9gourel","year":"2016","unstructured":"J\u00e9gourel, C., Legay, A., Sedwards, S.: Command-based importance sampling for statistical model checking. Theor. Comput. Sci. 649, 1\u201324 (2016). https:\/\/doi.org\/10.1016\/j.tcs.2016.08.009","journal-title":"Theor. Comput. Sci."},{"key":"4_CR134","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1007\/978-3-031-43835-6_7","volume-title":"QEST 2023","author":"J Jeppson","year":"2023","unstructured":"Jeppson, J., et al.: STAMINA in C++: modernizing an infinite-state probabilistic model checker. In: Jansen, N., Tribastone, M. (eds.) QEST 2023. LNCS, vol. 14287, pp. 101\u2013109. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-43835-6_7"},{"issue":"3","key":"4_CR135","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1007\/s11334-022-00445-7","volume":"18","author":"T John","year":"2022","unstructured":"John, T., Jantsch, S., Baier, C., Kl\u00fcppelholz, S.: From Emerson-Lei automata to deterministic, limit-deterministic or good-for-MDP automata. Innov. Syst. Softw. Eng. 18(3), 385\u2013403 (2022). https:\/\/doi.org\/10.1007\/s11334-022-00445-7","journal-title":"Innov. Syst. Softw. Eng."},{"key":"4_CR136","unstructured":"Junges, S.: Parameter synthesis in Markov models. Ph.D. thesis, RWTH Aachen University (2020). https:\/\/publications.rwth-aachen.de\/record\/783179"},{"key":"4_CR137","doi-asserted-by":"publisher","unstructured":"Junges, S.: sjunges\/parametric-Markov-models: 0.2 (2023). https:\/\/doi.org\/10.5281\/zenodo.10646479","DOI":"10.5281\/zenodo.10646479"},{"key":"4_CR138","doi-asserted-by":"publisher","unstructured":"Junges, S., et al.: Parameter synthesis for Markov models. CoRR abs\/1903.07993 (2019). https:\/\/doi.org\/10.48550\/arXiv.1903.07993","DOI":"10.48550\/arXiv.1903.07993"},{"key":"4_CR139","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"602","DOI":"10.1007\/978-3-030-81688-9_28","volume-title":"Computer Aided Verification","author":"S Junges","year":"2021","unstructured":"Junges, S., Jansen, N., Seshia, S.A.: Enforcing almost-sure reachability in POMDPs. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12760, pp. 602\u2013625. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_28"},{"key":"4_CR140","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"102","DOI":"10.1007\/978-3-031-13185-1_6","volume-title":"CAV 2022","author":"S Junges","year":"2022","unstructured":"Junges, S., Spaan, M.T.J.: Abstraction-refinement for hierarchical probabilistic models. In: Shoham, S., Vizel, Y. (eds.) CAV 2022. LNCS, vol. 13371, pp. 102\u2013123. Springer, Cham (2022)"},{"key":"4_CR141","first-page":"27","volume":"12","author":"H Kahn","year":"1951","unstructured":"Kahn, H., Harris, T.E.: Estimation of particle transmission by random sampling. Natl. Bureau Stand. Appl. Math. Lett. 12, 27\u201330 (1951)","journal-title":"Natl. Bureau Stand. Appl. Math. Lett."},{"key":"4_CR142","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1613\/jair.1.11595","volume":"68","author":"M Klauck","year":"2020","unstructured":"Klauck, M., Steinmetz, M., Hoffmann, J., Hermanns, H.: Bridging the gap between probabilistic model checking and probabilistic planning: survey, compilations, and empirical comparison. J. Artif. Intell. Res. 68, 247\u2013310 (2020). https:\/\/doi.org\/10.1613\/jair.1.11595","journal-title":"J. Artif. Intell. Res."},{"key":"4_CR143","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/10187.001.0001","volume-title":"Decision Making Under Uncertainty: Theory and Application","author":"MJ Kochenderfer","year":"2015","unstructured":"Kochenderfer, M.J.: Decision Making Under Uncertainty: Theory and Application. MIT Press, Cambridge (2015)"},{"key":"4_CR144","doi-asserted-by":"publisher","unstructured":"K\u00f6hl, M.A.: QComp 2023: State space exploration artifact (2024). https:\/\/doi.org\/10.5281\/zenodo.10626177","DOI":"10.5281\/zenodo.10626177"},{"key":"4_CR145","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/978-3-030-72013-1_23","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"MA K\u00f6hl","year":"2021","unstructured":"K\u00f6hl, M.A., Klauck, M., Hermanns, H.: Momba: JANI meets Python. In: TACAS 2021. LNCS, vol. 12652, pp. 389\u2013398. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72013-1_23"},{"key":"4_CR146","doi-asserted-by":"publisher","unstructured":"Kret\u00ednsk\u00fd, J.: LTL-constrained steady-state policy synthesis. In: Zhou, Z.H. (ed.) 30th International Joint Conference on Artificial Intelligence (IJCAI), pp. 4104\u20134111. ijcai.org (2021). https:\/\/doi.org\/10.24963\/ijcai.2021\/565","DOI":"10.24963\/ijcai.2021\/565"},{"key":"4_CR147","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1007\/978-3-642-31424-7_7","volume-title":"Computer Aided Verification","author":"J K\u0159et\u00ednsk\u00fd","year":"2012","unstructured":"K\u0159et\u00ednsk\u00fd, J., Esparza, J.: Deterministic automata for the (F,G)-fragment of LTL. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 7\u201322. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_7"},{"key":"4_CR148","doi-asserted-by":"publisher","unstructured":"Kret\u00ednsk\u00fd, J., Meggendorfer, T.: Of cores: a partial-exploration framework for Markov decision processes. Log. Methods Comput. Sci. 16(4) (2020). https:\/\/doi.org\/10.23638\/LMCS-16(4:3)2020","DOI":"10.23638\/LMCS-16(4:3)2020"},{"key":"4_CR149","doi-asserted-by":"publisher","unstructured":"Kret\u00ednsk\u00fd, J., Meggendorfer, T., Sickert, S.: LTL Store: Repository of LTL formulae from literature and case studies. CoRR abs\/1807.03296 (2018). https:\/\/doi.org\/10.48550\/arXiv.1807.03296","DOI":"10.48550\/arXiv.1807.03296"},{"key":"4_CR150","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"543","DOI":"10.1007\/978-3-030-01090-4_34","volume-title":"Automated Technology for Verification and Analysis","author":"J K\u0159et\u00ednsk\u00fd","year":"2018","unstructured":"K\u0159et\u00ednsk\u00fd, J., Meggendorfer, T., Sickert, S.: Owl: a library for $$\\omega $$-words, automata, and LTL. In: Lahiri, S.K., Wang, C. (eds.) ATVA 2018. LNCS, vol. 11138, pp. 543\u2013550. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-01090-4_34"},{"key":"4_CR151","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"567","DOI":"10.1007\/978-3-319-96145-3_30","volume-title":"Computer Aided Verification","author":"J K\u0159et\u00ednsk\u00fd","year":"2018","unstructured":"K\u0159et\u00ednsk\u00fd, J., Meggendorfer, T., Sickert, S., Ziegler, C.: Rabinizer 4: from LTL to your favourite deterministic automaton. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 567\u2013577. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_30"},{"key":"4_CR152","doi-asserted-by":"publisher","unstructured":"Kret\u00ednsk\u00fd, J., Meggendorfer, T., Weininger, M.: Stopping criteria for value iteration on stochastic games with quantitative objectives. In: 38th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS), pp. 1\u201314 (2023). https:\/\/doi.org\/10.1109\/LICS56636.2023.10175771","DOI":"10.1109\/LICS56636.2023.10175771"},{"key":"4_CR153","unstructured":"Kret\u00ednsk\u00fd, J., Michel, F., Michel, L., P\u00e9rez, G.A.: Finite-memory near-optimal learning for Markov decision processes with long-run average reward. In: Adams, R.P., Gogate, V. (eds.) 36th Conference on Uncertainty in Artificial Intelligence (UAI). Proceedings of Machine Learning Research, vol.\u00a0124, pp. 1149\u20131158. AUAI Press (2020)"},{"key":"4_CR154","doi-asserted-by":"publisher","unstructured":"Kret\u00ednsk\u00fd, J., Ramneantu, E., Slivinskiy, A., Weininger, M.: Comparison of algorithms for simple stochastic games. Inf. Comput. 289(Part), 104885 (2022). https:\/\/doi.org\/10.1016\/j.ic.2022.104885","DOI":"10.1016\/j.ic.2022.104885"},{"key":"4_CR155","doi-asserted-by":"publisher","unstructured":"Kurniawati, H., Hsu, D., Lee, W.S.: SARSOP: efficient point-based POMDP planning by approximating optimally reachable belief spaces. In: Brock, O., Trinkle, J., Ramos, F. (eds.) Robotics: Science and Systems IV. The MIT Press (2008). https:\/\/doi.org\/10.15607\/RSS.2008.IV.009","DOI":"10.15607\/RSS.2008.IV.009"},{"key":"4_CR156","volume-title":"Computer Networking - A Top-down Approach Featuring the Internet","author":"JF Kurose","year":"2001","unstructured":"Kurose, J.F., Ross, K.W.: Computer Networking - A Top-down Approach Featuring the Internet. Addison-Wesley-Longman, Boston (2001)"},{"key":"4_CR157","doi-asserted-by":"publisher","unstructured":"Kuwahara, H., Mura, I.: An efficient and exact stochastic simulation method to analyze rare events in biochemical systems. J. Chem. Phys. 129(16) (2008). https:\/\/doi.org\/10.1063\/1.2987701","DOI":"10.1063\/1.2987701"},{"key":"4_CR158","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"475","DOI":"10.1007\/978-3-030-53291-8_25","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2020","unstructured":"Kwiatkowska, M., Norman, G., Parker, D., Santos, G.: PRISM-games 3.0: stochastic game verification with concurrency, equilibria and time. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12225, pp. 475\u2013487. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_25"},{"issue":"1\u20132","key":"4_CR159","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/s10703-020-00356-y","volume":"58","author":"M Kwiatkowska","year":"2021","unstructured":"Kwiatkowska, M., Norman, G., Parker, D., Santos, G.: Automatic verification of concurrent stochastic systems. Formal Methods Syst. Des. 58(1\u20132), 188\u2013250 (2021). https:\/\/doi.org\/10.1007\/s10703-020-00356-y","journal-title":"Formal Methods Syst. Des."},{"key":"4_CR160","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1007\/978-3-030-99527-0_4","volume-title":"TACAS 2022","author":"M Kwiatkowska","year":"2022","unstructured":"Kwiatkowska, M., Norman, G., Parker, D., Santos, G.: Correlated equilibria and fairness in concurrent stochastic games. In: Fisman, D., Rosu, G. (eds.) TACAS 2022. LNCS, vol. 13244, pp. 60\u201378. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99527-0_4"},{"key":"4_CR161","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"388","DOI":"10.1007\/978-3-031-22337-2_19","volume-title":"Principles of Systems Design","author":"M Kwiatkowska","year":"2022","unstructured":"Kwiatkowska, M., Norman, G., Parker, D., Santos, G.: Symbolic verification and strategy synthesis for turn-based stochastic games. In: Raskin, J.F., Chatterjee, K., Doyen, L., Majumdar, R. (eds.) Principles of Systems Design. LNCS, vol. 13660, pp. 388\u2013406. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-22337-2_19"},{"key":"4_CR162","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1007\/978-3-642-04368-0_17","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"M Kwiatkowska","year":"2009","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Stochastic games for verification of probabilistic timed automata. In: Ouaknine, J., Vaandrager, F.W. (eds.) FORMATS 2009. LNCS, vol. 5813, pp. 212\u2013227. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-04368-0_17"},{"key":"4_CR163","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585\u2013591. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_47"},{"key":"4_CR164","doi-asserted-by":"publisher","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D.: The PRISM benchmark suite. In: 9th International Conference on the Quantitative Evaluation of Systems (QEST), pp. 203\u2013204. IEEE Computer Society (2012). https:\/\/doi.org\/10.1109\/QEST.2012.14","DOI":"10.1109\/QEST.2012.14"},{"issue":"1","key":"4_CR165","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/s10703-006-0005-2","volume":"29","author":"MZ Kwiatkowska","year":"2006","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D., Sproston, J.: Performance analysis of probabilistic timed automata using digital clocks. Formal Methods Syst. Des. 29(1), 33\u201378 (2006). https:\/\/doi.org\/10.1007\/s10703-006-0005-2","journal-title":"Formal Methods Syst. Des."},{"issue":"1","key":"4_CR166","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/S0304-3975(01)00046-9","volume":"282","author":"MZ Kwiatkowska","year":"2002","unstructured":"Kwiatkowska, M.Z., Norman, G., Segala, R., Sproston, J.: Automatic verification of real-time systems with discrete probability distributions. Theor. Comput. Sci. 282(1), 101\u2013150 (2002). https:\/\/doi.org\/10.1016\/S0304-3975(01)00046-9","journal-title":"Theor. Comput. Sci."},{"issue":"7","key":"4_CR167","doi-asserted-by":"publisher","first-page":"1027","DOI":"10.1016\/j.ic.2007.01.004","volume":"205","author":"MZ Kwiatkowska","year":"2007","unstructured":"Kwiatkowska, M.Z., Norman, G., Sproston, J., Wang, F.: Symbolic model checking for probabilistic timed automata. Inf. Comput. 205(7), 1027\u20131077 (2007). https:\/\/doi.org\/10.1016\/j.ic.2007.01.004","journal-title":"Inf. Comput."},{"issue":"1","key":"4_CR168","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/s00165-006-0015-2","volume":"19","author":"R Lanotte","year":"2007","unstructured":"Lanotte, R., Maggiolo-Schettini, A., Troina, A.: Parametric probabilistic transition systems for system design and analysis. Formal Aspects Comput. 19(1), 93\u2013109 (2007). https:\/\/doi.org\/10.1007\/s00165-006-0015-2","journal-title":"Formal Aspects Comput."},{"key":"4_CR169","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"478","DOI":"10.1007\/978-3-319-91908-9_23","volume-title":"Computing and Software Science","author":"A Legay","year":"2019","unstructured":"Legay, A., Lukina, A., Traonouez, L.M., Yang, J., Smolka, S.A., Grosu, R.: Statistical model checking. In: Steffen, B., Woeginger, G. (eds.) Computing and Software Science. LNCS, vol. 10000, pp. 478\u2013504. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-319-91908-9_23"},{"issue":"5","key":"4_CR170","doi-asserted-by":"publisher","first-page":"1545","DOI":"10.1109\/TSE.2020.3024215","volume":"48","author":"M Li","year":"2022","unstructured":"Li, M., Turrini, A., Hahn, E.M., She, Z., Zhang, L.: Probabilistic preference planning problem for Markov decision processes. IEEE Trans. Software Eng. 48(5), 1545\u20131559 (2022). https:\/\/doi.org\/10.1109\/TSE.2020.3024215","journal-title":"IEEE Trans. Software Eng."},{"issue":"1","key":"4_CR171","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1287\/opre.39.1.162","volume":"39","author":"WS Lovejoy","year":"1991","unstructured":"Lovejoy, W.S.: Computationally feasible bounds for partially observed Markov decision processes. Oper. Res. 39(1), 162\u2013175 (1991). https:\/\/doi.org\/10.1287\/opre.39.1.162","journal-title":"Oper. Res."},{"issue":"1\u20132","key":"4_CR172","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1016\/S0004-3702(02)00378-8","volume":"147","author":"O Madani","year":"2003","unstructured":"Madani, O., Hanks, S., Condon, A.: On the undecidability of probabilistic planning and related stochastic optimization problems. Artif. Intell. 147(1\u20132), 5\u201334 (2003). https:\/\/doi.org\/10.1016\/S0004-3702(02)00378-8","journal-title":"Artif. Intell."},{"key":"4_CR173","doi-asserted-by":"publisher","unstructured":"Madsen, C., Zhang, Z., Roehner, N., Winstead, C., Myers, C.J.: Stochastic model checking of genetic circuits. ACM J. Emerg. Technol. Comput. Syst. 11(3), 23:1\u201323:21 (2014). https:\/\/doi.org\/10.1145\/2644817","DOI":"10.1145\/2644817"},{"key":"4_CR174","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/978-3-030-31784-3_21","volume-title":"Automated Technology for Verification and Analysis","author":"J Major","year":"2019","unstructured":"Major, J., Blahoudek, F., Strej\u010dek, J., Sasar\u00e1kov\u00e1, M., Zbon\u010d\u00e1kov\u00e1, T.: ltl3tela: LTL to small deterministic or nondeterministic Emerson-Lei automata. In: Chen, Y.-F., Cheng, C.-H., Esparza, J. (eds.) ATVA 2019. LNCS, vol. 11781, pp. 357\u2013365. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-31784-3_21"},{"issue":"2","key":"4_CR175","doi-asserted-by":"publisher","first-page":"308","DOI":"10.1287\/mnsc.1060.0614","volume":"53","author":"S Mannor","year":"2007","unstructured":"Mannor, S., Simester, D., Sun, P., Tsitsiklis, J.N.: Bias and variance approximation in value function estimates. Manag. Sci. 53(2), 308\u2013322 (2007). https:\/\/doi.org\/10.1287\/mnsc.1060.0614","journal-title":"Manag. Sci."},{"key":"4_CR176","doi-asserted-by":"publisher","unstructured":"Mausam, Kolobov, A.: Planning with Markov Decision Processes: An AI Perspective. Synthesis Lectures on Artificial Intelligence and Machine Learning, Morgan & Claypool Publishers (2012). https:\/\/doi.org\/10.2200\/S00426ED1V01Y201206AIM017","DOI":"10.2200\/S00426ED1V01Y201206AIM017"},{"key":"4_CR177","doi-asserted-by":"publisher","unstructured":"McMillan, K.L., Zuck, L.D.: Compositional testing of Internet protocols. In: 2019 IEEE Secure Development Conference (SecDev), pp. 161\u2013174. IEEE (2019). https:\/\/doi.org\/10.1109\/SecDev.2019.00031","DOI":"10.1109\/SecDev.2019.00031"},{"key":"4_CR178","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"536","DOI":"10.1007\/978-3-030-01090-4_33","volume-title":"Automated Technology for Verification and Analysis","author":"BL Mediouni","year":"2018","unstructured":"Mediouni, B.L., Nouri, A., Bozga, M., Dellabani, M., Legay, A., Bensalem, S.: $$\\cal{S}$$BIP 2.0: statistical model checking stochastic real-time systems. In: Lahiri, S.K., Wang, C. (eds.) ATVA 2018. LNCS, vol. 11138, pp. 536\u2013542. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-01090-4_33"},{"key":"4_CR179","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"320","DOI":"10.1007\/978-3-031-19992-9_20","volume-title":"ATVA 2022","author":"T Meggendorfer","year":"2022","unstructured":"Meggendorfer, T.: PET - a partial exploration tool for probabilistic verification. In: Bouajjani, A., Hol\u00edk, L., Wu, Z. (eds.) ATVA 2022. LNCS, vol. 13505, pp. 320\u2013326. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-19992-9_20"},{"key":"4_CR180","doi-asserted-by":"publisher","unstructured":"Meggendorfer, T.: QComp 2023: Stochastic games \u2013 evaluation (2023). https:\/\/doi.org\/10.5281\/zenodo.7831387","DOI":"10.5281\/zenodo.7831387"},{"key":"4_CR181","doi-asserted-by":"publisher","unstructured":"M\u00fcller, D., Sickert, S.: LTL to deterministic Emerson-Lei automata. In: Bouyer, P., Orlandini, A., Pietro, P.S. (eds.) 8th International Symposium on Games, Automata, Logics and Formal Verification (GandALF). EPTCS, vol.\u00a0256, pp. 180\u2013194 (2017). https:\/\/doi.org\/10.4204\/EPTCS.256.13","DOI":"10.4204\/EPTCS.256.13"},{"key":"4_CR182","doi-asserted-by":"publisher","unstructured":"Munsky, B., Khammash, M.: The finite state projection algorithm for the solution of the chemical master equation. J. Chem. Phys. 124(4) (2006). https:\/\/doi.org\/10.1063\/1.2145882","DOI":"10.1063\/1.2145882"},{"key":"4_CR183","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"540","DOI":"10.1007\/978-3-030-25540-4_31","volume-title":"Computer Aided Verification","author":"T Neupane","year":"2019","unstructured":"Neupane, T., Myers, C.J., Madsen, C., Zheng, H., Zhang, Z.: STAMINA: STochastic approximate model-checker for INfinite-state analysis. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 540\u2013549. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_31"},{"key":"4_CR184","series-title":"Computational Biology","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1007\/978-3-030-17297-8_12","volume-title":"Automated Reasoning for Systems Biology and Medicine","author":"T Neupane","year":"2019","unstructured":"Neupane, T., Zhang, Z., Madsen, C., Zheng, H., Myers, C.J.: Approximation techniques for stochastic analysis of biological systems. In: Li\u00f2, P., Zuliani, P. (eds.) Automated Reasoning for Systems Biology and Medicine. CB, vol. 30, pp. 327\u2013348. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17297-8_12"},{"issue":"3","key":"4_CR185","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1109\/24.974122","volume":"50","author":"VF Nicola","year":"2001","unstructured":"Nicola, V.F., Shahabuddin, P., Nakayama, M.K.: Techniques for fast simulation of models of highly dependable systems. IEEE Trans. Reliab. 50(3), 246\u2013264 (2001). https:\/\/doi.org\/10.1109\/24.974122","journal-title":"IEEE Trans. Reliab."},{"key":"4_CR186","doi-asserted-by":"publisher","unstructured":"Niehage, M., Hartmanns, A., Remke, A.: Learning optimal decisions for stochastic hybrid systems. In: Arun-Kumar, S., M\u00e9ry, D., Saha, I., Zhang, L. (eds.) 19th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE), pp. 44\u201355. ACM (2021). https:\/\/doi.org\/10.1145\/3487212.3487339","DOI":"10.1145\/3487212.3487339"},{"issue":"5","key":"4_CR187","doi-asserted-by":"publisher","first-page":"780","DOI":"10.1287\/opre.1050.0216","volume":"53","author":"A Nilim","year":"2005","unstructured":"Nilim, A., Ghaoui, L.E.: Robust control of Markov decision processes with uncertain transition matrices. Oper. Res. 53(5), 780\u2013798 (2005). https:\/\/doi.org\/10.1287\/opre.1050.0216","journal-title":"Oper. Res."},{"issue":"3","key":"4_CR188","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1007\/s11241-017-9269-4","volume":"53","author":"G Norman","year":"2017","unstructured":"Norman, G., Parker, D., Zou, X.: Verification and control of partially observable probabilistic systems. Real Time Syst. 53(3), 354\u2013402 (2017). https:\/\/doi.org\/10.1007\/s11241-017-9269-4","journal-title":"Real Time Syst."},{"key":"4_CR189","doi-asserted-by":"publisher","unstructured":"Pai, G.J., Dugan, J.B.: Automatic synthesis of dynamic fault trees from UML system models. In: 13th International Symposium on Software Reliability Engineering (ISSRE), pp. 243\u2013256. IEEE Computer Society (2002). https:\/\/doi.org\/10.1109\/ISSRE.2002.1173261","DOI":"10.1109\/ISSRE.2002.1173261"},{"key":"4_CR190","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1007\/978-3-030-53291-8_19","volume-title":"Computer Aided Verification","author":"K Phalakarn","year":"2020","unstructured":"Phalakarn, K., Takisaka, T., Haas, T., Hasuo, I.: Widest paths and global propagation in bounded value iteration for stochastic games. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12225, pp. 349\u2013371. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_19"},{"key":"4_CR191","doi-asserted-by":"publisher","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science (FOCS), pp. 46\u201357. IEEE Computer Society (1977). https:\/\/doi.org\/10.1109\/SFCS.1977.32","DOI":"10.1109\/SFCS.1977.32"},{"key":"4_CR192","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"222","DOI":"10.1007\/978-3-030-88885-5_15","volume-title":"Automated Technology for Verification and Analysis","author":"S Pranger","year":"2021","unstructured":"Pranger, S., K\u00f6nighofer, B., Posch, L., Bloem, R.: TEMPEST - synthesis tool for reactive systems and shields in probabilistic environments. In: Hou, Z., Ganesh, V. (eds.) ATVA 2021. LNCS, vol. 12971, pp. 222\u2013228. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-88885-5_15"},{"key":"4_CR193","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"527","DOI":"10.1007\/978-3-642-39799-8_35","volume-title":"Computer Aided Verification","author":"A Puggelli","year":"2013","unstructured":"Puggelli, A., Li, W., Sangiovanni-Vincentelli, A.L., Seshia, S.A.: Polynomial-time verification of PCTL properties of MDPs with convex uncertainties. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 527\u2013542. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_35"},{"key":"4_CR194","doi-asserted-by":"publisher","unstructured":"Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley Series in Probability and Statistics. Wiley (1994). https:\/\/doi.org\/10.1002\/9780470316887","DOI":"10.1002\/9780470316887"},{"key":"4_CR195","doi-asserted-by":"publisher","unstructured":"Quatmann, T.: Replication package: QComp 2023 \u2013 multi-objective analysis (2023). https:\/\/doi.org\/10.5281\/zenodo.8063883","DOI":"10.5281\/zenodo.8063883"},{"issue":"1","key":"4_CR196","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/s10703-021-00364-6","volume":"60","author":"T Quatmann","year":"2022","unstructured":"Quatmann, T., Junges, S., Katoen, J.P.: Markov automata with multiple objectives. Formal Methods Syst. Des. 60(1), 33\u201386 (2022). https:\/\/doi.org\/10.1007\/s10703-021-00364-6","journal-title":"Formal Methods Syst. Des."},{"key":"4_CR197","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1007\/978-3-030-72016-2_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T Quatmann","year":"2021","unstructured":"Quatmann, T., Katoen, J.-P.: Multi-objective optimization of long-run average and total rewards. In: TACAS 2021. LNCS, vol. 12651, pp. 230\u2013249. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72016-2_13"},{"key":"4_CR198","doi-asserted-by":"publisher","unstructured":"Reijsbergen, D., de\u00a0Boer, P.T., Scheinhardt, W.R.W., Juneja, S.: Path-ZVA: general, efficient, and automated importance sampling for highly reliable Markovian systems. ACM Trans. Model. Comput. Simul. 28(3), 22:1\u201322:25 (2018). https:\/\/doi.org\/10.1145\/3161569","DOI":"10.1145\/3161569"},{"key":"4_CR199","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/978-3-030-94583-1_16","volume-title":"VMCAI 2022","author":"R Roberts","year":"2022","unstructured":"Roberts, R., Neupane, T., Buecherl, L., Myers, C.J., Zhang, Z.: STAMINA 2.0: improving scalability of infinite-state stochastic model checking. In: Finkbeiner, B., Wies, T. (eds.) VMCAI 2022. LNCS, vol. 13182, pp. 319\u2013331. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-94583-1_16"},{"key":"4_CR200","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1016\/j.ress.2019.02.004","volume":"186","author":"E Ruijters","year":"2019","unstructured":"Ruijters, E., Reijsbergen, D., de Boer, P.T., Stoelinga, M.: Rare event simulation for dynamic fault trees. Reliab. Eng. Syst. Saf. 186, 220\u2013231 (2019). https:\/\/doi.org\/10.1016\/j.ress.2019.02.004","journal-title":"Reliab. Eng. Syst. Saf."},{"key":"4_CR201","volume-title":"Artificial Intelligence: A Modern Approach","author":"S Russell","year":"2020","unstructured":"Russell, S., Norvig, P.: Artificial Intelligence: A Modern Approach, 4th edn. Pearson, London (2020)","edition":"4"},{"key":"4_CR202","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/978-3-030-86772-0_20","volume-title":"Symbolic and Quantitative Approaches to Reasoning with Uncertainty","author":"B Salmani","year":"2021","unstructured":"Salmani, B., Katoen, J.-P.: Fine-tuning the odds in Bayesian networks. In: Vejnarov\u00e1, J., Wilson, N. (eds.) ECSQARU 2021. LNCS (LNAI), vol. 12897, pp. 268\u2013283. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-86772-0_20"},{"key":"4_CR203","doi-asserted-by":"publisher","unstructured":"Schwartz, A.: A reinforcement learning method for maximizing undiscounted rewards. In: Utgoff, P.E. (ed.) 10th International Conference on Machine Learning (ICML), pp. 298\u2013305. Morgan Kaufmann (1993). https:\/\/doi.org\/10.1016\/b978-1-55860-307-3.50045-9","DOI":"10.1016\/b978-1-55860-307-3.50045-9"},{"issue":"1","key":"4_CR204","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10458-012-9200-2","volume":"27","author":"G Shani","year":"2013","unstructured":"Shani, G., Pineau, J., Kaplow, R.: A survey of point-based POMDP solvers. Auton. Agents Multi Agent Syst. 27(1), 1\u201351 (2013). https:\/\/doi.org\/10.1007\/s10458-012-9200-2","journal-title":"Auton. Agents Multi Agent Syst."},{"key":"4_CR205","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1007\/978-3-319-41540-6_17","volume-title":"Computer Aided Verification","author":"S Sickert","year":"2016","unstructured":"Sickert, S., Esparza, J., Jaax, S., K\u0159et\u00ednsk\u00fd, J.: Limit-deterministic B\u00fcchi automata for linear temporal logic. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 312\u2013332. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41540-6_17"},{"key":"4_CR206","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1007\/978-3-319-46520-3_9","volume-title":"Automated Technology for Verification and Analysis","author":"S Sickert","year":"2016","unstructured":"Sickert, S., K\u0159et\u00ednsk\u00fd, J.: MoChiBA: probabilistic LTL model checking using limit-deterministic B\u00fcchi automata. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 130\u2013137. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-46520-3_9"},{"key":"4_CR207","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"479","DOI":"10.1007\/978-3-030-31784-3_28","volume-title":"Automated Technology for Verification and Analysis","author":"J Spel","year":"2019","unstructured":"Spel, J., Junges, S., Katoen, J.-P.: Are parametric Markov chains monotonic? In: Chen, Y.-F., Cheng, C.-H., Esparza, J. (eds.) ATVA 2019. LNCS, vol. 11781, pp. 479\u2013496. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-31784-3_28"},{"key":"4_CR208","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-030-72016-2_10","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J Spel","year":"2021","unstructured":"Spel, J., Junges, S., Katoen, J.-P.: Finding provably optimal Markov chains. In: TACAS 2021. LNCS, vol. 12651, pp. 173\u2013190. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72016-2_10"},{"key":"4_CR209","doi-asserted-by":"publisher","unstructured":"Suilen, M., Jansen, N., Cubuktepe, M., Topcu, U.: Robust policy synthesis for uncertain POMDPs via convex optimization. In: Bessiere, C. (ed.) 29th International Joint Conference on Artificial Intelligence (IJCAI), pp. 4113\u20134120. ijcai.org (2020). https:\/\/doi.org\/10.24963\/ijcai.2020\/569","DOI":"10.24963\/ijcai.2020\/569"},{"key":"4_CR210","unstructured":"Suilen, M., Sim\u00e3o, T.D., Parker, D., Jansen, N.: Robust anytime learning of Markov decision processes. In: NeurIPS (2022)"},{"key":"4_CR211","doi-asserted-by":"publisher","unstructured":"Taylor, L., Israelsen, B., Zhang, Z.: Cycle and commute: rare-event probability verification for chemical reaction networks. In: Nadel, A., Rozier, K.Y. (eds.) 23rd Conference on Formal Methods in Computer-Aided Design (FMCAD), pp. 284\u2013293. TU Wien Academic Press (2023). https:\/\/doi.org\/10.34727\/2023\/ISBN.978-3-85448-060-0_37","DOI":"10.34727\/2023\/ISBN.978-3-85448-060-0_37"},{"key":"4_CR212","volume-title":"Stochastic Processes in Physics and Chemistry","author":"NG Van Kampen","year":"1992","unstructured":"Van Kampen, N.G.: Stochastic Processes in Physics and Chemistry, vol. 1. Elsevier, Amsterdam (1992)"},{"key":"4_CR213","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification (preliminary report). In: 1st Annual IEEE Symposium on Logic in Computer Science (LICS), pp. 332\u2013344. IEEE Computer Society (1986)"},{"key":"4_CR214","doi-asserted-by":"publisher","unstructured":"Velasquez, A., Alkhouri, I., Beckus, A., Trivedi, A., Atia, G.K.: Controller synthesis for omega-regular and steady-state specifications. In: Faliszewski, P., Mascardi, V., Pelachaud, C., Taylor, M.E. (eds.) 21st International Conference on Autonomous Agents and Multiagent Systems (AAMAS), pp. 1310\u20131318. International Foundation for Autonomous Agents and Multiagent Systems (2022). https:\/\/doi.org\/10.5555\/3535850.3535996","DOI":"10.5555\/3535850.3535996"},{"key":"4_CR215","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1016\/j.peva.2018.02.002","volume":"121\u2013122","author":"J Vill\u00e9n-Altamirano","year":"2018","unstructured":"Vill\u00e9n-Altamirano, J.: RESTART vs splitting: a comparative study. Perform. Evaluation 121\u2013122, 38\u201347 (2018). https:\/\/doi.org\/10.1016\/j.peva.2018.02.002","journal-title":"Perform. Evaluation"},{"key":"4_CR216","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/978-3-319-45477-1_20","volume-title":"Computer Safety, Reliability, and Security","author":"M Volk","year":"2016","unstructured":"Volk, M., Junges, S., Katoen, J.-P.: Advancing dynamic fault tree analysis - get\u00a0succinct state spaces fast and synthesise failure rates. In: Skavhaug, A., Guiochet, J., Bitsch, F. (eds.) SAFECOMP 2016. LNCS, vol. 9922, pp. 253\u2013265. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-45477-1_20"},{"issue":"1","key":"4_CR217","doi-asserted-by":"publisher","first-page":"370","DOI":"10.1109\/TII.2017.2710316","volume":"14","author":"M Volk","year":"2018","unstructured":"Volk, M., Junges, S., Katoen, J.P.: Fast dynamic fault tree analysis by model checking techniques. IEEE Trans. Ind. Informatics 14(1), 370\u2013379 (2018). https:\/\/doi.org\/10.1109\/TII.2017.2710316","journal-title":"IEEE Trans. Ind. Informatics"},{"issue":"6","key":"4_CR218","doi-asserted-by":"publisher","first-page":"1358","DOI":"10.1287\/opre.2014.1314","volume":"62","author":"W Wiesemann","year":"2014","unstructured":"Wiesemann, W., Kuhn, D., Sim, M.: Distributionally robust convex optimization. Oper. Res. 62(6), 1358\u20131376 (2014). https:\/\/doi.org\/10.1287\/opre.2014.1314","journal-title":"Oper. Res."},{"key":"4_CR219","doi-asserted-by":"publisher","unstructured":"Winkler, T., Junges, S., P\u00e9rez, G.A., Katoen, J.P.: On the complexity of reachability in parametric Markov decision processes. In: Fokkink, W.J., van Glabbeek, R. (eds.) 30th International Conference on Concurrency Theory (CONCUR). LIPIcs, vol.\u00a0140, pp. 14:1\u201314:17. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2019). https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2019.14","DOI":"10.4230\/LIPIcs.CONCUR.2019.14"},{"key":"4_CR220","doi-asserted-by":"publisher","unstructured":"Wolff, E.M., Topcu, U., Murray, R.M.: Robust control of uncertain Markov decision processes with temporal logic specifications. In: 51th IEEE Conference on Decision and Control (CDC), pp. 3372\u20133379. IEEE (2012). https:\/\/doi.org\/10.1109\/CDC.2012.6426174","DOI":"10.1109\/CDC.2012.6426174"},{"key":"4_CR221","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/3-540-45657-0_17","volume-title":"Computer Aided Verification","author":"HLS Younes","year":"2002","unstructured":"Younes, H.L.S., Simmons, R.G.: Probabilistic verification of discrete event systems using acceptance sampling. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 223\u2013235. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45657-0_17"},{"key":"4_CR222","unstructured":"Yu, H., Bertsekas, D.P.: Discretized approximations for POMDP with average cost. In: Chickering, D.M., Halpern, J.Y. (eds.) 20th Conference on Uncertainty in Artificial Intelligence (UAI), p.\u00a0519. AUAI Press (2004)"},{"issue":"2","key":"4_CR223","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1504\/IJCBDD.2009.028825","volume":"2","author":"J Zhang","year":"2009","unstructured":"Zhang, J., Watson, L.T., Cao, Y.: Adaptive aggregation method for the chemical master equation. Int. J. Comput. Biol. Drug Des. 2(2), 134\u2013148 (2009). https:\/\/doi.org\/10.1504\/IJCBDD.2009.028825","journal-title":"Int. J. Comput. Biol. Drug Des."}],"container-title":["Lecture Notes in Computer Science","TOOLympics Challenge 2023"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-67695-6_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,25]],"date-time":"2025-06-25T09:13:13Z","timestamp":1750842793000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-67695-6_4"}},"subtitle":["QComp 2023 Competition Report"],"short-title":[],"issued":{"date-parts":[[2024,11,1]]},"ISBN":["9783031676949","9783031676956"],"references-count":223,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-67695-6_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,11,1]]},"assertion":[{"value":"1 November 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}