{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,8]],"date-time":"2026-07-08T22:30:16Z","timestamp":1783549816835,"version":"3.55.0"},"publisher-location":"Cham","reference-count":61,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031656293","type":"print"},{"value":"9783031656309","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T00:00:00Z","timestamp":1721865600000},"content-version":"vor","delay-in-days":206,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Modern software systems must comply with increasingly complex regulations in domains ranging from industrial automation to data protection. Runtime enforcement addresses this challenge by empowering systems to not only observe, but also actively control, the behavior of target systems by modifying their actions to ensure policy compliance. We propose a novel approach to the proactive real-time enforcement of policies expressed in metric first-order temporal logic (MFOTL). We introduce a new system model, define an expressive MFOTL fragment that is enforceable in that model,\u00a0and develop a sound enforcement algorithm for this fragment. We implement this algorithm in a\u00a0tool called<jats:sc>WhyEnf<\/jats:sc>and carry out a case study on enforcing GDPR-related policies. Our tool can enforce all policies from the study in real-time\u00a0with modest overhead. Our work thus provides the first tool-supported approach that can proactively enforce expressive first-order policies in real time.<\/jats:p>","DOI":"10.1007\/978-3-031-65630-9_8","type":"book-chapter","created":{"date-parts":[[2024,7,24]],"date-time":"2024-07-24T22:01:56Z","timestamp":1721858516000},"page":"156-181","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Proactive Real-Time First-Order Enforcement"],"prefix":"10.1007","author":[{"given":"Fran\u00e7ois","family":"Hublet","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Leonardo","family":"Lima","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"David","family":"Basin","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sr\u0111an","family":"Krsti\u0107","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Dmitriy","family":"Traytel","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2024,7,25]]},"reference":[{"key":"8_CR1","doi-asserted-by":"publisher","unstructured":"Abadi, M., Lamport, L., Wolper, P.: Realizable and unrealizable specifications of reactive systems. In: Ausiello, G., Dezani-Ciancaglini, M., Rocca, S.R.D. (eds.) 16th International Colloquium on Automata, Languages and Programming (ICALP). LNCS, vol.\u00a0372, pp. 1\u201317. Springer (1989). https:\/\/doi.org\/10.1007\/BFB0035748","DOI":"10.1007\/BFB0035748"},{"key":"8_CR2","unstructured":"Aceto, L., Cassar, I., Francalanza, A., Ing\u00f3lfsd\u00f3ttir, A.: On runtime enforcement via suppressions. In: 29th International Conference on Concurrency Theory (2018)"},{"key":"8_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-78089-0_1","volume-title":"Formal Techniques for Distributed Objects, Components, and Systems","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 2021. LNCS, vol. 12719, pp. 3\u201321. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-78089-0_1"},{"key":"8_CR4","doi-asserted-by":"crossref","unstructured":"Aceto, L., Cassar, I., Francalanza, A., Ingolfsdottir, A.: Bidirectional runtime enforcement of first-order branching-time properties. Logical Methods Comput. Sci. 19 (2023)","DOI":"10.46298\/lmcs-19(1:14)2023"},{"key":"8_CR5","doi-asserted-by":"crossref","unstructured":"Aceto, L., Cassar, I., Francalanza, A., Ing\u00f3lfsd\u00f3ttir, A.: On first-order runtime enforcement of branching-time properties. Acta Inform., 1\u201367 (2023)","DOI":"10.46298\/lmcs-19(1:14)2023"},{"issue":"4","key":"8_CR6","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. Inform. Process. Lett. 21(4), 181\u2013185 (1985)","journal-title":"Inform. Process. Lett."},{"key":"8_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"681","DOI":"10.1007\/978-3-030-29959-0_33","volume-title":"Computer Security \u2013 ESORICS 2019","author":"E Arfelt","year":"2019","unstructured":"Arfelt, E., Basin, D., Debois, S.: Monitoring the GDPR. In: Sako, K., Schneider, S., Ryan, P.Y.A. (eds.) ESORICS 2019. LNCS, vol. 11735, pp. 681\u2013699. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-29959-0_33"},{"key":"8_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-75632-5","volume-title":"Lectures on Runtime Verification","year":"2018","unstructured":"Bartocci, E., Falcone, Y. (eds.): Lectures on Runtime Verification. LNCS, vol. 10457. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-75632-5"},{"key":"8_CR9","doi-asserted-by":"publisher","unstructured":"Basin, D., et al.: VeriMon: a formally verified monitoring tool. In: Seidl, H., Liu, Z., Pasareanu, C.S. (eds.) 19th International Colloquium on Theoretical Aspects of Computing (ICTAC). LNCS, vol. 13572, pp.\u00a01\u20136. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-17715-6_1","DOI":"10.1007\/978-3-031-17715-6_1"},{"key":"8_CR10","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"432","DOI":"10.1007\/978-3-030-51074-9_25","volume-title":"Automated Reasoning","author":"D Basin","year":"2020","unstructured":"Basin, D., et al.: A formally verified, optimized monitor for metric first-order dynamic logic. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) IJCAR 2020. LNCS (LNAI), vol. 12166, pp. 432\u2013453. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-51074-9_25"},{"key":"8_CR11","doi-asserted-by":"crossref","unstructured":"Basin, D., Debois, S., Hildebrandt, T.T.: In the nick of time: proactive prevention of obligation violations. In: 29th Computer Security Foundations Symposium (CSF), pp. 120\u2013134. IEEE (2016)","DOI":"10.1109\/CSF.2016.16"},{"key":"8_CR12","unstructured":"Basin, D., Debois, S., Hildebrandt, T.: Proactive enforcement of provisions and obligations. J. Comput\/ Sec. (to appear)"},{"key":"8_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"360","DOI":"10.1007\/978-3-642-29860-8_27","volume-title":"Runtime Verification","author":"D Basin","year":"2012","unstructured":"Basin, D., Harvan, M., Klaedtke, F., Z\u0103linescu, E.: MONPOLY: monitoring usage-control policies. In: Khurshid, S., Sen, K. (eds.) RV 2011. LNCS, vol. 7186, pp. 360\u2013364. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-29860-8_27"},{"issue":"10","key":"8_CR14","doi-asserted-by":"publisher","first-page":"1403","DOI":"10.1109\/TSE.2013.18","volume":"39","author":"D Basin","year":"2013","unstructured":"Basin, D., Harvan, M., Klaedtke, F., Zalinescu, E.: Monitoring data usage in distributed systems. IEEE Trans. Softw. Eng. 39(10), 1403\u20131426 (2013)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"1","key":"8_CR15","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2487222.2487225","volume":"16","author":"D Basin","year":"2013","unstructured":"Basin, D., Jug\u00e9, V., Klaedtke, F., Z\u0103linescu, E.: Enforceable security policies revisited. ACM Trans. Inf. Syst. Secur. 16(1), 1\u201326 (2013)","journal-title":"ACM Trans. Inf. Syst. Secur."},{"key":"8_CR16","doi-asserted-by":"crossref","unstructured":"Basin, D., Klaedtke, F., Marinovic, S., Z\u0103linescu, E.: Monitoring of temporal first-order properties with aggregations. Formal Methods Syst. Des. 46, 262\u2013285 (2015)","DOI":"10.1007\/s10703-015-0222-7"},{"key":"8_CR17","unstructured":"Basin, D., Klaedtke, F., M\u00fcller, S., Pfitzmann, B.: Runtime monitoring of metric first-order temporal properties. In: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Schloss Dagstuhl-Leibniz-Zentrum f\u00fcr Informatik (2008)"},{"issue":"2","key":"8_CR18","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2699444","volume":"62","author":"D Basin","year":"2015","unstructured":"Basin, D., Klaedtke, F., M\u00fcller, S., Z\u0103linescu, E.: Monitoring metric first-order temporal properties. J. ACM (JACM) 62(2), 1\u201345 (2015)","journal-title":"J. ACM (JACM)"},{"key":"8_CR19","first-page":"19","volume":"3","author":"D Basin","year":"2017","unstructured":"Basin, D., Klaedtke, F., Zalinescu, E.: The MonPoly monitoring tool. RV-CuBES 3, 19\u201328 (2017)","journal-title":"RV-CuBES"},{"key":"8_CR20","doi-asserted-by":"publisher","unstructured":"Basin, D., Krsti\u0107, S., Schneider, J., Traytel, D.: Correct and efficient policy monitoring, a retrospective. In: 21st International Symposium on Automated Technology for Verification and Analysis (ATVA), pp. 3\u201330. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-45329-8_1","DOI":"10.1007\/978-3-031-45329-8_1"},{"key":"8_CR21","unstructured":"Bauer, L., Ligatti, J., Walker, D.: More enforceable security policies. In: Workshop on Foundations of Computer Security (FCS). Citeseer (2002)"},{"key":"8_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/978-3-540-73368-3_14","volume-title":"Computer Aided Verification","author":"G Behrmann","year":"2007","unstructured":"Behrmann, G., Cougnard, A., David, A., Fleury, E., Larsen, K.G., Lime, D.: UPPAAL-tiga: time for playing games! In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 121\u2013125. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73368-3_14"},{"issue":"2","key":"8_CR23","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1145\/210197.210200","volume":"20","author":"J Chomicki","year":"1995","unstructured":"Chomicki, J.: Efficient checking of temporal integrity constraints using bounded history encoding. ACM Trans. Database Syst. (TODS) 20(2), 149\u2013186 (1995)","journal-title":"ACM Trans. Database Syst. (TODS)"},{"key":"8_CR24","doi-asserted-by":"crossref","unstructured":"Debois, S., Slaats, T.: The analysis of a real life declarative process. In: 2015 IEEE Symposium Series on Computational Intelligence, pp. 1374\u20131382. IEEE (2015)","DOI":"10.1109\/SSCI.2015.196"},{"key":"8_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1007\/978-3-642-19835-9_25","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Ehlers","year":"2011","unstructured":"Ehlers, R.: Unbeast: symbolic bounded synthesis. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 272\u2013275. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-19835-9_25"},{"key":"8_CR26","doi-asserted-by":"crossref","unstructured":"Erlingsson, \u00da., Schneider, F.: SASI enforcement of security policies: a retrospective. In: Kienzle, D., Zurko, M.E., Greenwald, S., Serbau, C. (eds.) Workshop on New Security Paradigms, pp. 87\u201395. ACM (1999)","DOI":"10.1145\/335169.335201"},{"key":"8_CR27","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1016\/j.scico.2016.02.008","volume":"123","author":"Y Falcone","year":"2016","unstructured":"Falcone, Y., J\u00e9ron, T., Marchand, H., Pinisetty, S.: Runtime enforcement of regular timed properties by suppressing and delaying events. Sci. Comput. Program. 123, 2\u201341 (2016)","journal-title":"Sci. Comput. Program."},{"issue":"2","key":"8_CR28","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/s10009-021-00609-z","volume":"23","author":"Y Falcone","year":"2021","unstructured":"Falcone, Y., Krsti\u0107, S., Reger, G., Traytel, D.: A taxonomy for classifying runtime verification tools. Int. J. Softw. Tools Technol. Transf. 23(2), 255\u2013284 (2021)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"8_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/978-3-642-35632-2_23","volume-title":"Runtime Verification","author":"S Pinisetty","year":"2013","unstructured":"Pinisetty, S., Falcone, Y., J\u00e9ron, T., Marchand, H., Rollet, A., Nguena Timo, O.L.: Runtime enforcement of timed properties. In: Qadeer, S., Tasiran, S. (eds.) RV 2012. LNCS, vol. 7687, pp. 229\u2013244. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-35632-2_23"},{"key":"8_CR30","doi-asserted-by":"publisher","unstructured":"Feng, N., Marsso, L., Sabetzadeh, M., Chechik, M.: Early verification of legal compliance via bounded satisfiability checking. In: Enea, C., Lal, A. (eds.) CAV 2023. LNCS, vol. 13966, pp. 374\u2013396. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-37709-9_18","DOI":"10.1007\/978-3-031-37709-9_18"},{"key":"8_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"548","DOI":"10.1007\/978-3-642-31424-7_39","volume-title":"Computer Aided Verification","author":"M Fredrikson","year":"2012","unstructured":"Fredrikson, M., et al.: Efficient runtime policy enforcement using counterexample-guided abstraction refinement. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 548\u2013563. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_39"},{"key":"8_CR32","doi-asserted-by":"crossref","unstructured":"Gomaa, H.: Software modeling and design: UML, use cases, patterns, and software architectures. Cambridge University Press (2011)","DOI":"10.1017\/CBO9780511779183"},{"key":"8_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"648","DOI":"10.1007\/978-3-642-02658-4_50","volume-title":"Computer Aided Verification","author":"S Hall\u00e9","year":"2009","unstructured":"Hall\u00e9, S., Villemaire, R.: Browser-based enforcement of interface contracts in web applications with beepbeep. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 648\u2013653. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_50"},{"issue":"2","key":"8_CR34","doi-asserted-by":"publisher","first-page":"192","DOI":"10.1109\/TSC.2011.10","volume":"5","author":"S Hall\u00e9","year":"2012","unstructured":"Hall\u00e9, S., Villemaire, R.: Runtime enforcement of web service message contracts with data. IEEE Trans. Serv. Comput. 5(2), 192\u2013206 (2012)","journal-title":"IEEE Trans. Serv. Comput."},{"issue":"1\u20133","key":"8_CR35","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10703-018-00327-4","volume":"56","author":"K Havelund","year":"2020","unstructured":"Havelund, K., Peled, D., Ulus, D.: First-order temporal logic monitoring with bdds. Formal Methods Syst. Des. 56(1\u20133), 1\u201321 (2020)","journal-title":"Formal Methods Syst. Des."},{"issue":"5\u20137","key":"8_CR36","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1016\/j.jlap.2013.05.005","volume":"82","author":"T Hildebrandt","year":"2013","unstructured":"Hildebrandt, T., Mukkamala, R.R., Slaats, T., Zanitti, F.: Contracts for cross-organizational workflows as timed dynamic condition response graphs. J. Logic Algebraic Program. 82(5\u20137), 164\u2013185 (2013)","journal-title":"J. Logic Algebraic Program."},{"key":"8_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/11555827_7","volume-title":"Computer Security \u2013 ESORICS 2005","author":"M Hilty","year":"2005","unstructured":"Hilty, M., Basin, D., Pretschner, A.: On obligations. In: di Vimercati, S.C., Syverson, P., Gollmann, D. (eds.) ESORICS 2005. LNCS, vol. 3679, pp. 98\u2013117. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11555827_7"},{"key":"8_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-030-92124-8_2","volume-title":"Software Engineering and Formal Methods","author":"L Murphy","year":"2021","unstructured":"Murphy, L., Viger, T., Sandro, A.D., Shahin, R., Chechik, M.: Validating safety arguments with\u00a0lean. In: Calinescu, R., P\u0103s\u0103reanu, C.S. (eds.) SEFM 2021. LNCS, vol. 13085, pp. 23\u201343. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-92124-8_2"},{"key":"8_CR39","doi-asserted-by":"publisher","unstructured":"Hublet, F., Basin, D., Krsti\u0107, S.: Real-time policy enforcement with metric first-order temporal logic. In: European Symposium on Research in Computer Security. pp. 211\u2013232. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-17146-8_11","DOI":"10.1007\/978-3-031-17146-8_11"},{"key":"8_CR40","doi-asserted-by":"publisher","unstructured":"Hublet, F., Basin, D., Krsti\u0107, S.: Enforcing the GDPR. In: Tsudik, G., Conti, M., Liang, K., Smaragdakis, G. (eds.) Computer Security \u2013 ESORICS 2023. LNCS, vol. 14344. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-51476-0_20","DOI":"10.1007\/978-3-031-51476-0_20"},{"issue":"1","key":"8_CR41","doi-asserted-by":"publisher","first-page":"597","DOI":"10.56553\/popets-2024-0034","volume":"2024","author":"F Hublet","year":"2024","unstructured":"Hublet, F., Basin, D., Krsti\u0107, S.: User-controlled privacy: Taint, track, and control. Proc. Priv. Enhancing Technol. 2024(1), 597\u2013616 (2024)","journal-title":"Proc. Priv. Enhancing Technol."},{"key":"8_CR42","unstructured":"Hublet, F., Lima, L., Basin, D., Krsti\u0107, S., Traytel, D.: Proactive real-time first-order enforcement (extended report) (2024). https:\/\/github.com\/runtime-enforcement\/whyenf\/blob\/main\/docs\/cav24-extended.pdf"},{"key":"8_CR43","unstructured":"Hublet, F., Lima, L., Basin, D., Krsti\u0107, S., Traytel, D.: WhyEnf (2024). https:\/\/github.com\/runtime-enforcement\/whyenf"},{"key":"8_CR44","doi-asserted-by":"crossref","unstructured":"Jobstmann, B., Bloem, R.: Optimizations for LTL synthesis. In: International Conference Formal Methods in Computer-Aided Design (FMCAD), pp. 117\u2013124. IEEE (2006)","DOI":"10.1109\/FMCAD.2006.22"},{"key":"8_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"482","DOI":"10.1007\/978-3-030-60508-7_27","volume-title":"Runtime Verification","author":"S Krsti\u0107","year":"2020","unstructured":"Krsti\u0107, S., Schneider, J.: A benchmark generator for online first-order monitoring. In: Deshmukh, J., Ni\u010dkovi\u0107, D. (eds.) RV 2020. LNCS, vol. 12399, pp. 482\u2013494. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-60508-7_27"},{"key":"8_CR46","doi-asserted-by":"crossref","unstructured":"Li, G., Jensen, P., Larsen, K., Legay, A., Poulsen, D.: Practical controller synthesis for $$\\text{MTL}_{0,\\infty }$$. In: Erdogmus, H., Havelund, K. (eds.) ACM SIGSOFT International SPIN Symposium on Model Checking of Software, pp. 102\u2013111. ACM (2017)","DOI":"10.1145\/3092282.3092303"},{"key":"8_CR47","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, 2\u201316 (2005)","journal-title":"Int. J. Inf. Secur."},{"key":"8_CR48","doi-asserted-by":"publisher","unstructured":"Lima, L., Herasimau, A., Raszyk, M., Traytel, D., Yuan, S.: Explainable online monitoring of metric temporal logic. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp. 473\u2013491. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-30820-8_28","DOI":"10.1007\/978-3-031-30820-8_28"},{"key":"8_CR49","doi-asserted-by":"publisher","unstructured":"Lima, L., Huerta\u00a0y Munive, J.J., Traytel, D.: Explainable online monitoring of metric first-order temporal logic. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 288\u2013307. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-57246-3_16","DOI":"10.1007\/978-3-031-57246-3_16"},{"key":"8_CR50","doi-asserted-by":"publisher","unstructured":"Lima\u00a0Graf, J., Krsti\u0107, S., Schneider, J.: Metric first-order temporal logic with complex data types. In: International Conference on Runtime Verification. pp. 126\u2013147. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-44267-4_7","DOI":"10.1007\/978-3-031-44267-4_7"},{"key":"8_CR51","doi-asserted-by":"crossref","unstructured":"Ngo, M., Massacci, F., Milushev, D., Piessens, F.: Runtime enforcement of security policies on black box reactive programs. In: Rajamani, S.K., Walker, D. (eds.) 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pp. 43\u201354. ACM (2015)","DOI":"10.1145\/2676726.2676978"},{"key":"8_CR52","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"649","DOI":"10.1007\/978-3-642-22110-1_52","volume-title":"Computer Aided Verification","author":"H-J Peter","year":"2011","unstructured":"Peter, H.-J., Ehlers, R., Mattm\u00fcller, R.: Synthia: verification and synthesis for timed automata. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 649\u2013655. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_52"},{"key":"8_CR53","doi-asserted-by":"crossref","unstructured":"Pinisetty, S., Falcone, Y., J\u00e9ron, T., Marchand, H.: TiPEX: a tool chain for timed property enforcement during execution. In: International Conference on Runtime Verification (RV), pp. 306\u2013320. Springer (2015)","DOI":"10.1007\/978-3-319-23820-3_22"},{"key":"8_CR54","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1007\/s10703-014-0215-y","volume":"45","author":"S Pinisetty","year":"2014","unstructured":"Pinisetty, S., Falcone, Y., J\u00e9ron, T., Marchand, H., Rollet, A., Nguena Timo, O.: Runtime enforcement of timed properties revisited. Formal Methods Syst. Des. 45, 381\u2013422 (2014)","journal-title":"Formal Methods Syst. Des."},{"issue":"1","key":"8_CR55","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/s10703-017-0271-1","volume":"51","author":"S Pinisetty","year":"2017","unstructured":"Pinisetty, S., Preoteasa, V., Tripakis, S., J\u00e9ron, T., Falcone, Y., Marchand, H.: Predictive runtime enforcement. Formal Methods Syst. Des. 51(1), 154\u2013199 (2017)","journal-title":"Formal Methods Syst. Des."},{"key":"8_CR56","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: 16th ACM Symposium on Principles of Programming Languages (POPL), pp. 179\u2013190. ACM Press (1989)","DOI":"10.1145\/75277.75293"},{"key":"8_CR57","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1007\/978-3-319-67549-7_16","volume-title":"Testing Software and Systems","author":"M Renard","year":"2017","unstructured":"Renard, M., Rollet, A., Falcone, Y.: GREP: games for the runtime enforcement of properties. In: Yevtushenko, N., Cavalli, A.R., Yenig\u00fcn, H. (eds.) ICTSS 2017. LNCS, vol. 10533, pp. 259\u2013275. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-67549-7_16"},{"issue":"1","key":"8_CR58","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1145\/353323.353382","volume":"3","author":"F Schneider","year":"2000","unstructured":"Schneider, F.: Enforceable security policies. ACM Trans. Inf. Syst. Secur. 3(1), 30\u201350 (2000)","journal-title":"ACM Trans. Inf. Syst. Secur."},{"key":"8_CR59","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"310","DOI":"10.1007\/978-3-030-32079-9_18","volume-title":"Runtime Verification","author":"J Schneider","year":"2019","unstructured":"Schneider, J., Basin, D., Krsti\u0107, S., Traytel, D.: A formally verified monitor for metric first-order temporal logic. In: Finkbeiner, B., Mariani, L. (eds.) RV 2019. LNCS, vol. 11757, pp. 310\u2013328. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-32079-9_18"},{"key":"8_CR60","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-319-70389-3_10","volume-title":"Hardware and Software: Verification and Testing","author":"S Zhu","year":"2017","unstructured":"Zhu, S., Tabajara, L.M., Li, J., Pu, G., Vardi, M.Y.: A symbolic approach to safety ltl synthesis. In: HVC 2017. LNCS, vol. 10629, pp. 147\u2013162. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-70389-3_10"},{"key":"8_CR61","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/978-3-030-99527-0_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Zingg","year":"2022","unstructured":"Zingg, S., Krsti\u0107, S., Raszyk, M., Schneider, J., Traytel, D.: Verified first-order monitoring with recursive rules. In: TACAS 2022. LNCS, vol. 13244, pp. 236\u2013253. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99527-0_13"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-65630-9_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,24]],"date-time":"2024-11-24T19:46:40Z","timestamp":1732477600000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-65630-9_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031656293","9783031656309"],"references-count":61,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-65630-9_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"25 July 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Montreal, QC","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 July 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 July 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"36","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}