{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,28]],"date-time":"2026-07-28T17:04:25Z","timestamp":1785258265818,"version":"3.55.0"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032054340","type":"print"},{"value":"9783032054357","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,9,12]],"date-time":"2025-09-12T00:00:00Z","timestamp":1757635200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,9,12]],"date-time":"2025-09-12T00:00:00Z","timestamp":1757635200000},"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":[[2026]]},"DOI":"10.1007\/978-3-032-05435-7_20","type":"book-chapter","created":{"date-parts":[[2025,9,13]],"date-time":"2025-09-13T01:30:17Z","timestamp":1757727017000},"page":"357-376","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Runtime Verification for\u00a0LTL in\u00a0Stochastic Systems"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9862-4919","authenticated-orcid":false,"given":"Javier","family":"Esparza","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0009-3071-0736","authenticated-orcid":false,"given":"Vincent","family":"Fischer","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,9,12]]},"reference":[{"key":"20_CR1","volume-title":"Principles of model checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of model checking. MIT Press, Cambridge, Massachusetts (2008)"},{"key":"20_CR2","unstructured":"Barringer, H., Goldberg, A., Havelund, K., Sen, K.: Program monitoring with LTL in EAGLE. In: IPDPS. IEEE Computer Society (2004)"},{"key":"20_CR3","doi-asserted-by":"crossref","unstructured":"Barringer, H., Goldberg, A., Havelund, K., Sen, K.: Rule-based runtime verification. In: VMCAI. Lecture Notes in Computer Science, vol. 2937, pp. 44\u201357. Springer (2004)","DOI":"10.1007\/978-3-540-24622-0_5"},{"key":"20_CR4","doi-asserted-by":"crossref","unstructured":"Bartocci, E., Falcone, Y., Francalanza, A., Reger, G.: Introduction to runtime verification. In: Lectures on Runtime Verification, Lecture Notes in Computer Science, vol. 10457, pp. 1\u201333. Springer (2018)","DOI":"10.1007\/978-3-319-75632-5_1"},{"key":"20_CR5","doi-asserted-by":"crossref","unstructured":"Bauer, A., Leucker, M., Schallhart, C.: Monitoring of real-time properties. In: FSTTCS. Lecture Notes in Computer Science, vol. 4337, pp. 260\u2013272. Springer (2006)","DOI":"10.1007\/11944836_25"},{"key":"20_CR6","doi-asserted-by":"crossref","unstructured":"Bauer, A., Leucker, M., Schallhart, C.: The good, the bad, and the ugly, but how ugly is ugly? In: RV. Lecture Notes in Computer Science, vol. 4839, pp. 126\u2013138. Springer (2007)","DOI":"10.1007\/978-3-540-77395-5_11"},{"issue":"3","key":"20_CR7","doi-asserted-by":"publisher","first-page":"651","DOI":"10.1093\/logcom\/exn075","volume":"20","author":"A Bauer","year":"2010","unstructured":"Bauer, A., Leucker, M., Schallhart, C.: Comparing LTL semantics for runtime verification. J. Log. Comput. 20(3), 651\u2013674 (2010)","journal-title":"J. Log. Comput."},{"key":"20_CR8","doi-asserted-by":"crossref","unstructured":"Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for LTL and TLTL. ACM Trans. Softw. Eng. Methodol. 20(4), 14:1\u201314:64 (2011)","DOI":"10.1145\/2000799.2000800"},{"key":"20_CR9","doi-asserted-by":"crossref","unstructured":"Bonnet, R., Kiefer, S., Lin, A.W.: Analysis of probabilistic basic parallel processes. In: FoSSaCS. Lecture Notes in Computer Science, vol. 8412, pp. 43\u201357. Springer (2014)","DOI":"10.1007\/978-3-642-54830-7_3"},{"issue":"2","key":"20_CR10","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/s10703-012-0166-0","volume":"43","author":"T Br\u00e1zdil","year":"2013","unstructured":"Br\u00e1zdil, T., Esparza, J., Kiefer, S., Kucera, A.: Analyzing probabilistic pushdown automata. Formal Methods Syst. Des. 43(2), 124\u2013163 (2013)","journal-title":"Formal Methods Syst. Des."},{"key":"20_CR11","doi-asserted-by":"crossref","unstructured":"Br\u00e1zdil, T., Kiefer, S., Kucera, A.: Efficient analysis of probabilistic programs with an unbounded counter. J. ACM 61(6), 41:1\u201341:35 (2014)","DOI":"10.1145\/2629599"},{"key":"20_CR12","doi-asserted-by":"crossref","unstructured":"Daca, P., Henzinger, T.A., Kret\u00ednsk\u00fd, J., Petrov, T.: Faster statistical model checking for unbounded temporal properties. ACM Trans. Comput. Log. 18(2), 12:1\u201312:25 (2017)","DOI":"10.1145\/3060139"},{"key":"20_CR13","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: ICSE, pp. 411\u2013420. ACM (1999)","DOI":"10.1145\/302405.302672"},{"key":"20_CR14","unstructured":"Esparza, J., Grande, V.P.: Black-box testing liveness properties of partially observable stochastic systems. In: ICALP. LIPIcs, vol.\u00a0261, pp. 126:1\u2013126:17. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2023)"},{"key":"20_CR15","unstructured":"Esparza, J., Kiefer, S., Kret\u00ednsk\u00fd, J., Weininger, M.: Enforcing $$\\omega $$-regular properties in markov chains by restarting. In: CONCUR. LIPIcs, vol.\u00a0203, pp. 5:1\u20135:22. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2021)"},{"key":"20_CR16","doi-asserted-by":"crossref","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)","DOI":"10.1145\/3417995"},{"key":"20_CR17","unstructured":"Falcone, Y., Havelund, K., Reger, G.: A tutorial on runtime verification. In: Engineering Dependable Software Systems, NATO Science for Peace and Security Series, D: Information and Communication Security, vol.\u00a034, pp. 141\u2013175. IOS Press (2013)"},{"key":"20_CR18","doi-asserted-by":"crossref","unstructured":"Gondi, K., Patel, Y., Sistla, A.P.: Monitoring the full range of omega-regular properties of stochastic systems. In: VMCAI. Lecture Notes in Computer Science, vol.\u00a05403, pp. 105\u2013119. Springer (2009)","DOI":"10.1007\/978-3-540-93900-9_12"},{"key":"20_CR19","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Mazzocchi, N., Sara\u00e7, N.E.: Abstract monitors for quantitative specifications. In: RV. Lecture Notes in Computer Science, vol. 13498, pp. 200\u2013220. Springer (2022)","DOI":"10.1007\/978-3-031-17196-3_11"},{"key":"20_CR20","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Sara\u00e7, N.E.: Quantitative and approximate monitoring. In: LICS. pp. 1\u201314. IEEE (2021)","DOI":"10.1109\/LICS52264.2021.9470547"},{"issue":"3","key":"20_CR21","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1007\/s10009-010-0184-4","volume":"14","author":"X Huang","year":"2012","unstructured":"Huang, X., et al.: Software monitoring with controllable overhead. Int. J. Softw. Tools Technol. Transf. 14(3), 327\u2013347 (2012)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"3","key":"20_CR22","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1023\/A:1011254632723","volume":"19","author":"O Kupferman","year":"2001","unstructured":"Kupferman, O., Vardi, M.Y.: Model checking of safety properties. Formal Methods Syst. Des. 19(3), 291\u2013314 (2001)","journal-title":"Formal Methods Syst. Des."},{"key":"20_CR23","doi-asserted-by":"crossref","unstructured":"Legay, A., Lukina, A., Traonouez, L., Yang, J., Smolka, S.A., Grosu, R.: Statistical model checking. In: Computing and Software Science, Lecture Notes in Computer Science, vol. 10000, pp. 478\u2013504. Springer (2019)","DOI":"10.1007\/978-3-319-91908-9_23"},{"key":"20_CR24","volume-title":"Testing statistical hypotheses","author":"EL Lehmann","year":"2005","unstructured":"Lehmann, E.L., Romano, J.P.: Testing statistical hypotheses. Springer Texts in Statistics, Springer, New York (2005)"},{"issue":"5","key":"20_CR25","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1016\/j.jlap.2008.08.004","volume":"78","author":"M Leucker","year":"2009","unstructured":"Leucker, M., Schallhart, C.: A brief account of runtime verification. J. Log. Algebraic Methods Program. 78(5), 293\u2013303 (2009)","journal-title":"J. Log. Algebraic Methods Program."},{"key":"20_CR26","doi-asserted-by":"crossref","unstructured":"Norris, J.R.: Markov Chains. Cambridge University Press (1997)","DOI":"10.1017\/CBO9780511810633"},{"key":"20_CR27","doi-asserted-by":"crossref","unstructured":"Stoller, S.D., et al.: Runtime verification with state estimation. In: RV. Lecture Notes in Computer Science, vol.\u00a07186, pp. 193\u2013207. Springer (2011)","DOI":"10.1007\/978-3-642-29860-8_15"}],"container-title":["Lecture Notes in Computer Science","Runtime Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-05435-7_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,28]],"date-time":"2026-07-28T16:47:51Z","timestamp":1785257271000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-05435-7_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9,12]]},"ISBN":["9783032054340","9783032054357"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-05435-7_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,9,12]]},"assertion":[{"value":"12 September 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"RV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Runtime Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Graz","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Austria","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 September 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19 September 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"rv2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/rv25.isec.tugraz.at\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}