{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,29]],"date-time":"2026-07-29T10:55:09Z","timestamp":1785322509084,"version":"3.55.0"},"publisher-location":"Cham","reference-count":59,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030816872","type":"print"},{"value":"9783030816889","type":"electronic"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,7,15]],"date-time":"2021-07-15T00:00:00Z","timestamp":1626307200000},"content-version":"vor","delay-in-days":195,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We investigate the problem of monitoring partially observable systems with nondeterministic and probabilistic dynamics. In such systems, every state may be associated with a risk, e.g., the probability of an imminent crash. During runtime, we obtain partial information about the system state in form of observations. The monitor uses this information to estimate the risk of the (unobservable) current system state. Our results are threefold. First, we show that extensions of state estimation approaches do not scale due the combination of nondeterminism and probabilities. While exploiting a geometric interpretation of the state estimates improves the practical runtime, this cannot prevent an exponential memory blowup. Second, we present a tractable algorithm based on model checking conditional reachability probabilities. Third, we provide prototypical implementations and manifest the applicability of our algorithms to a range of benchmarks. The results highlight the possibilities and boundaries of our novel algorithms.<\/jats:p>","DOI":"10.1007\/978-3-030-81688-9_26","type":"book-chapter","created":{"date-parts":[[2021,7,16]],"date-time":"2021-07-16T16:20:47Z","timestamp":1626452447000},"page":"553-576","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":22,"title":["Runtime Monitors for Markov Decision Processes"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0978-8466","authenticated-orcid":false,"given":"Sebastian","family":"Junges","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9628-1200","authenticated-orcid":false,"given":"Hazem","family":"Torfah","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6190-8707","authenticated-orcid":false,"given":"Sanjit A.","family":"Seshia","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2021,7,15]]},"reference":[{"key":"26_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-31280-0_1","volume-title":"Testing Software and Systems","author":"BK Aichernig","year":"2019","unstructured":"Aichernig, B.K., et al.: Learning a behavior model of hybrid systems through combining model-based testing and machine learning. In: Gaston, C., Kosmatov, N., Le Gall, P. (eds.) ICTSS 2019. LNCS, vol. 11812, pp. 3\u201321. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-31280-0_1"},{"issue":"3","key":"26_CR2","doi-asserted-by":"publisher","first-page":"416","DOI":"10.1007\/s10703-019-00333-0","volume":"54","author":"BK Aichernig","year":"2019","unstructured":"Aichernig, B.K., Tappler, M.: Probabilistic black-box reachability checking (extended version). Formal Methods Syst. Des. 54(3), 416\u2013448 (2019)","journal-title":"Formal Methods Syst. Des."},{"key":"26_CR3","doi-asserted-by":"crossref","unstructured":"Alshiekh, M., Bloem, R., Ehlers, R., K\u00f6nighofer, B., Niekum, S., Topcu, U.: Safe reinforcement learning via shielding. In: AAAI, pp. 2669\u20132678. AAAI Press (2018)","DOI":"10.1609\/aaai.v32i1.11797"},{"key":"26_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/978-3-540-40903-8_8","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"S Andova","year":"2004","unstructured":"Andova, S., Hermanns, H., Katoen, J.-P.: Discrete-time rewards model-checked. In: Larsen, K.G., Niebert, P. (eds.) FORMATS 2003. LNCS, vol. 2791, pp. 88\u2013104. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-40903-8_8"},{"key":"26_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"630","DOI":"10.1007\/978-3-030-25540-4_36","volume-title":"Computer Aided Verification","author":"G Avni","year":"2019","unstructured":"Avni, G., Bloem, R., Chatterjee, K., Henzinger, T.A., K\u00f6nighofer, B., Pranger, S.: Run-time optimization for learned controllers through quantitative games. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 630\u2013649. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_36"},{"key":"26_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1007\/978-3-319-92970-5_13","volume-title":"Software Engineering and Formal Methods","author":"R Babaee","year":"2018","unstructured":"Babaee, R., Gurfinkel, A., Fischmeister, S.: $$\\cal{P}revent$$: a predictive run-time verification framework using statistical learning. In: Johnsen, E.B., Schaefer, I. (eds.) SEFM 2018. LNCS, vol. 10886, pp. 205\u2013220. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-92970-5_13"},{"key":"26_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/978-3-030-03769-7_11","volume-title":"Runtime Verification","author":"R Babaee","year":"2018","unstructured":"Babaee, R., Gurfinkel, A., Fischmeister, S.: Predictive run-time verification of discrete-time reachability properties in black-box systems using trace-level abstraction and statistical learning. In: Colombo, C., Leucker, M. (eds.) RV 2018. LNCS, vol. 11237, pp. 187\u2013204. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-03769-7_11"},{"key":"26_CR8","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"26_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"515","DOI":"10.1007\/978-3-642-54862-8_43","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C Baier","year":"2014","unstructured":"Baier, C., Klein, J., Kl\u00fcppelholz, S., M\u00e4rcker, S.: Computing conditional probabilities in Markovian models efficiently. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 515\u2013530. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_43"},{"issue":"4","key":"26_CR10","doi-asserted-by":"publisher","first-page":"469","DOI":"10.1145\/235815.235821","volume":"22","author":"CB Barber","year":"1996","unstructured":"Barber, C.B., Dobkin, D.P., Huhdanpaa, H.: The Quickhull algorithm for convex hulls. ACM Trans. Math. Softw. 22(4), 469\u2013483 (1996)","journal-title":"ACM Trans. Math. Softw."},{"key":"26_CR11","unstructured":"Barrett, C.W., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 825\u2013885. IOS Press (2009)"},{"key":"26_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-319-75632-5_5","volume-title":"Lectures on Runtime Verification","author":"E Bartocci","year":"2018","unstructured":"Bartocci, E., et al.: Specification-based monitoring of cyber-physical systems: a survey on theory, tools and applications. In: Bartocci, E., Falcone, Y. (eds.) Lectures on Runtime Verification. LNCS, vol. 10457, pp. 135\u2013175. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-75632-5_5"},{"key":"26_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1007\/978-3-642-54830-7_2","volume-title":"Foundations of Software Science and Computation Structures","author":"N Bertrand","year":"2014","unstructured":"Bertrand, N., Fabre, \u00c9., Haar, S., Haddad, S., H\u00e9lou\u00ebt, L.: Active diagnosis for probabilistic systems. In: Muscholl, A. (ed.) FoSSaCS 2014. LNCS, vol. 8412, pp. 29\u201342. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54830-7_2"},{"key":"26_CR14","doi-asserted-by":"crossref","unstructured":"Bertrand, N., Haddad, S., Lefaucheux, E.: A tale of two diagnoses in probabilistic systems. Inf. Comput. 269 (2019)","DOI":"10.1016\/j.ic.2019.104441"},{"key":"26_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"533","DOI":"10.1007\/978-3-662-46681-0_51","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Bloem","year":"2015","unstructured":"Bloem, R., K\u00f6nighofer, B., K\u00f6nighofer, R., Wang, C.: Shield synthesis: runtime enforcement for reactive systems. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 533\u2013548. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_51"},{"key":"26_CR16","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":"26_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/978-3-030-32079-9_8","volume-title":"Runtime Verification","author":"L Bortolussi","year":"2019","unstructured":"Bortolussi, L., Cairoli, F., Paoletti, N., Smolka, S.A., Stoller, S.D.: Neural predictive monitoring. In: Finkbeiner, B., Mariani, L. (eds.) RV 2019. LNCS, vol. 11757, pp. 129\u2013147. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-32079-9_8"},{"key":"26_CR18","volume-title":"Convex Optimization","author":"SP Boyd","year":"2014","unstructured":"Boyd, S.P., Vandenberghe, L.: Convex Optimization. Cambridge University Press, Cambridge (2014)"},{"key":"26_CR19","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1016\/j.artint.2016.01.007","volume":"234","author":"K Chatterjee","year":"2016","unstructured":"Chatterjee, K., Chmelik, M., Gupta, R., Kanodia, A.: Optimal cost almost-sure reachability in POMDPs. Artif. Intell. 234, 26\u201348 (2016)","journal-title":"Artif. Intell."},{"key":"26_CR20","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Doyen, L.: Partial-observation stochastic games: how to win when belief fails. ACM Trans. Comput. Log. 15(2), 16:1\u201316:44 (2014)","DOI":"10.1145\/2579821"},{"key":"26_CR21","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Novotn\u00fd, P., P\u00e9rez, G.A., Raskin, J., Zikelic, D.: Optimizing expectation with guarantees in POMDPs. In: AAAI, pp. 3725\u20133732. AAAI Press (2017)","DOI":"10.1609\/aaai.v31i1.11046"},{"key":"26_CR22","doi-asserted-by":"crossref","unstructured":"Chou, Y., Yoon, H., Sankaranarayanan, S.: Predictive runtime monitoring of vehicle models using Bayesian estimation and reachability analysis. In: IROS (2020, to appear)","DOI":"10.1109\/IROS45743.2020.9340755"},{"key":"26_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1007\/978-3-030-32079-9_10","volume-title":"Runtime Verification","author":"A Cimatti","year":"2019","unstructured":"Cimatti, A., Tian, C., Tonetta, S.: Assumption-based runtime verification with partial observability and resets. In: Finkbeiner, B., Mariani, L. (eds.) RV 2019. LNCS, vol. 11757, pp. 165\u2013184. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-32079-9_10"},{"key":"26_CR24","doi-asserted-by":"crossref","unstructured":"Dr\u00e4ger, K., Forejt, V., Kwiatkowska, M.Z., Parker, D., Ujma, M.: Permissive controller synthesis for probabilistic systems. Log. Methods Comput. Sci. 11(2) (2015)","DOI":"10.2168\/LMCS-11(2:16)2015"},{"issue":"1","key":"26_CR25","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/s00165-017-0440-4","volume":"30","author":"M Gerhold","year":"2018","unstructured":"Gerhold, M., Stoelinga, M.: Model-based testing of probabilistic systems. Formal Asp. Comput. 30(1), 77\u2013106 (2018)","journal-title":"Formal Asp. Comput."},{"key":"26_CR26","unstructured":"Grigore, R., Kiefer, S.: Selective monitoring. In: CONCUR. LIPIcs, vol. 118, pp. 20:1\u201320:16. Dagstuhl - LZI (2018)"},{"key":"26_CR27","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1016\/j.tcs.2016.12.003","volume":"735","author":"S Haddad","year":"2018","unstructured":"Haddad, S., Monmege, B.: Interval iteration algorithm for MDPs and IMDPs. Theor. Comput. Sci. 735, 111\u2013131 (2018)","journal-title":"Theor. Comput. Sci."},{"key":"26_CR28","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":"26_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-03769-7_1","volume-title":"Runtime Verification","author":"K Havelund","year":"2018","unstructured":"Havelund, K., Ro\u015fu, G.: Runtime verification - 17 years later. In: Colombo, C., Leucker, M. (eds.) RV 2018. LNCS, vol. 11237, pp. 3\u201317. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-03769-7_1"},{"key":"26_CR30","doi-asserted-by":"crossref","unstructured":"Hensel, C., Junges, S., Katoen, J., Quatmann, T., Volk, M.: The probabilistic model checker storm. CoRR abs\/2002.07080 (2020)","DOI":"10.1007\/s10009-021-00633-z"},{"key":"26_CR31","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Ho, P.-H., Wong-Toi, H.: Algorithmic analysis of nonlinear hybrid systems. IEEE Trans. Autom. Control 43(4), 540\u2013554 (1998)","DOI":"10.1109\/9.664156"},{"key":"26_CR32","doi-asserted-by":"crossref","unstructured":"Hor\u00e1k, K., Bosansk\u00fd, B., Chatterjee, K.: Goal-HSVI: heuristic search value iteration for goal POMDPs. In: IJCAI, pp. 4764\u20134770. ijcai.org (2018)","DOI":"10.24963\/ijcai.2018\/662"},{"key":"26_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/978-3-030-20652-9_16","volume-title":"NASA Formal Methods","author":"N Jansen","year":"2019","unstructured":"Jansen, N., Humphrey, L., Tumova, J., Topcu, U.: Structured synthesis for probabilistic systems. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2019. LNCS, vol. 11460, pp. 237\u2013254. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-20652-9_16"},{"key":"26_CR34","unstructured":"Jansen, N., K\u00f6nighofer, B., Junges, S., Serban, A., Bloem, R.: Safe reinforcement learning using probabilistic shields (invited paper). In: CONCUR. LIPIcs, vol. 171, pp. 3:1\u20133:16. Dagstuhl - LZI (2020)"},{"key":"26_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1007\/978-3-662-49674-9_8","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Junges","year":"2016","unstructured":"Junges, S., Jansen, N., Dehnert, C., Topcu, U., Katoen, J.-P.: Safety-constrained reinforcement learning for MDPs. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 130\u2013146. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49674-9_8"},{"key":"26_CR36","doi-asserted-by":"crossref","unstructured":"Junges, S., Torfah, H., Seshia, S.A.: Runtime monitoring for Markov decision processes. CoRR abs\/2105.12322 (2021)","DOI":"10.1007\/978-3-030-81688-9_26"},{"key":"26_CR37","doi-asserted-by":"crossref","unstructured":"Kiefer, S., Sistla, A.P.: Distinguishing hidden Markov chains. In: LICS, pp. 66\u201375. ACM (2016)","DOI":"10.1145\/2933575.2933608"},{"key":"26_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"issue":"2","key":"26_CR39","doi-asserted-by":"publisher","first-page":"412","DOI":"10.1109\/TSMCB.2009.2025657","volume":"40","author":"W Nam","year":"2010","unstructured":"Nam, W., Alur, R.: Active learning of plans for safety and reachability goals with partial observability. IEEE Trans. Syst. Man Cybern. Part B 40(2), 412\u2013420 (2010)","journal-title":"IEEE Trans. Syst. Man Cybern. Part B"},{"issue":"3","key":"26_CR40","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)","journal-title":"Real Time Syst."},{"issue":"3","key":"26_CR41","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1287\/moor.12.3.441","volume":"12","author":"CH Papadimitriou","year":"1987","unstructured":"Papadimitriou, C.H., Tsitsiklis, J.N.: The complexity of Markov decision processes. Math. Oper. Res. 12(3), 441\u2013450 (1987)","journal-title":"Math. Oper. Res."},{"key":"26_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/978-3-030-55754-6_6","volume-title":"NASA Formal Methods","author":"DT Phan","year":"2020","unstructured":"Phan, D.T., Grosu, R., Jansen, N., Paoletti, N., Smolka, S.A., Stoller, S.D.: Neural simplex architecture. In: Lee, R., Jha, S., Mavridou, A., Giannakopoulou, D. (eds.) NFM 2020. LNCS, vol. 12229, pp. 97\u2013114. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-55754-6_6"},{"key":"26_CR43","doi-asserted-by":"crossref","unstructured":"Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley Series in Probability and Statistics. Wiley (1994)","DOI":"10.1002\/9780470316887"},{"issue":"2","key":"26_CR44","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1109\/5.18626","volume":"77","author":"LR Rabiner","year":"1989","unstructured":"Rabiner, L.R.: A tutorial on hidden Markov models and selected applications in speech recognition. Proc. IEEE 77(2), 257\u2013286 (1989)","journal-title":"Proc. IEEE"},{"issue":"3","key":"26_CR45","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/s10703-019-00337-w","volume":"54","author":"C S\u00e1nchez","year":"2019","unstructured":"S\u00e1nchez, C., et al.: A survey of challenges for runtime verification from advanced application domains (beyond software). Formal Methods Syst. Des. 54(3), 279\u2013335 (2019)","journal-title":"Formal Methods Syst. Des."},{"issue":"2","key":"26_CR46","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1016\/S0022-0000(70)80006-X","volume":"4","author":"WJ Savitch","year":"1970","unstructured":"Savitch, W.J.: Relationships between nondeterministic and deterministic tape complexities. J. Comput. Syst. Sci. 4(2), 177\u2013192 (1970)","journal-title":"J. Comput. Syst. Sci."},{"key":"26_CR47","unstructured":"Schrijver, A.: Theory of Linear and Integer Programming. Wiley-Interscience Series in Discrete Mathematics and Optimization. Wiley (1999)"},{"key":"26_CR48","doi-asserted-by":"crossref","unstructured":"Seidel, R.: Convex hull computations. In: Handbook of Discrete and Computational Geometry, 2nd edn, pp. 495\u2013512. Chapman and Hall\/CRC (2004)","DOI":"10.1201\/9781420035315.pt3"},{"key":"26_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-030-32079-9_2","volume-title":"Runtime Verification","author":"SA Seshia","year":"2019","unstructured":"Seshia, S.A.: Introspective environment modeling. In: Finkbeiner, B., Mariani, L. (eds.) RV 2019. LNCS, vol. 11757, pp. 15\u201326. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-32079-9_2"},{"key":"26_CR50","unstructured":"Seshia, S.A., Sadigh, D., Sastry, S.S.: Towards verified artificial intelligence. arXiv e-prints, July 2016"},{"key":"26_CR51","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"294","DOI":"10.1007\/978-3-540-78163-9_25","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"AP Sistla","year":"2008","unstructured":"Sistla, A.P., Srinivas, A.R.: Monitoring temporal properties of stochastic systems. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds.) VMCAI 2008. LNCS, vol. 4905, pp. 294\u2013308. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78163-9_25"},{"key":"26_CR52","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"276","DOI":"10.1007\/978-3-642-29860-8_21","volume-title":"Runtime Verification","author":"AP Sistla","year":"2012","unstructured":"Sistla, A.P., \u017defran, M., Feng, Y.: Runtime monitoring of stochastic cyber-physical systems with hybrid state. In: Khurshid, S., Sen, K. (eds.) RV 2011. LNCS, vol. 7186, pp. 276\u2013293. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-29860-8_21"},{"key":"26_CR53","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1007\/978-3-642-27645-3_12","volume-title":"Reinforcement Learning, Adaptation, Learning, and Optimization","author":"MTJ Spaan","year":"2012","unstructured":"Spaan, M.T.J.: Partially observable Markov decision processes. In: Wiering, M., van Otterlo, M. (eds.) Reinforcement Learning, Adaptation, Learning, and Optimization, vol. 12, pp. 387\u2013414. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-27645-3_12"},{"key":"26_CR54","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/978-3-642-29860-8_15","volume-title":"Runtime Verification","author":"SD Stoller","year":"2012","unstructured":"Stoller, S.D., et al.: Runtime verification with state estimation. In: Khurshid, S., Sen, K. (eds.) RV 2011. LNCS, vol. 7186, pp. 193\u2013207. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-29860-8_15"},{"key":"26_CR55","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"651","DOI":"10.1007\/978-3-030-30942-8_38","volume-title":"Formal Methods \u2013 The Next 30 Years","author":"M Tappler","year":"2019","unstructured":"Tappler, M., Aichernig, B.K., Bacci, G., Eichlseder, M., Larsen, K.G.: $$L^*$$-based learning of Markov decision processes. In: ter Beek, M.H., McIver, A., Oliveira, J.N. (eds.) FM 2019. LNCS, vol. 11800, pp. 651\u2013669. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-30942-8_38"},{"key":"26_CR56","unstructured":"Thrun, S., Burgard, W., Fox, D.: Probabilistic Robotics. Intelligent Robotics and Autonomous Agents. MIT Press (2005)"},{"key":"26_CR57","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"452","DOI":"10.1007\/978-3-642-16612-9_34","volume-title":"Runtime Verification","author":"CM Wilcox","year":"2010","unstructured":"Wilcox, C.M., Williams, B.C.: Runtime verification of stochastic, faulty systems. In: Barringer, H., et al. (eds.) RV 2010. LNCS, vol. 6418, pp. 452\u2013459. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-16612-9_34"},{"key":"26_CR58","doi-asserted-by":"crossref","unstructured":"Woo, H., Mok, A.K.: Real-time monitoring of uncertain data streams using probabilistic similarity. In: RTSS, pp. 288\u2013300. IEEE CS (2007)","DOI":"10.1109\/RTSS.2007.29"},{"key":"26_CR59","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/11562436_9","volume-title":"Formal Techniques for Networked and Distributed Systems - FORTE 2005","author":"L Zhang","year":"2005","unstructured":"Zhang, L., Hermanns, H., Jansen, D.N.: Logic and model checking for hidden Markov models. In: Wang, F. (ed.) FORTE 2005. LNCS, vol. 3731, pp. 98\u2013112. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11562436_9"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-81688-9_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,4]],"date-time":"2023-01-04T17:47:19Z","timestamp":1672854439000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-81688-9_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030816872","9783030816889"],"references-count":59,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-81688-9_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"15 July 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 July 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 July 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"33","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2021\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"290","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"63","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"22% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"12","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"16 tool papers and 5 invited papers are also included.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}