{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,17]],"date-time":"2025-11-17T14:29:08Z","timestamp":1763389748164,"version":"3.37.3"},"reference-count":85,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2023,8,3]],"date-time":"2023-08-03T00:00:00Z","timestamp":1691020800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,8,3]],"date-time":"2023-08-03T00:00:00Z","timestamp":1691020800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"funder":[{"DOI":"10.13039\/501100001840","name":"Icelandic Centre for Research","doi-asserted-by":"publisher","award":["184776-051","163406-051"],"award-info":[{"award-number":["184776-051","163406-051"]}],"id":[{"id":"10.13039\/501100001840","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2023,12]]},"DOI":"10.1007\/s00236-023-00441-9","type":"journal-article","created":{"date-parts":[[2023,8,3]],"date-time":"2023-08-03T18:02:22Z","timestamp":1691085742000},"page":"385-451","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["On first-order runtime enforcement of branching-time properties"],"prefix":"10.1007","volume":"60","author":[{"given":"Luca","family":"Aceto","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5845-3753","authenticated-orcid":false,"given":"Ian","family":"Cassar","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":[]}],"member":"297","published-online":{"date-parts":[[2023,8,3]]},"reference":[{"key":"441_CR1","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1016\/j.ic.2021.104704","journal-title":"Inf. Comput."},{"issue":"1","key":"441_CR2","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. (TISSEC) 3(1), 30\u201350 (2000)","journal-title":"ACM Trans. Inf. Syst. Secur. (TISSEC)"},{"key":"441_CR3","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., Aceto, L., Achilleos, A., Attard, D.P., Cassar, I., Della Monica, D., Ing\u00f3lfsd\u00f3ttir, A.: A foundation for runtime monitoring. In: Lahiri, S., Reger, G. (eds.) Runtime Verification, pp. 8\u201329. Springer, Cham (2017)"},{"issue":"1","key":"441_CR4","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), 2\u201316 (2005)","journal-title":"Int. J. Inf. Secur."},{"key":"441_CR5","first-page":"87","volume-title":"CESORICS","author":"J Ligatti","year":"2010","unstructured":"Ligatti, J., Reddy, S.: A theory of runtime enforcement, with results. In: Gritzalis, D., Preneel, B., Theoharidou, M. (eds.) CESORICS, pp. 87\u2013100. Springer, Berlin (2010)"},{"issue":"3","key":"441_CR6","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/s10703-011-0114-4","volume":"38","author":"Y Falcone","year":"2011","unstructured":"Falcone, Y., Mounier, L., Fernandez, J.-C., Richier, J.-L.: Runtime enforcement monitors: composition, synthesis, and enforcement abilities. Formal Methods Syst. Des. 38(3), 223\u2013262 (2011)","journal-title":"Formal Methods Syst. Des."},{"key":"441_CR7","doi-asserted-by":"crossref","unstructured":"Berstel, J., Boasson, L.: Transductions and context-free languages. Ed. Teubner, pp. 1\u2013278 (1979)","DOI":"10.1007\/978-3-663-09367-1"},{"key":"441_CR8","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195218","volume-title":"Elements of Automata Theory","author":"J Sakarovitch","year":"2009","unstructured":"Sakarovitch, J.: Elements of Automata Theory. Cambridge University Press, New York (2009)"},{"key":"441_CR9","doi-asserted-by":"crossref","unstructured":"Alur, R., \u010cern\u00fd, P.: Streaming transducers for algorithmic verification of single-pass list-processing programs. In: Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 599\u2013610. ACM, ISBN 978-1-4503-0490-0 (2011)","DOI":"10.1145\/1925844.1926454"},{"issue":"2","key":"441_CR10","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1007\/s10703-017-0276-9","volume":"51","author":"B K\u00f6nighofer","year":"2017","unstructured":"K\u00f6nighofer, B., Alshiekh, M., Bloem, R., Humphrey, L., K\u00f6nighofer, R., Topcu, U., Wang, C.: Shield synthesis. Formal Methods Syst. Des. 51(2), 332\u2013361 (2017)","journal-title":"Formal Methods Syst. Des."},{"issue":"1","key":"441_CR11","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)","journal-title":"Formal Methods Syst. Des."},{"key":"441_CR12","first-page":"7:1","volume-title":"FSTTCS 2017: Foundations of Software Technology and Theoretical Computer Science, volume\u00a093 of LIPIcs","author":"L Aceto","year":"2018","unstructured":"Aceto, L., Achilleos, A., Francalanza, A., Ing\u00f3lfsd\u00f3ttir, A.: Monitoring for silent actions. In: Lokam, S., Ramanujam, R. (eds.) FSTTCS 2017: Foundations of Software Technology and Theoretical Computer Science, volume\u00a093 of LIPIcs, p. 7:1-7:14. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl (2018)"},{"key":"441_CR13","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.) Foundations of Software Science and Computation Structures, pp. 203\u2013220. Springer, Cham (2018)"},{"key":"441_CR14","first-page":"3","volume-title":"FORTE, volume 12719 of Lecture Notes in Computer Science","author":"L Aceto","year":"2021","unstructured":"Aceto, L., Cassar, I., Francalanza, A., Ing\u00f3lfsd\u00f3ttir, A.: On bidirectional runtime enforcement. In: Peters, K., Willemse, T.A.C. (eds.) FORTE, volume 12719 of Lecture Notes in Computer Science, pp. 3\u201321. Springer, Cham (2021)"},{"issue":"4","key":"441_CR15","doi-asserted-by":"publisher","first-page":"601","DOI":"10.1007\/s10009-021-00624-0","volume":"23","author":"L Aceto","year":"2021","unstructured":"Aceto, L., Cassar, I., Francalanza, A., Ing\u00f3lfsd\u00f3ttir, A.: Comparing controlled system synthesis and suppression enforcement. Int. J. Softw. Tools Technol. Transf. 23(4), 601\u2013614 (2021)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"441_CR16","first-page":"20:1","volume-title":"35th European Conference on Object-Oriented Programming, ECOOP 2021, July 11\u201317, 2021, Aarhus, Denmark (Virtual Conference), volume 194 of LIPIcs","author":"CB Burl\u00f2","year":"2021","unstructured":"Burl\u00f2, C.B., Francalanza, A., Scalas, A.: On the monitorability of session types, in theory and practice. In: M\u00f8ller, A., Sridharan, M. (eds.) 35th European Conference on Object-Oriented Programming, ECOOP 2021, July 11\u201317, 2021, Aarhus, Denmark (Virtual Conference), volume 194 of LIPIcs, p. 20:1-20:30. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl (2021)"},{"issue":"2\u20133","key":"441_CR17","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1016\/j.tcs.2004.11.007","volume":"336","author":"C Artho","year":"2005","unstructured":"Artho, C., Barringer, H., Goldberg, A., Havelund, K., Khurshid, S., Lowry, M.R., Pasareanu, C.S., Rosu, G., Sen, K., Visser, W., Washington, R.: Combining test case generation and runtime verification. Theoret. Comput. Sci. 336(2\u20133), 209\u2013234 (2005)","journal-title":"Theoret. Comput. Sci."},{"key":"441_CR18","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/978-3-319-67531-2_11","volume-title":"Runtime Verification (RV), LNCS","author":"A Desai","year":"2017","unstructured":"Desai, A., Dreossi, T., Seshia, S.A.: Combining model checking and runtime verification for safe robotics. In: Lahiri, S., Reger, G. (eds.) Runtime Verification (RV), LNCS, pp. 172\u2013189. Springer, Cham (2017)"},{"key":"441_CR19","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1016\/j.tcs.2017.02.009","volume":"669","author":"L Bocchi","year":"2017","unstructured":"Bocchi, L., Chen, T.-C., Demangeon, R., Honda, K., Yoshida, N.: Monitoring networks through multiparty session types. Theor. Comput. Sci. 669, 33\u201358 (2017)","journal-title":"Theor. Comput. Sci."},{"key":"441_CR20","doi-asserted-by":"crossref","unstructured":"Jia, L., Gommerstadt, H., Pfenning, F.: Monitors and blame assignment for higher-order session types. In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM, New York, pp. 582\u2013594 (2016)","DOI":"10.1145\/2837614.2837662"},{"key":"441_CR21","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/978-3-030-03769-7_15","volume-title":"Runtime Verification\u201418th International Conference, RV 2018, volume 11237 of Lecture Notes in Computer Science","author":"A Ferrando","year":"2018","unstructured":"Ferrando, A., Dennis, L.A., Ancona, D., Fisher, M., Mascardi, V.: Verifying and validating autonomous systems: towards an integrated approach. In: Colombo, C., Leucker, M. (eds.) Runtime Verification\u201418th International Conference, RV 2018, volume 11237 of Lecture Notes in Computer Science, pp. 263\u2013281. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-03769-7_15"},{"key":"441_CR22","volume-title":"Runtime Verification RV 2017","author":"K Kejstov\u00e1","year":"2017","unstructured":"Kejstov\u00e1, K., Ro\u010dkai, P., Barnat, J.: From model checking to runtime verification and back. In: Lahiri, S., Reger, G. (eds.) Runtime Verification RV 2017. Springer, Cham (2017)"},{"key":"441_CR23","doi-asserted-by":"publisher","first-page":"52:1","DOI":"10.1145\/3290365","volume":"3","author":"L Aceto","year":"2019","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, 52:1-52:29 (2019). https:\/\/doi.org\/10.1145\/3290365","journal-title":"Proc. ACM Program. Lang."},{"key":"441_CR24","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/978-3-642-58041-3_5","volume-title":"Logic and Algebra of Specification","author":"E Chang","year":"1993","unstructured":"Chang, E., Manna, Z., Pnueli, A.: The safety-progress classification. In: Bauer, F.L., et al. (eds.) Logic and Algebra of Specification, pp. 143\u2013202. Springer, Berlin (1993)"},{"key":"441_CR25","first-page":"573","volume-title":"International Symposium on Formal Methods","author":"A Pnueli","year":"2006","unstructured":"Pnueli, A., Zaks, A.: PSL model checking and run-time verification via testers. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) International Symposium on Formal Methods, pp. 573\u2013586. Springer, Berlin (2006)"},{"key":"441_CR26","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2020.100636","volume":"119","author":"A Francalanza","year":"2021","unstructured":"Francalanza, A., Cini, C.: Computer says no: verdict explainability for runtime monitors using a local proof system. J. Log. Algebraic Methods Program. 119, 100636 (2021). https:\/\/doi.org\/10.1016\/j.jlamp.2020.100636","journal-title":"J. Log. Algebraic Methods Program."},{"key":"441_CR27","doi-asserted-by":"publisher","first-page":"7:1","DOI":"10.4230\/LIPIcs.CSL.2021.7","volume-title":"29th EACSL Annual Conference on Computer Science Logic, CSL 2021, January 25\u201328, 2021, Ljubljana, Slovenia (Virtual Conference), volume 183 of LIPIcs","author":"L Aceto","year":"2021","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, January 25\u201328, 2021, Ljubljana, Slovenia (Virtual Conference), volume 183 of LIPIcs, p. 7:1-7:23. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, Dagstu (2021). https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2021.7"},{"issue":"3","key":"441_CR28","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 (2012)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"441_CR29","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. Theoret. Comput. Sci. 27, 333\u2013354 (1983)","journal-title":"Theoret. Comput. Sci."},{"issue":"2","key":"441_CR30","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)","journal-title":"Theor. Comput. Sci."},{"key":"441_CR31","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1007\/978-3-540-69850-0_12","volume-title":"25 Years of Model Checking","author":"EM Clarke","year":"2008","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) 25 Years of Model Checking, pp. 196\u2013215. Springer, Berlin (2008)"},{"issue":"2","key":"441_CR32","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":"441_CR33","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-540-77395-5_11","volume-title":"International Workshop on Runtime Verification","author":"A Bauer","year":"2007","unstructured":"Bauer, A., Leucker, M., Schallhart, C.: The good, the bad, and the ugly, but how ugly is ugly? In: Sokolsky, O., Tasiran, S. (eds.) International Workshop on Runtime Verification, pp. 126\u2013138. Springer, Berlin (2007)"},{"issue":"2\u20133","key":"441_CR34","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1016\/j.tcs.2004.11.007","volume":"336","author":"C Artho","year":"2005","unstructured":"Artho, C., Barringer, H., Goldberg, A., Havelund, K., Khurshid, S., Lowry, M.R., Pasareanu, C.S., Rosu, G., Sen, K., Visser, W., Washington, R.: Combining test case generation and runtime verification. Theor. Comput. Sci. 336(2\u20133), 209\u2013234 (2005)","journal-title":"Theor. Comput. Sci."},{"key":"441_CR35","first-page":"82","volume-title":"RV, volume 7687 of Lecture Notes in Computer Science","author":"M Leucker","year":"2012","unstructured":"Leucker, M.: Sliding between model checking and runtime verification. In: Qadeer, S., Tasiran, S. (eds.) RV, volume 7687 of Lecture Notes in Computer Science, pp. 82\u201387. Springer, Berlin (2012)"},{"key":"441_CR36","first-page":"459","volume-title":"NASA Formal Methods, volume 7871 of Lecture Notes in Computer Science","author":"N Decker","year":"2013","unstructured":"Decker, N., Leucker, M., Thoma, D.: junit$${}^{\\text{ rv }}$$-adding runtime verification to junit. In: Brat, G., Rungta, N., Venet, A. (eds.) NASA Formal Methods, volume 7871 of Lecture Notes in Computer Science, pp. 459\u2013464. Springer, Berlin (2013)"},{"key":"441_CR37","first-page":"172","volume-title":"RV, volume 10548 of Lecture Notes in Computer Science","author":"A Desai","year":"2017","unstructured":"Desai, A., Dreossi, T., Seshia, S.A.: Combining model checking and runtime verification for safe robotics. In: Lahiri, S., Reger, G. (eds.) RV, volume 10548 of Lecture Notes in Computer Science, pp. 172\u2013189. Springer, Cham (2017)"},{"key":"441_CR38","first-page":"225","volume-title":"RV, volume 10548 of Lecture Notes in Computer Science","author":"K Kejstov\u00e1","year":"2017","unstructured":"Kejstov\u00e1, K., Rockai, P., Barnat, J.: From model checking to runtime verification and back. In: Lahiri, S., Reger, G. (eds.) RV, volume 10548 of Lecture Notes in Computer Science, pp. 225\u2013240. Springer, Cham (2017)"},{"key":"441_CR39","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/978-3-030-21485-2_4","volume-title":"Models, Languages, and Tools for Concurrent and Distributed Programming, volume 11665 of Lecture Notes in Computer Science","author":"L Aceto","year":"2019","unstructured":"Aceto, L., Achilleos, A., Francalanza, A., Ing\u00f3lfsd\u00f3ttir, A., Lehtinen, K.: Testing equivalence vs. runtime monitoring. In: Boreale, M., Corradini, F., Loreti, M., Pugliese, R. (eds.) Models, Languages, and Tools for Concurrent and Distributed Programming, volume 11665 of Lecture Notes in Computer Science, pp. 28\u201344. Springer, Berlin (2019)"},{"key":"441_CR40","unstructured":"Monica, D.D, Francalanza, A.L.: Pushing runtime verification to the limit: may process semantics be with us. In: OVERLAY@AI*IA, volume 2509 of CEUR Workshop Proceedings, pp. 47\u201352. CEUR-WS.org (2019)"},{"key":"441_CR41","first-page":"107","volume-title":"RV, volume 12399 of Lecture Notes in Computer Science","author":"K Havelund","year":"2020","unstructured":"Havelund, K., Peled, D.: Bdds for representing data in runtime verification. In: Deshmukh, J., Nickovic, D. (eds.) RV, volume 12399 of Lecture Notes in Computer Science, pp. 107\u2013128. Springer, Cham (2020)"},{"key":"441_CR42","first-page":"279","volume-title":"RV, volume 12399 of Lecture Notes in Computer Science","author":"M Guzm\u00e1n","year":"2020","unstructured":"Guzm\u00e1n, M., Riganelli, O., Micucci, D., Mariani, L.: Test4enforcers: test case generation for software enforcers. In: Deshmukh, J., Nickovic, D. (eds.) RV, volume 12399 of Lecture Notes in Computer Science, pp. 279\u2013297. Springer, Cham (2020)"},{"key":"441_CR43","first-page":"227","volume-title":"FORTE, volume 12136 of Lecture Notes in Computer Science","author":"CB Burl\u00f2","year":"2020","unstructured":"Burl\u00f2, C.B., Francalanza, A., Scalas, A.: Towards a hybrid verification methodology for communication protocols (short paper). In: Gotsman, A., Sokolova, A. (eds.) FORTE, volume 12136 of Lecture Notes in Computer Science, pp. 227\u2013235. Springer, Cham (2020)"},{"key":"441_CR44","first-page":"100","volume-title":"RV, volume 12974 of Lecture Notes in Computer Science","author":"J Shijubo","year":"2021","unstructured":"Shijubo, J., Waga, M., Suenaga, K.: Efficient black-box checking via model checking with strengthened specifications. In: Feng, L., Fisman, D. (eds.) RV, volume 12974 of Lecture Notes in Computer Science, pp. 100\u2013120. Springer, Cham (2021)"},{"key":"441_CR45","unstructured":"Martinelli, F., Matteucci, I.: Partial model checking, process algebra operators and satisfiability procedures for (automatically) enforcing security properties. In: Foundations of Computer Security. Citeseer, pp. 133\u2013144 (2005)"},{"key":"441_CR46","doi-asserted-by":"crossref","unstructured":"Andersen, H.R.: Partial model checking. In: Proceedings of Tenth Annual IEEE Symposium on Logic in Computer Science. IEEE, pp. 398\u2013407 (1995)","DOI":"10.1109\/LICS.1995.523274"},{"key":"441_CR47","first-page":"141","volume-title":"TACAS","author":"F Lang","year":"2012","unstructured":"Lang, F., Mateescu, R.: Partial model checking using networks of labelled transition systems and Boolean equation systems. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS, pp. 141\u2013156. Springer, Berlin (2012)"},{"key":"441_CR48","doi-asserted-by":"publisher","first-page":"473","DOI":"10.1007\/978-3-319-46982-9_31","volume-title":"Runtime Verification","author":"DP Attard","year":"2016","unstructured":"Attard, D.P., Francalanza, A.: A monitoring tool for a branching-time logic. In: Falcone, Y., Sanchez, C. (eds.) Runtime Verification, pp. 473\u2013481. Springer, Cham (2016)"},{"key":"441_CR49","first-page":"49","volume-title":"A Runtime Monitoring Tool for Actor-Based Systems","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, pp. 49\u201374. River Publishers, Aalborg (2017)"},{"key":"441_CR50","first-page":"350","volume-title":"COORDINATION, volume 12134 of Lecture Notes in Computer Science","author":"A Francalanza","year":"2020","unstructured":"Francalanza, A., Xuereb, J.: On implementing symbolic controllability. In: Bliudze, S., Bocchi, L. (eds.) COORDINATION, volume 12134 of Lecture Notes in Computer Science, pp. 350\u2013369. Springer, Cham (2020)"},{"key":"441_CR51","doi-asserted-by":"publisher","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.) Formal Techniques for Distributed Objects, Components, and Systems\u201441st IFIP WG 6.1 International Conference, FORTE 2021, Held as Part of the 16th International Federated Conference on Distributed Computing Techniques, DisCoTec 2021, Valletta, Malta, June 14\u201318, 2021, Proceedings, volume 12719 of Lecture Notes in Computer Science, pp. 207\u2013225. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-78089-0_14","DOI":"10.1007\/978-3-030-78089-0_14"},{"key":"441_CR52","first-page":"181","volume-title":"COORDINATION, volume 13271 of Lecture Notes in Computer Science","author":"A Achilleos","year":"2022","unstructured":"Achilleos, A., Exibard, L., Francalanza, A., Lehtinen, K., Xuereb, J.: A synthesis tool for optimal monitors in a branching-time setting. In: ter Beek, M.H., Sirjani, M. (eds.) COORDINATION, volume 13271 of Lecture Notes in Computer Science, pp. 181\u2013199. Springer, Cham (2022)"},{"key":"441_CR53","first-page":"200","volume-title":"COORDINATION, volume 13271 of Lecture Notes in Computer Science","author":"L Aceto","year":"2022","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.H., Sirjani, M. (eds.) COORDINATION, volume 13271 of Lecture Notes in Computer Science, pp. 200\u2013219. Springer, Cham (2022)"},{"key":"441_CR54","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, September 4\u20137, 2018, Beijing, China, pp. 34:1\u201334:17 (2018). https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2018.34","DOI":"10.4230\/LIPIcs.CONCUR.2018.34"},{"issue":"1","key":"441_CR55","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(92)90008-4","volume":"100","author":"R Milner","year":"1992","unstructured":"Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes. I. Inf. Comput. 100(1), 1\u201340 (1992)","journal-title":"Inf. Comput."},{"key":"441_CR56","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511777110","volume-title":"Introduction to Bisimulation and Coinduction","author":"D Sangiorgi","year":"2011","unstructured":"Sangiorgi, D.: Introduction to Bisimulation and Coinduction. Cambridge University Press, New York (2011)"},{"key":"441_CR57","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 University Press, New York (2007)"},{"issue":"1","key":"441_CR58","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":"441_CR59","doi-asserted-by":"crossref","unstructured":"Stirling, C.: Handbook of logic in computer science, vol. 2. Modal and Temporal Logics, pp. 477\u2013563. Oxford University Press, Inc., New York (1992)","DOI":"10.1093\/oso\/9780198537618.003.0005"},{"key":"441_CR60","unstructured":"Stirling, C.: Model checking and other games. In: Notes for Mathfit Workshop on Finite Model Theory. University of Wales, Swansea (1996)"},{"key":"441_CR61","doi-asserted-by":"crossref","unstructured":"Francalanza, A.: A Theory of Monitors (extended abstract). In: International Conference on Foundations of Software Science and Computation Structures. Springer, pp. 145\u2013161 (2016)","DOI":"10.1007\/978-3-662-49630-5_9"},{"key":"441_CR62","unstructured":"Francalanza, A.: Consistently-detecting monitors. In: 28th International Conference on Concurrency Theory (CONCUR 2017), volume\u00a085 of Leibniz International Proceedings in Informatics (LIPIcs). Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Dagstuhl, pp. 8:1\u20138:19 (2017)"},{"key":"441_CR63","doi-asserted-by":"crossref","unstructured":"d\u2019Amorim, M., Ro\u015fu, G.: Efficient monitoring of $$\\omega $$-languages. In: CAV, pp. 364\u2013378 (2005)","DOI":"10.1007\/11513988_36"},{"key":"441_CR64","doi-asserted-by":"publisher","unstructured":"Wolff, E.M., Topcu, U., Murray, R.M.: Efficient reactive controller synthesis for a fragment of linear temporal logic. In: 2013 IEEE International Conference on Robotics and Automation, pp. 5033\u20135040, May (2013). https:\/\/doi.org\/10.1109\/ICRA.2013.6631296","DOI":"10.1109\/ICRA.2013.6631296"},{"issue":"1","key":"441_CR65","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/s10207-014-0239-8","volume":"14","author":"E Dolzhenko","year":"2015","unstructured":"Dolzhenko, E., Ligatti, J., Reddy, S.: Modeling runtime enforcement with mandatory results automata. Int. J. Inf. Secur. 14(1), 47\u201360 (2015). https:\/\/doi.org\/10.1007\/s10207-014-0239-8","journal-title":"Int. J. Inf. Secur."},{"key":"441_CR66","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/978-3-319-19249-9_10","volume-title":"FM 2015: Formal Methods","author":"S Debois","year":"2015","unstructured":"Debois, S., Hildebrandt, T., Slaats, T.: Safety, liveness and run-time refinement for modular process-aware information systems with dynamic sub processes. In: Bj\u00f8rner, N., de Boer, F. (eds.) FM 2015: Formal Methods, pp. 143\u2013160. Springer, Cham (2015)"},{"key":"441_CR67","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2019.100515","volume":"111","author":"L Aceto","year":"2020","unstructured":"Aceto, L., Achilleos, A., Francalanza, A., Ing\u00f3lfsd\u00f3ttir, A., Kjartansson, S.\u00d6.: Determinizing monitors for HML with recursion. J. Log. Algebraic Methods Program. 111, 100515 (2020). https:\/\/doi.org\/10.1016\/j.jlamp.2019.100515","journal-title":"J. Log. Algebraic Methods Program."},{"issue":"1","key":"441_CR68","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/s10626-016-0231-8","volume":"27","author":"AC van Hulst","year":"2017","unstructured":"van Hulst, A.C., Reniers, M.A., Fokkink, W.J.: Maximally permissive controlled system synthesis for non-determinism and modal logic. Discrete Event Dyn. Syst. 27(1), 109\u2013142 (2017)","journal-title":"Discrete Event Dyn. Syst."},{"key":"441_CR69","series-title":"PHI Series in Computer Science","volume-title":"Communication and Concurrency","author":"R Milner","year":"1989","unstructured":"Milner, R.: Communication and Concurrency. PHI Series in Computer Science, Prentice Hall, Upper Saddle River (1989)"},{"key":"441_CR70","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/978-3-642-19125-1_6","volume-title":"International Symposium on Engineering Secure Software and Systems","author":"N Bielova","year":"2011","unstructured":"Bielova, N., Massacci, F.: Predictability of enforcement. In: Erlingsson, U., Wieringa, R., Zannone, N. (eds.) International Symposium on Engineering Secure Software and Systems, pp. 73\u201386. Springer, Berlin (2011)"},{"key":"441_CR71","doi-asserted-by":"publisher","unstructured":"Attard, D.P., Francalanza, A.: Trace partitioning and local monitoring for asynchronous components. In: Cimatti, A., Sirjani, M. (eds.) Software Engineering and Formal Methods\u201415th International Conference, SEFM 2017, Trento, Italy, September 4\u20138, 2017, Proceedings, volume 10469 of Lecture Notes in Computer Science, pp. 219\u2013235. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66197-1_14","DOI":"10.1007\/978-3-319-66197-1_14"},{"key":"441_CR72","doi-asserted-by":"publisher","unstructured":"Aceto, L., Attard, D.P., Francalanza, A., Ing\u00f3lfsd\u00f3ttir, A.: On benchmarking for concurrent runtime verification. In: Guerra, E., Stoelinga, M. (eds.) Fundamental Approaches to Software Engineering\u201424th International Conference, FASE 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27\u2013April 1 (2021), Proceedings, volume 12649 of Lecture Notes in Computer Science, pp. 3\u201323. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-71500-7_1","DOI":"10.1007\/978-3-030-71500-7_1"},{"key":"441_CR73","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/3-540-49019-1_4","volume-title":"Foundations of Software Science and Computation Structures","author":"L Aceto","year":"1999","unstructured":"Aceto, L., Ing\u00f3lfsd\u00f3ttir, A.: Testing Hennessy\u2013Milner logic with recursion. In: Thomas, W. (ed.) Foundations of Software Science and Computation Structures, pp. 41\u201355. Springer, Berlin (1999)"},{"key":"441_CR74","doi-asserted-by":"publisher","first-page":"530","DOI":"10.1007\/3-540-58027-1_25","volume-title":"Proceedings of the 9th International Conference on Mathematical Foundations of Programming Semantics","author":"AM Rabinovich","year":"1994","unstructured":"Rabinovich, A.M.: A complete axiomatisation for trace congruence of finite state behaviors. In: Brookes, S., Main, M., Melton, A., Mislove, M., Schmidt, D. (eds.) Proceedings of the 9th International Conference on Mathematical Foundations of Programming Semantics, pp. 530\u2013543. Springer, London (1994)"},{"key":"441_CR75","unstructured":"Bielova, N.: A theory of constructive and predictable runtime enforcement mechanisms. Ph.D. Thesis, University of Trento (2011)"},{"key":"441_CR76","unstructured":"Pnueli, Z.M.A.: A hierarchy of temporal properties. In: Proceedings of the 2nd Symposium. ACM of Principle Of Distributed Computer (1990)"},{"key":"441_CR77","doi-asserted-by":"crossref","unstructured":"Pinisetty, S., Falcone, Y., J\u00e9ron, T., Marchand, H.: Runtime enforcement of parametric timed properties with practical applications. In: IEEE International Workshop on Discrete Event Systems, Cachan, France, May, pp. 46\u201353 (2014)","DOI":"10.1145\/2554850.2554967"},{"key":"441_CR78","doi-asserted-by":"crossref","unstructured":"Pinisetty, S., Roop, P.S., Smyth, S., Tripakis, S., von Hanxleden, R.: Runtime enforcement of reactive systems using synchronous enforcers. CoRR, arxiv:1612.05030 (2016)","DOI":"10.1145\/3092282.3092291"},{"issue":"5","key":"441_CR79","first-page":"178:1","volume":"16","author":"S Pinisetty","year":"2017","unstructured":"Pinisetty, S., Roop, P.S., Smyth, S., Allen, N., Tripakis, S., Hanxleden, R.V.: Runtime enforcement of cyber-physical systems. ACM Trans. Embed. Comput. Syst. 16(5), 178:1-178:25 (2017)","journal-title":"ACM Trans. Embed. Comput. Syst."},{"key":"441_CR80","doi-asserted-by":"publisher","unstructured":"Lanotte, R., Merro, M., Munteanu, A.: Runtime enforcement for control system security. In: 33rd IEEE Computer Security Foundations Symposium, CSF 2020, Boston, MA, USA, June 22\u201326, 2020. IEEE, pp. 246\u2013261 (2020). https:\/\/doi.org\/10.1109\/CSF49147.2020.00025","DOI":"10.1109\/CSF49147.2020.00025"},{"key":"441_CR81","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1016\/j.entcs.2006.08.029","volume":"179","author":"F Martinelli","year":"2006","unstructured":"Martinelli, F., Matteucci, I.: Through modeling to synthesis of security automata. Electron. Not. Theor. Comput. Sci. 179, 31\u201346 (2006)","journal-title":"Electron. Not. Theor. Comput. Sci."},{"key":"441_CR82","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1016\/j.entcs.2006.12.003","volume":"168","author":"F Martinelli","year":"2007","unstructured":"Martinelli, F., Matteucci, I.: An approach for the specification, verification and synthesis of secure systems. Electron. Not. Theor. Comput. Sci. 168, 29\u201343 (2007)","journal-title":"Electron. Not. Theor. Comput. Sci."},{"key":"441_CR83","doi-asserted-by":"crossref","unstructured":"Castellani, I., Dezani-Ciancaglini, M., P\u00e9rez, J.A.: Self-adaptation and secure information flow in multiparty communications. Formal Asp. Comput. 28 (4): 669-696 (2016)","DOI":"10.1007\/s00165-016-0381-3"},{"key":"441_CR84","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/978-3-319-33693-0_12","volume-title":"International Conference on Integrated Formal Methods","author":"I Cassar","year":"2016","unstructured":"Cassar, I., Francalanza, A.: On implementing a monitor-oriented programming framework for actor systems. In: Abraham, E., Huisman, M. (eds.) International Conference on Integrated Formal Methods, pp. 176\u2013192. Springer, Cham (2016)"},{"key":"441_CR85","first-page":"112","volume-title":"RV, volume 8174 of Lecture Notes in Computer Science","author":"A Francalanza","year":"2013","unstructured":"Francalanza, A., Seychell, A.: Synthesising correct concurrent runtime monitors (extended abstract). In: Legay, A., Bensalem, S. (eds.) RV, volume 8174 of Lecture Notes in Computer Science, vol. 8174, pp. 112\u2013129. Springer, Cham (2013)"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-023-00441-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00236-023-00441-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-023-00441-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,25]],"date-time":"2024-10-25T17:17:30Z","timestamp":1729876650000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s00236-023-00441-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,8,3]]},"references-count":85,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2023,12]]}},"alternative-id":["441"],"URL":"https:\/\/doi.org\/10.1007\/s00236-023-00441-9","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"type":"print","value":"0001-5903"},{"type":"electronic","value":"1432-0525"}],"subject":[],"published":{"date-parts":[[2023,8,3]]},"assertion":[{"value":"2 July 2019","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"1 June 2023","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"3 August 2023","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}