{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T14:21:32Z","timestamp":1743085292607,"version":"3.40.3"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031223365"},{"type":"electronic","value":"9783031223372"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"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":[[2022]]},"DOI":"10.1007\/978-3-031-22337-2_16","type":"book-chapter","created":{"date-parts":[[2022,12,28]],"date-time":"2022-12-28T10:08:41Z","timestamp":1672222121000},"page":"325-342","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["On Probabilistic Monitorability"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2197-3018","authenticated-orcid":false,"given":"Luca","family":"Aceto","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1314-333X","authenticated-orcid":false,"given":"Antonis","family":"Achilleos","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7526-9256","authenticated-orcid":false,"given":"Elli","family":"Anastasiadi","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3829-7391","authenticated-orcid":false,"given":"Adrian","family":"Francalanza","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8362-3075","authenticated-orcid":false,"given":"Anna","family":"Ing\u00f3lfsd\u00f3ttir","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1171-8790","authenticated-orcid":false,"given":"Karoliina","family":"Lehtinen","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7470-4962","authenticated-orcid":false,"given":"Mathias Ruggaard","family":"Pedersen","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,12,29]]},"reference":[{"key":"16_CR1","doi-asserted-by":"crossref","unstructured":"Aceto, L., Achilleos, A., Attard, D.P., Exibard, L., Francalanza, A., Ing\u00f3lfsd\u00f3ttir, A.: A monitoring tool for linear-time $$\\mu $$HML. In: ter Beek, M., Sirjani, M. (eds.) Proceedings of Coordination Models and Languages \u2013 24th IFIP WG 6.1 International Conference, COORDINATION 2022. LNCS. Springer, Cham (2022). (to appear)","DOI":"10.1007\/978-3-031-08143-9_12"},{"key":"16_CR2","unstructured":"Aceto, L., Achilleos, A., Francalanza, A., Ing\u00f3lfsd\u00f3ttir, A.: Monitoring for silent actions. In: Lokam, S.V., Ramanujam, R. (eds.) 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2017. LIPIcs, Kanpur, India, 11\u201315 December 2017, vol. 93, pp. 7:1\u20137:14. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2017)"},{"key":"16_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/978-3-319-89366-2_11","volume-title":"Foundations of Software Science and Computation Structures","author":"L Aceto","year":"2018","unstructured":"Aceto, L., Achilleos, A., Francalanza, A., Ing\u00f3lfsd\u00f3ttir, A.: A framework for parameterized monitorability. In: Baier, C., Dal Lago, U. (eds.) FoSSaCS 2018. LNCS, vol. 10803, pp. 203\u2013220. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89366-2_11"},{"key":"16_CR4","doi-asserted-by":"crossref","unstructured":"Aceto, L., Achilleos, A., Francalanza, A., Ing\u00f3lfsd\u00f3ttir, A., Lehtinen, K.: Adventures in monitorability: from branching to linear time and back again. Proc. ACM Program. Lang. 3(POPL), 52:1\u201352:29 (2019)","DOI":"10.1145\/3290365"},{"key":"16_CR5","unstructured":"Aceto, L., Achilleos, A., Francalanza, A., Ing\u00f3lfsd\u00f3ttir, A., Lehtinen, K.: The best a monitor can do. In: Baier, C., Goubault-Larrecq, J. (eds.) 29th EACSL Annual Conference on Computer Science Logic, CSL 2021. LIPIcs, Ljubljana, Slovenia, 25\u201328 January 2021, (Virtual Conference), vol. 183, pp. 7:1\u20137:23. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2021)"},{"issue":"2","key":"16_CR6","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1007\/s10270-020-00860-z","volume":"20","author":"L Aceto","year":"2021","unstructured":"Aceto, L., Achilleos, A., Francalanza, A., Ing\u00f3lfsd\u00f3ttir, A., Lehtinen, K.: An operational guide to monitorability with applications to regular properties. Softw. Syst. Model. 20(2), 335\u2013361 (2021). https:\/\/doi.org\/10.1007\/s10270-020-00860-z","journal-title":"Softw. Syst. Model."},{"key":"16_CR7","volume-title":"Probability & Measure Theory","author":"RB Ash","year":"1999","unstructured":"Ash, R.B., Dol\u00e9ans-Dade, C.A.: Probability & Measure Theory, 2nd edn. Harcourt\/Academic Press, Cambridge (1999)","edition":"2"},{"key":"16_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/978-3-030-78089-0_14","volume-title":"Formal Techniques for Distributed Objects, Components, and Systems","author":"DP Attard","year":"2021","unstructured":"Attard, D.P., Aceto, L., Achilleos, A., Francalanza, A., Ing\u00f3lfsd\u00f3ttir, A., Lehtinen, K.: Better late than never or: verifying asynchronous components at runtime. In: Peters, K., Willemse, T.A.C. (eds.) FORTE 2021. LNCS, vol. 12719, pp. 207\u2013225. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-78089-0_14"},{"key":"16_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/978-3-319-66197-1_14","volume-title":"Software Engineering and Formal Methods","author":"DP Attard","year":"2017","unstructured":"Attard, D.P., Francalanza, A.: Trace partitioning and local monitoring for asynchronous components. In: Cimatti, A., Sirjani, M. (eds.) SEFM 2017. LNCS, vol. 10469, pp. 219\u2013235. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66197-1_14"},{"key":"16_CR10","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"16_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-319-75632-5_1","volume-title":"Lectures on Runtime Verification","author":"E Bartocci","year":"2018","unstructured":"Bartocci, E., Falcone, Y., Francalanza, A., Reger, G.: Introduction to runtime verification. In: Bartocci, E., Falcone, Y. (eds.) Lectures on Runtime Verification. LNCS, vol. 10457, pp. 1\u201333. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-75632-5_1"},{"key":"16_CR12","volume-title":"Probability and Measure","author":"P Billingsley","year":"1995","unstructured":"Billingsley, P.: Probability and Measure, 3rd edn. Wiley-Interscience, Hoboken (1995)","edition":"3"},{"key":"16_CR13","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":"16_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1007\/978-3-030-78142-2_7","volume-title":"Coordination Models and Languages","author":"C Bartolo Burl\u00f2","year":"2021","unstructured":"Bartolo Burl\u00f2, C., Francalanza, A., Scalas, A., Trubiani, C., Tuosto, E.: Towards probabilistic session-type monitoring. In: Damiani, F., Dardha, O. (eds.) COORDINATION 2021. LNCS, vol. 12717, pp. 106\u2013120. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-78142-2_7"},{"key":"16_CR15","doi-asserted-by":"crossref","unstructured":"Chen, X., Sankaranarayanan, S.: Model predictive real-time monitoring of linear systems. In: Proceedings of the 2017 IEEE Real-Time Systems Symposium, RTSS 2017, pp. 297\u2013306. IEEE Computer Society (2017)","DOI":"10.1109\/RTSS.2017.00035"},{"key":"16_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/3-540-56287-7_93","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"M Dam","year":"1992","unstructured":"Dam, M.: Fixed points of B\u00fcchi automata. In: Shyamasundar, R. (ed.) FSTTCS 1992. LNCS, vol. 652, pp. 39\u201350. Springer, Heidelberg (1992). https:\/\/doi.org\/10.1007\/3-540-56287-7_93"},{"issue":"3","key":"16_CR17","doi-asserted-by":"publisher","first-page":"549","DOI":"10.1142\/S0129054108005814","volume":"19","author":"L Doyen","year":"2008","unstructured":"Doyen, L., Henzinger, T.A., Raskin, J.-F.: Equivalence of labeled Markov chains. Int. J. Found. Comput. Sci. 19(3), 549\u2013563 (2008)","journal-title":"Int. J. Found. Comput. Sci."},{"key":"16_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/978-3-030-00151-3_4","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"A Elgy\u00fctt","year":"2018","unstructured":"Elgy\u00fctt, A., Ferr\u00e8re, T., Henzinger, T.A.: Monitoring temporal logic with clock variables. In: Jansen, D.N., Prabhakar, P. (eds.) FORMATS 2018. LNCS, vol. 11022, pp. 53\u201370. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-00151-3_4"},{"key":"16_CR19","unstructured":"Esparza, J., Kiefer, S., Kret\u00ednsk\u00fd, J., Weininger, M.: Enforcing $$\\omega $$-regular properties in Markov chains by restarting. In: Haddad, S., Varacca, D. (eds.) Proceedings of the 32nd International Conference on Concurrency Theory, CONCUR 2021. LIPIcs, vol. 203, pp. 5:1\u20135:22. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2021)"},{"issue":"3","key":"16_CR20","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1007\/s10009-011-0196-8","volume":"14","author":"Y Falcone","year":"2012","unstructured":"Falcone, Y., Fernandez, J.-C., Mounier, L.: What can you verify and enforce at runtime? Int. J. Softw. Tools Technol. Transfer 14(3), 349\u2013382 (2012)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"16_CR21","unstructured":"Ferr\u00e8re, T., Henzinger, T.A., Kragl, B.: Monitoring event frequencies. In: Fern\u00e1ndez, M., Muscholl, A. (eds.) Proceedings of the 28th EACSL Annual Conference on Computer Science Logic, CSL 2020. LIPIcs, vol. 152, pp. 20:1\u201320:16. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2020)"},{"key":"16_CR22","doi-asserted-by":"crossref","unstructured":"Ferr\u00e8re, T., Henzinger, T.A., Sara\u00e7, N.E.: A theory of register monitors. In: Dawar, A., Gr\u00e4del, E. (eds.) Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2018, pp. 394\u2013403. ACM (2018)","DOI":"10.1145\/3209108.3209194"},{"key":"16_CR23","unstructured":"Francalanza, A.: Consistently-detecting monitors. In: Meyer, R., Nestmann, U. (eds.) 28th International Conference on Concurrency Theory, CONCUR 2017. LIPIcs, Berlin, Germany, 5\u20138 September 2017, vol. 85, pp. 8:1\u20138:19. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2017)"},{"key":"16_CR24","doi-asserted-by":"publisher","first-page":"104704","DOI":"10.1016\/j.ic.2021.104704","volume":"281","author":"A Francalanza","year":"2021","unstructured":"Francalanza, A.: A theory of monitors. Inf. Comput. 281, 104704 (2021)","journal-title":"Inf. Comput."},{"key":"16_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1007\/978-3-319-67531-2_2","volume-title":"Runtime Verification","author":"A Francalanza","year":"2017","unstructured":"Francalanza, A., et al.: A foundation for runtime monitoring. In: Lahiri, S., Reger, G. (eds.) RV 2017. LNCS, vol. 10548, pp. 8\u201329. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-67531-2_2"},{"issue":"1","key":"16_CR26","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/s10703-017-0273-z","volume":"51","author":"A Francalanza","year":"2017","unstructured":"Francalanza, A., Aceto, L., Ing\u00f3lfsd\u00f3ttir, A.: Monitorability for the Hennessy-Milner logic with recursion. Formal Methods Syst. Des. 51(1), 87\u2013116 (2017)","journal-title":"Formal Methods Syst. Des."},{"key":"16_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/978-3-540-93900-9_12","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"K Gondi","year":"2008","unstructured":"Gondi, K., Patel, Y., Sistla, A.P.: Monitoring the full range of $$\\omega $$-regular properties of stochastic systems. In: Jones, N.D., M\u00fcller-Olm, M. (eds.) VMCAI 2009. LNCS, vol. 5403, pp. 105\u2013119. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-93900-9_12"},{"issue":"1","key":"16_CR28","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1145\/2455.2460","volume":"32","author":"M Hennessy","year":"1985","unstructured":"Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. J. ACM 32(1), 137\u2013161 (1985)","journal-title":"J. ACM"},{"key":"16_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-60508-7_1","volume-title":"Runtime Verification","author":"TA Henzinger","year":"2020","unstructured":"Henzinger, T.A., Sara\u00e7, N.E.: Monitorability under assumptions. In: Deshmukh, J., Ni\u010dkovi\u0107, D. (eds.) RV 2020. LNCS, vol. 12399, pp. 3\u201318. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-60508-7_1"},{"key":"16_CR30","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Sara\u00e7, N.E.: Quantitative and approximate monitoring. In: Proceedings of the 36th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2021, pp. 1\u201314. IEEE (2021)","DOI":"10.1109\/LICS52264.2021.9470547"},{"key":"16_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"553","DOI":"10.1007\/978-3-030-81688-9_26","volume-title":"Computer Aided Verification","author":"S Junges","year":"2021","unstructured":"Junges, S., Torfah, H., Seshia, S.A.: Runtime monitors for Markov decision processes. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12760, pp. 553\u2013576. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_26"},{"key":"16_CR32","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D.: The PRISM benchmark suite. In: Proceedings of the Ninth International Conference on Quantitative Evaluation of Systems, QEST 2012, pp. 203\u2013204. IEEE Computer Society (2012)","DOI":"10.1109\/QEST.2012.14"},{"key":"16_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"422","DOI":"10.1007\/978-3-030-01090-4_25","volume-title":"Automated Technology for Verification and Analysis","author":"D Phan","year":"2018","unstructured":"Phan, D., Paoletti, N., Zhang, T., Grosu, R., Smolka, S.A., Stoller, S.D.: Neural state classification for hybrid systems. In: Lahiri, S.K., Wang, C. (eds.) ATVA 2018. LNCS, vol. 11138, pp. 422\u2013440. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-01090-4_25"},{"key":"16_CR34","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":"16_CR35","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":"16_CR36","unstructured":"Tao, T.: An Introduction to Measure Theory. Graduate Studies in Mathematics. American Mathematical Society, Providence (2013)"},{"key":"16_CR37","doi-asserted-by":"crossref","unstructured":"Vardi, M.Y.: Automatic verification of probabilistic concurrent finite-state programs. In: 26th Annual Symposium on Foundations of Computer Science, Portland, Oregon, USA, 21\u201323 October 1985, pp. 327\u2013338. IEEE Computer Society (1985)","DOI":"10.1109\/SFCS.1985.12"},{"key":"16_CR38","doi-asserted-by":"crossref","unstructured":"Vardi, M.Y.: A temporal fixpoint calculus. In: Ferrante, J., Mager, P. (eds.) Conference Record of the Fifteenth Annual ACM Symposium on Principles of Programming Languages, San Diego, California, USA, 10\u201313 January 1988, pp. 250\u2013259. ACM Press (1988)","DOI":"10.1145\/73560.73582"}],"container-title":["Lecture Notes in Computer Science","Principles of Systems Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-22337-2_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,11]],"date-time":"2024-10-11T02:55:14Z","timestamp":1728615314000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-22337-2_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031223365","9783031223372"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-22337-2_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"29 December 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}