{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,14]],"date-time":"2026-03-14T22:22:41Z","timestamp":1773526961688,"version":"3.50.1"},"reference-count":67,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2021,2,5]],"date-time":"2021-02-05T00:00:00Z","timestamp":1612483200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,2,5]],"date-time":"2021-02-05T00:00:00Z","timestamp":1612483200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100001840","name":"Icelandic Centre for Research","doi-asserted-by":"publisher","award":["163406-51"],"award-info":[{"award-number":["163406-51"]}],"id":[{"id":"10.13039\/501100001840","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001840","name":"Icelandic Centre for Research","doi-asserted-by":"publisher","award":["184940-051"],"award-info":[{"award-number":["184940-051"]}],"id":[{"id":"10.13039\/501100001840","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/P020909\/1"],"award-info":[{"award-number":["EP\/P020909\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002347","name":"Bundesministerium f\u00fcr Bildung und Forschung","doi-asserted-by":"publisher","award":["01IS160253"],"award-info":[{"award-number":["01IS160253"]}],"id":[{"id":"10.13039\/501100002347","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100010686","name":"H2020 European Institute of Innovation and Technology","doi-asserted-by":"publisher","award":["778233"],"award-info":[{"award-number":["778233"]}],"id":[{"id":"10.13039\/100010686","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Softw Syst Model"],"published-print":{"date-parts":[[2021,4]]},"DOI":"10.1007\/s10270-020-00860-z","type":"journal-article","created":{"date-parts":[[2021,2,5]],"date-time":"2021-02-05T08:02:57Z","timestamp":1612512177000},"page":"335-361","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":17,"title":["An operational guide to monitorability with applications to regular properties"],"prefix":"10.1007","volume":"20","author":[{"given":"Luca","family":"Aceto","sequence":"first","affiliation":[]},{"given":"Antonis","family":"Achilleos","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3829-7391","authenticated-orcid":false,"given":"Adrian","family":"Francalanza","sequence":"additional","affiliation":[]},{"given":"Anna","family":"Ing\u00f3lfsd\u00f3ttir","sequence":"additional","affiliation":[]},{"given":"Karoliina","family":"Lehtinen","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,2,5]]},"reference":[{"key":"860_CR1","first-page":"7:1","volume-title":"FSTTCS, LIPIcs","author":"L Aceto","year":"2017","unstructured":"Aceto, L., Achilleos, A., Francalanza, A., Ing\u00f3lfsd\u00f3ttir, A.: Monitoring for silent actions. In: Lokam, S., Ramanujam, R. (eds.) FSTTCS, LIPIcs, vol. 93, pp. 7:1\u20137:14. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl (2017)"},{"key":"860_CR2","doi-asserted-by":"publisher","unstructured":"Aceto, L., Achilleos, A., Francalanza, A., Ing\u00f3lfsd\u00f3ttir, A.: A Framework for Parameterized Monitorability. In: Foundations of Software Science and Computation Structures\u201421st International Conference, FOSSACS 2018, LNCS, vol. 10803, pp. 203\u2013220 (2018). https:\/\/doi.org\/10.1007\/978-3-319-89366-2_11","DOI":"10.1007\/978-3-319-89366-2_11"},{"key":"860_CR3","unstructured":"Aceto, L., Achilleos, A., Francalanza, A., Ing\u00f3lfsd\u00f3ttir, A., Kjartansson, S.\u00d6.: Determinizing monitors for HML with recursion. CoRR (2016). arXiv:1611.10212"},{"key":"860_CR4","doi-asserted-by":"publisher","unstructured":"Aceto, L., Achilleos, A., Francalanza, A., Ing\u00f3lfsd\u00f3ttir, A., Kjartansson, S.\u00d6.: On the complexity of determinizing monitors. In: Carayol, A., Nicaud, C. (eds.) Implementation and Application of Automata\u201322nd International Conference, CIAA 2017, LNCS, vol. 10329, pp. 1\u201313. Springer, Berlin (2017). https:\/\/doi.org\/10.1007\/978-3-319-60134-2_1","DOI":"10.1007\/978-3-319-60134-2_1"},{"key":"860_CR5","unstructured":"Aceto, L., Achilleos, A., Francalanza, A., Ing\u00f3lfsd\u00f3ttir, A., Lehtinen, K.: Adventures in monitorability: from branching to linear time and back again. In: Proceedings of the ACM on Programming Languages, vol. 3, No. POPL, pp. 52:1\u201352:29 (2019). https:\/\/dl.acm.org\/citation.cfm?id=3290365"},{"key":"860_CR6","doi-asserted-by":"publisher","unstructured":"Aceto, L., Achilleos, A., Francalanza, A., Ing\u00f3lfsd\u00f3ttir, A., Lehtinen, K.: An operational guide to monitorability. In: \u00d6lveczky, P.C., Sala\u00fcn, G. (eds.) Software Engineering and Formal Methods\u201317th International Conference, SEFM 2019, Oslo, Norway, September 18\u201320, 2019, Proceedings. Lecture Notes in Computer Science, vol. 11724, pp. 433\u2013453. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-30446-1_23","DOI":"10.1007\/978-3-030-30446-1_23"},{"key":"860_CR7","doi-asserted-by":"publisher","unstructured":"Aceto, L., Cassar, I., Francalanza, A., Ing\u00f3lfsd\u00f3ttir, A.: On runtime enforcement via suppressions. In: 29th International Conference on Concurrency Theory, CONCUR 2018, LIPIcs, vol. 118, pp. 34:1\u201334:17. Schloss Dagstuhl (2018). https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2018.34","DOI":"10.4230\/LIPIcs.CONCUR.2018.34"},{"key":"860_CR8","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511814105","volume-title":"Reactive Systems: Modelling. Specification and Verification","author":"L Aceto","year":"2007","unstructured":"Aceto, L., Ing\u00f3lfsd\u00f3ttir, A., Larsen, K.G., Srba, J.: Reactive Systems: Modelling. Specification and Verification. Cambridge Univ. Press, New York (2007)"},{"issue":"4","key":"860_CR9","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1016\/0020-0190(85)90056-0","volume":"21","author":"B Alpern","year":"1985","unstructured":"Alpern, B., Schneider, F.B.: Defining liveness. Inf. Process. Lett. 21(4), 181\u2013185 (1985)","journal-title":"Inf. Process. Lett."},{"key":"860_CR10","volume-title":"Rudiments of $$\\mu $$-Calculus, Studies in Logic and the Foundations of Mathematics","author":"A Arnold","year":"2001","unstructured":"Arnold, A., Niwinski, D.: Rudiments of $$\\mu $$-Calculus, Studies in Logic and the Foundations of Mathematics, vol. 146. North-Holland, Amsterdam (2001)"},{"key":"860_CR11","first-page":"49","volume-title":"Behavioural Types: From Theory to Tools","author":"DP Attard","year":"2017","unstructured":"Attard, D.P., Cassar, I., Francalanza, A., Aceto, L., Ingolfsdottir, A.: A runtime monitoring tool for actor-based systems. In: Gay, S., Ravara, A. (eds.) Behavioural Types: From Theory to Tools, pp. 49\u201374. River Publishers, Gistrup (2017)"},{"key":"860_CR12","doi-asserted-by":"publisher","unstructured":"Attard, D.P., Francalanza, A.: A monitoring tool for a branching-time logic. In: Falcone, Y., S\u00e1nchez, C. (eds.) Runtime Verification\u201416th International Conference, RV 2016, LNCS, vol. 10012, pp. 473\u2013481. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-46982-9_31","DOI":"10.1007\/978-3-319-46982-9_31"},{"key":"860_CR13","unstructured":"Baier, C., Tinelli, C. (eds.): Tools and Algorithms for the Construction and Analysis of Systems\u201421st International Conference, TACAS 2015, LNCS, vol. 9035. Springer (2015)"},{"issue":"3","key":"860_CR14","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1093\/logcom\/exn076","volume":"20","author":"H Barringer","year":"2008","unstructured":"Barringer, H., Rydeheard, D., Havelund, K.: Rule systems for run-time monitoring: from Eagle to RuleR. J. Logic Comput. 20(3), 675\u2013706 (2008)","journal-title":"J. Logic Comput."},{"key":"860_CR15","doi-asserted-by":"publisher","unstructured":"Bartocci, E., Falcone, Y., Francalanza, A., Reger, G.: Introduction to runtime verification. In: Bartocci, E., Falcone, Y. (eds.) Lectures on Runtime Verification\u2014Introductory and Advanced Topics, LNCS, vol. 10457, pp. 1\u201333. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-75632-5_1","DOI":"10.1007\/978-3-319-75632-5_1"},{"issue":"3","key":"860_CR16","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. Logic Comput. 20(3), 651\u2013674 (2010)","journal-title":"J. Logic Comput."},{"issue":"4","key":"860_CR17","doi-asserted-by":"publisher","first-page":"14:1","DOI":"10.1145\/2000799.2000800","volume":"20","author":"A Bauer","year":"2011","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). https:\/\/doi.org\/10.1145\/2000799.2000800","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"issue":"4","key":"860_CR18","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1145\/2000799.2000800","volume":"20","author":"A Bauer","year":"2011","unstructured":"Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for LTL and TLTL. ACM Trans. Softw. Eng. Methodol. 20(4), 14 (2011)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"860_CR19","volume-title":"Systems and Software Verification: Model-Checking Techniques and Tools","author":"B B\u00e9rard","year":"2013","unstructured":"B\u00e9rard, B., Bidoit, M., Finkel, A., Laroussinie, F., Petit, A., Petrucci, L., Schnoebelen, P.: Systems and Software Verification: Model-Checking Techniques and Tools. Springer, Berlin (2013)"},{"issue":"4","key":"860_CR20","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/s10207-011-0137-2","volume":"10","author":"N Bielova","year":"2011","unstructured":"Bielova, N., Massacci, F.: Do you really mean what you actually enforced? Int. J. Inf. Secur. 10(4), 239\u2013254 (2011). https:\/\/doi.org\/10.1007\/s10207-011-0137-2","journal-title":"Int. J. Inf. Secur."},{"key":"860_CR21","doi-asserted-by":"publisher","unstructured":"Chang, E.Y., Manna, Z., Pnueli, A.: Characterization of temporal property classes. In: Kuich, W. (ed.) Automata, Languages and Programming, 19th International Colloquium, ICALP 1992, LNCS, vol. 623, pp. 474\u2013486. Springer (1992). https:\/\/doi.org\/10.1007\/3-540-55719-9_97","DOI":"10.1007\/3-540-55719-9_97"},{"key":"860_CR22","doi-asserted-by":"publisher","unstructured":"Chen, F., Rosu, G.: Mop: an efficient and generic runtime verification framework. In: Gabriel, R.P., Bacon, D.F., Lopes, C.V., Steele Jr., G.L. (eds.) Proceedings of the 22nd Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2007, pp. 569\u2013588. ACM (2007). https:\/\/doi.org\/10.1145\/1297027.1297069","DOI":"10.1145\/1297027.1297069"},{"key":"860_CR23","doi-asserted-by":"crossref","unstructured":"Chen, Z., Wu, Y., Wei, O., Sheng, B.: Poster: Deciding weak monitorability for runtime verification. In: 2018 IEEE\/ACM 40th International Conference on Software Engineering: Companion (ICSE-Companion), pp. 163\u2013164 (2018)","DOI":"10.1145\/3183440.3195077"},{"key":"860_CR24","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Tian, C., Tonetta, S.: Assumption-based runtime verification with partial observability and resets. In: International Conference on Runtime Verification, pp. 165\u2013184. Springer (2019)","DOI":"10.1007\/978-3-030-32079-9_10"},{"key":"860_CR25","doi-asserted-by":"publisher","unstructured":"Cini, C., Francalanza, A.: An LTL proof system for runtime verification. In: Baier and Tinelli [13], pp. 581\u2013595. https:\/\/doi.org\/10.1007\/978-3-662-46681-0_54","DOI":"10.1007\/978-3-662-46681-0_54"},{"key":"860_CR26","volume-title":"Model Checking","author":"EM Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"860_CR27","doi-asserted-by":"publisher","unstructured":"Convent, L., Hungerecker, S., Leucker, M., Scheffel, T., Schmitz, M., Thoma, D.: TeSSLa: temporal stream-based specification language. In: Formal Methods: Foundations and Applications\u201421st Brazilian Symposium, SBMF 2018, LNCS, vol. 11254, pp. 144\u2013162 (2018). https:\/\/doi.org\/10.1007\/978-3-030-03044-5_10","DOI":"10.1007\/978-3-030-03044-5_10"},{"key":"860_CR28","unstructured":"D\u2019Angelo, B., Sankaranarayanan, S., S\u00e1nchez, C., Robinson, W., Finkbeiner, B., Sipma, H.B., Mehrotra, S., Manna, Z.: Lola: Runtime monitoring of synchronous systems. In: 12th International Symposium on Temporal Representation and Reasoning (TIME\u201905), pp. 166\u2013174. IEEE Computer Society Press (2005)"},{"issue":"4","key":"860_CR29","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/s10009-014-0361-y","volume":"17","author":"A David","year":"2015","unstructured":"David, A., Larsen, K.G., Legay, A., Mikucionis, M., Poulsen, D.B.: Uppaal SMC tutorial. Int. J. Softw. Tools Technol. Transf. 17(4), 397\u2013415 (2015). https:\/\/doi.org\/10.1007\/s10009-014-0361-y","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"860_CR30","unstructured":"De Giacomo, G., Vardi, M.Y.: Linear temporal logic and linear dynamic logic on finite traces. In: Rossi, F. (ed.) IJCAI 2013, Proceedings of the 23rd International Joint Conference on Artificial Intelligence, pp. 854\u2013860. IJCAI\/AAAI (2013). http:\/\/www.aaai.org\/ocs\/index.php\/IJCAI\/IJCAI13\/paper\/view\/6997"},{"key":"860_CR31","doi-asserted-by":"publisher","unstructured":"Decker, N., Leucker, M., Thoma, D.: jUnit$${}^{\\text{rv}}$$-adding runtime verification to jUnit. In: NASA Formal Methods, 5th International Symposium, NFM, LNCS, vol. 7871, pp. 459\u2013464 (2013). https:\/\/doi.org\/10.1007\/978-3-642-38088-4_34","DOI":"10.1007\/978-3-642-38088-4_34"},{"key":"860_CR32","unstructured":"Diekert, V., Gastin, P.: First-order definable languages. In: Logic and Automata: History and Perspectives, Texts in Logic and Games, pp. 261\u2013306. Amsterdam University Press (2008)"},{"key":"860_CR33","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1016\/j.tcs.2014.02.052","volume":"537","author":"V Diekert","year":"2014","unstructured":"Diekert, V., Leucker, M.: Topology, monitorable properties and runtime verification. Theor. Comput. Sci. 537, 29\u201341 (2014). https:\/\/doi.org\/10.1016\/j.tcs.2014.02.052","journal-title":"Theor. Comput. Sci."},{"issue":"3","key":"860_CR34","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. Transf. 14(3), 349\u2013382 (2012)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"860_CR35","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1145\/3209108.3209194","DOI":"10.1145\/3209108.3209194"},{"key":"860_CR36","doi-asserted-by":"crossref","unstructured":"Francalanza, A.: A theory of monitors (extended abstract). In: Foundations of Software Science and Computation Structures\u201419th International Conference, FOSSACS, Eindhoven, The Netherlands, LNCS, vol. 9634, pp. 145\u2013161 (2016)","DOI":"10.1007\/978-3-662-49630-5_9"},{"key":"860_CR37","doi-asserted-by":"publisher","unstructured":"Francalanza, A.: Consistently-detecting monitors. In: 28th International Conference on Concurrency Theory (CONCUR), LIPIcs, vol.\u00a085, pp. 8:1\u20138:19. Schloss Dagstuhl (2017). https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2017.8","DOI":"10.4230\/LIPIcs.CONCUR.2017.8"},{"key":"860_CR38","doi-asserted-by":"publisher","unstructured":"Francalanza, A., Aceto, L., Achilleos, A., Attard, D.P., Cassar, I., Monica, D.D., Ing\u00f3lfsd\u00f3ttir, A.: A foundation for runtime monitoring. In: Runtime Verification\u201417th International Conference, RV 2017, LNCS, vol. 10548, pp. 8\u201329. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-67531-2_2","DOI":"10.1007\/978-3-319-67531-2_2"},{"issue":"1","key":"860_CR39","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\u2013Milner logic with recursion. Formal Methods Syst. Des. 51(1), 87\u2013116 (2017). https:\/\/doi.org\/10.1007\/s10703-017-0273-z","journal-title":"Formal Methods Syst. Des."},{"issue":"3","key":"860_CR40","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1007\/s10703-014-0217-9","volume":"46","author":"A Francalanza","year":"2015","unstructured":"Francalanza, A., Seychell, A.: Synthesising correct concurrent runtime monitors. Formal Methods Syst. Des. (FMSD) 46(3), 226\u2013261 (2015). https:\/\/doi.org\/10.1007\/s10703-014-0217-9","journal-title":"Formal Methods Syst. Des. (FMSD)"},{"key":"860_CR41","doi-asserted-by":"publisher","unstructured":"Francalanza, A., Xuereb, J.: On implementing symbolic controllability. In: Bliudze, S., Bocchi, L. (eds.) Coordination Models and Languages\u201422nd IFIP WG 6.1 International Conference, COORDINATION 2020, Lecture Notes in Computer Science, vol. 12134, pp. 350\u2013369. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-50029-0_22","DOI":"10.1007\/978-3-030-50029-0_22"},{"key":"860_CR42","doi-asserted-by":"publisher","unstructured":"Havelund, K., Peled, D.: Runtime verification: from propositional to first-order temporal logic. In: Runtime Verification\u201418th International Conference, RV 2018, Limassol, Cyprus, November 10\u201313, 2018, Proceedings, LNCS, vol. 11237, pp. 90\u2013112. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-030-03769-7_7","DOI":"10.1007\/978-3-030-03769-7_7"},{"issue":"1","key":"860_CR43","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). https:\/\/doi.org\/10.1145\/2455.2460","journal-title":"J. ACM"},{"issue":"1","key":"860_CR44","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1145\/568438.568455","volume":"32","author":"JE Hopcroft","year":"2001","unstructured":"Hopcroft, J.E., Motwani, R., Ullman, J.D.: Introduction to automata theory, languages, and computation. ACM Sigact News 32(1), 60\u201365 (2001)","journal-title":"ACM Sigact News"},{"key":"860_CR45","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"DC Kozen","year":"1983","unstructured":"Kozen, D.C.: Results on the propositional $$\\mu $$-calculus. Theor. Comput. Sci. 27, 333\u2013354 (1983)","journal-title":"Theor. Comput. Sci."},{"issue":"3","key":"860_CR46","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."},{"issue":"2","key":"860_CR47","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1145\/333979.333987","volume":"47","author":"O Kupferman","year":"2000","unstructured":"Kupferman, O., Vardi, M.Y., Wolper, P.: An automata-theoretic approach to branching-time model checking. J. ACM 47(2), 312\u2013360 (2000)","journal-title":"J. ACM"},{"issue":"2","key":"860_CR48","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1016\/0304-3975(90)90038-J","volume":"72","author":"KG Larsen","year":"1990","unstructured":"Larsen, K.G.: Proof systems for satisfiability in Hennessy\u2013Milner logic with recursion. Theor. Comput. Sci. 72(2), 265\u2013288 (1990). https:\/\/doi.org\/10.1016\/0304-3975(90)90038-J","journal-title":"Theor. Comput. Sci."},{"key":"860_CR49","doi-asserted-by":"publisher","unstructured":"Larsen, K.G., Lorber, F., Nielsen, B.: 20 years of UPPAAL enabled industrial model-based validation and beyond. In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification and Validation, Industrial Practice\u20148th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part IV, Lecture Notes in Computer Science, vol. 11247, pp. 212\u2013229. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-030-03427-6_18","DOI":"10.1007\/978-3-030-03427-6_18"},{"key":"860_CR50","doi-asserted-by":"crossref","unstructured":"Laurent, J., Goodloe, A., Pike, L.: Assuring the guardians. In: Runtime Verification (RV), LNCS, vol. 9333, pp. 87\u2013101 (2015)","DOI":"10.1007\/978-3-319-23820-3_6"},{"key":"860_CR51","doi-asserted-by":"crossref","unstructured":"Leucker, M.: Sliding between model checking and runtime verification. In: International Conference on Runtime Verification, pp. 82\u201387. Springer (2012)","DOI":"10.1007\/978-3-642-35632-2_10"},{"issue":"1\u20132","key":"860_CR52","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/s10207-004-0046-8","volume":"4","author":"J Ligatti","year":"2005","unstructured":"Ligatti, J., Bauer, L., Walker, D.: Edit automata: enforcement mechanisms for run-time security policies. Int. J. Inf. Secur. 4(1\u20132), 2\u201316 (2005). https:\/\/doi.org\/10.1007\/s10207-004-0046-8","journal-title":"Int. J. Inf. Secur."},{"issue":"1","key":"860_CR53","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1016\/0304-3975(91)90041-Y","volume":"83","author":"Z Manna","year":"1991","unstructured":"Manna, Z., Pnueli, A.: Completing the temporal picture. Theor. Comput. Sci. 83(1), 97\u2013130 (1991). https:\/\/doi.org\/10.1016\/0304-3975(91)90041-Y","journal-title":"Theor. Comput. Sci."},{"issue":"5","key":"860_CR54","doi-asserted-by":"publisher","first-page":"877","DOI":"10.1007\/s00165-017-0420-8","volume":"29","author":"R Neykova","year":"2017","unstructured":"Neykova, R., Bocchi, L., Yoshida, N.: Timed runtime monitoring for multiparty conversations. Formal Asp. Comput. 29(5), 877\u2013910 (2017). https:\/\/doi.org\/10.1007\/s00165-017-0420-8","journal-title":"Formal Asp. Comput."},{"key":"860_CR55","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1016\/0304-3975(87)90117-4","volume":"50","author":"I Phillips","year":"1987","unstructured":"Phillips, I.: Refusal testing. Theor. Comput. Sci. 50, 241\u2013284 (1987). https:\/\/doi.org\/10.1016\/0304-3975(87)90117-4","journal-title":"Theor. Comput. Sci."},{"key":"860_CR56","doi-asserted-by":"publisher","unstructured":"Pnueli, A., Zaks, A.: PSL model checking and run-time verification via testers. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006: Formal Methods, 14th International Symposium on Formal Methods, LNCS, vol. 4085, pp. 573\u2013586. Springer (2006). https:\/\/doi.org\/10.1007\/11813040_38","DOI":"10.1007\/11813040_38"},{"issue":"2","key":"860_CR57","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1147\/rd.32.0114","volume":"3","author":"MO Rabin","year":"1959","unstructured":"Rabin, M.O., Scott, D.: Finite automata and their decision problems. IBM J. Res. Dev. 3(2), 114\u2013125 (1959)","journal-title":"IBM J. Res. Dev."},{"key":"860_CR58","doi-asserted-by":"publisher","unstructured":"Reger, G., Cruz, H.C., Rydeheard, D.E.: MarQ: Monitoring at runtime with QEA. In: Baier and Tinelli [13], pp. 596\u2013610. https:\/\/doi.org\/10.1007\/978-3-662-46681-0_55","DOI":"10.1007\/978-3-662-46681-0_55"},{"issue":"2","key":"860_CR59","first-page":"327","volume":"22","author":"G Rosu","year":"2012","unstructured":"Rosu, G.: On safety properties and their monitoring. Sci. Ann. Comput. Sci. 22(2), 327\u2013365 (2012)","journal-title":"Sci. Ann. Comput. Sci."},{"key":"860_CR60","doi-asserted-by":"publisher","unstructured":"Safra, S.: Exponential determinization for $$\\omega $$-automata with strong-fairness acceptance condition (extended abstract). In: Proceedings of the Twenty-Fourth Annual ACM Symposium on Theory of Computing, STOC \u201992, pp. 275\u2013282. Association for Computing Machinery, New York, NY, USA (1992). https:\/\/doi.org\/10.1145\/129712.129739","DOI":"10.1145\/129712.129739"},{"key":"860_CR61","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/978-3-642-11319-2_22","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"C S\u00e1nchez","year":"2010","unstructured":"S\u00e1nchez, C., Leucker, M.: Regular linear temporal logic with past. In: Barthe, G., Hermenegildo, M. (eds.) Verification, Model Checking, and Abstract Interpretation, pp. 295\u2013311. Springer, Berlin Heidelberg (2010)"},{"issue":"1","key":"860_CR62","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1145\/353323.353382","volume":"3","author":"FB Schneider","year":"2000","unstructured":"Schneider, F.B.: Enforceable security policies. ACM Trans. Inf. Syst. Secur. 3(1), 30\u201350 (2000)","journal-title":"ACM Trans. Inf. Syst. Secur."},{"issue":"1","key":"860_CR63","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1006\/inco.1994.1028","volume":"110","author":"B Steffen","year":"1994","unstructured":"Steffen, B., Ing\u00f3lfsd\u00f3ttir, A.: Characteristic formulae for processes with divergence. Inf. Comput. 110(1), 149\u2013163 (1994). https:\/\/doi.org\/10.1006\/inco.1994.1028","journal-title":"Inf. Comput."},{"key":"860_CR64","doi-asserted-by":"publisher","first-page":"406","DOI":"10.1007\/978-3-030-30942-8_25","volume-title":"Formal Methods\u2014The Next 30 Years","author":"S Stucki","year":"2019","unstructured":"Stucki, S., S\u00e1nchez, C., Schneider, G., Bonakdarpour, B.: Gray-box monitoring of hyperproperties. In: ter Beek, M.H., McIver, A., Oliveira, J.N. (eds.) Formal Methods\u2014The Next 30 Years, pp. 406\u2013424. Springer, Cham (2019)"},{"key":"860_CR65","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1016\/B978-0-444-88074-1.50009-3","volume-title":"Formal Models and Semantics, Handbook of Theoretical Computer Science","author":"W Thomas","year":"1990","unstructured":"Thomas, W.: Chapter 4\u2013automata on infinite objects. In: Leeuwen, J.V. (ed.) Formal Models and Semantics, Handbook of Theoretical Computer Science, pp. 133\u2013191. Elsevier, Amsterdam (1990). https:\/\/doi.org\/10.1016\/B978-0-444-88074-1.50009-3"},{"key":"860_CR66","doi-asserted-by":"publisher","unstructured":"Viswanathan, M., Kim, M.: Foundations for the run-time monitoring of reactive systems\u2013fundamentals of the MaC language. In: Liu, Z., Araki, K. (eds.) Theoretical Aspects of Computing\u2014ICTAC 2004, First International Colloquium, LNCS, vol. 3407, pp. 543\u2013556. Springer (2004). https:\/\/doi.org\/10.1007\/978-3-540-31862-0_38","DOI":"10.1007\/978-3-540-31862-0_38"},{"issue":"1\/2","key":"860_CR67","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1016\/S0019-9958(83)80051-5","volume":"56","author":"P Wolper","year":"1983","unstructured":"Wolper, P.: Temporal logic can be more expressive. Inf. Control 56(1\/2), 72\u201399 (1983). https:\/\/doi.org\/10.1016\/S0019-9958(83)80051-5","journal-title":"Inf. Control"}],"container-title":["Software and Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-020-00860-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10270-020-00860-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-020-00860-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,10]],"date-time":"2021-04-10T06:09:50Z","timestamp":1618034990000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10270-020-00860-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,2,5]]},"references-count":67,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2021,4]]}},"alternative-id":["860"],"URL":"https:\/\/doi.org\/10.1007\/s10270-020-00860-z","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"value":"1619-1366","type":"print"},{"value":"1619-1374","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,2,5]]},"assertion":[{"value":"28 February 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"9 November 2020","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"18 December 2020","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"5 February 2021","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}