{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T21:56:02Z","timestamp":1777499762172,"version":"3.51.4"},"publisher-location":"Cham","reference-count":19,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032087065","type":"print"},{"value":"9783032087072","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,10,26]],"date-time":"2025-10-26T00:00:00Z","timestamp":1761436800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,10,26]],"date-time":"2025-10-26T00:00:00Z","timestamp":1761436800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-08707-2_7","type":"book-chapter","created":{"date-parts":[[2025,10,25]],"date-time":"2025-10-25T22:33:29Z","timestamp":1761431609000},"page":"135-156","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Prompt Runtime Enforcement"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0009-3754-630X","authenticated-orcid":false,"given":"Ayush","family":"Anand","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3843-5427","authenticated-orcid":false,"given":"Lo\u00efc","family":"Germerie Guizouarn","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9922-6186","authenticated-orcid":false,"given":"Thierry","family":"J\u00e9ron","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6473-3172","authenticated-orcid":false,"given":"Sayan","family":"Mukherjee","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7779-8231","authenticated-orcid":false,"given":"Srinivas","family":"Pinisetty","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8146-4429","authenticated-orcid":false,"given":"Ocan","family":"Sankur","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,10,26]]},"reference":[{"key":"7_CR1","doi-asserted-by":"crossref","unstructured":"Almagor, S., Hirshfeld, Y., Kupferman, O.: Promptness in $$\\omega $$-regular automata. In: Automated Technology for Verification and Analysis: 8th International Symposium, ATVA 2010, Singapore, September 21-24, 2010. Proceedings 8, pp. 22\u201336. Springer (2010)","DOI":"10.1007\/978-3-642-15643-4_4"},{"key":"7_CR2","unstructured":"Anand, A., Guizouarn, L.G., J\u00e9ron, T., Mukherjee, S., Pinisetty, S., Sankur, O.: Prompt runtime enforcement. https:\/\/github.com\/TimedProperties\/PromptEnforcement\/blob\/main\/Appendix\/appendix.pdf (2025). technical Appendix. Accessed 16 July 2025"},{"key":"7_CR3","doi-asserted-by":"publisher","first-page":"630","DOI":"10.1007\/978-3-030-25540-4_36","volume-title":"Computer Aided Verification","author":"G Avni","year":"2019","unstructured":"Avni, G., Bloem, R., Chatterjee, K., Henzinger, T.A., K\u00f6nighofer, B., Pranger, S.: Run-time optimization for learned controllers through quantitative games. In: Dillig, I., Tasiran, S. (eds.) Computer Aided Verification, pp. 630\u2013649. Springer International Publishing, Cham (2019)"},{"key":"7_CR4","doi-asserted-by":"crossref","unstructured":"Bloem, R., K\u00f6nighofer, B., K\u00f6nighofer, R., Wang, C.: Shield synthesis: runtime enforcement for reactive systems. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp. 533\u2013548. Springer (2015)","DOI":"10.1007\/978-3-662-46681-0_51"},{"key":"7_CR5","doi-asserted-by":"crossref","unstructured":"Dershowitz, N., Jayasimha, D., Park, S.: Bounded fairness. Verification: Theory and Practice: Essays Dedicated to Zohar Manna on the Occasion of His 64th Birthday, pp. 304\u2013317 (2003)","DOI":"10.1007\/978-3-540-39910-0_14"},{"issue":"3","key":"7_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. Design 38(3), 223\u2013262 (2011)","journal-title":"Formal Methods Syst. Design"},{"key":"7_CR7","unstructured":"Fijalkow, N., et\u00a0al.: Games on graphs. arXiv preprint arXiv:2305.10546 (2023)"},{"issue":"4","key":"7_CR8","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1007\/s11334-022-00480-4","volume":"19","author":"B K\u00f6nighofer","year":"2023","unstructured":"K\u00f6nighofer, B., Rudolf, J., Palmisano, A., Tappler, M., Bloem, R.: Online shielding for reinforcement learning. Innovations Syst. Softw. Eng. 19(4), 379\u2013394 (2023)","journal-title":"Innovations Syst. Softw. Eng."},{"key":"7_CR9","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":"7_CR10","doi-asserted-by":"crossref","unstructured":"Ligatti, J., Bauer, L., Walker, D.: Run-time enforcement of nonsafety policies. ACM Trans. Inf. Syst. Secur. 12(3) (2009)","DOI":"10.1145\/1455526.1455532"},{"issue":"7","key":"7_CR11","doi-asserted-by":"publisher","first-page":"4659","DOI":"10.1109\/TII.2019.2945520","volume":"16","author":"HA Pearce","year":"2020","unstructured":"Pearce, H.A., Pinisetty, S., Roop, P.S., Kuo, M.M.Y., Ukil, A.: Smart I\/O modules for mitigating cyber-physical attacks on industrial control systems. IEEE Trans. Ind. Inf. 16(7), 4659\u20134669 (2020)","journal-title":"IEEE Trans. Ind. Inf."},{"issue":"3","key":"7_CR12","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. Design 45(3), 381\u2013422 (2014). https:\/\/doi.org\/10.1007\/s10703-014-0215-y","journal-title":"Formal Methods Syst. Design"},{"key":"7_CR13","doi-asserted-by":"crossref","unstructured":"Pinisetty, S., Roop, P.S., Smyth, S., Allen, N., Tripakis, S., von Hanxleden, R.: Runtime enforcement of cyber-physical systems. ACM Trans. Embed. Comput. Syst. 16(5s), 178:1\u2013178:25 (2017). https:\/\/doi.org\/10.1145\/3126500","DOI":"10.1145\/3126500"},{"key":"7_CR14","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. In: Erdogmus, H., Havelund, K. (eds.) Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software, Santa Barbara, CA, USA, July 10-14, 2017, pp. 80\u201389. ACM (2017)","DOI":"10.1145\/3092282.3092291"},{"key":"7_CR15","doi-asserted-by":"crossref","unstructured":"Pradhan, A., Akil, C.G.M., Pinisetty, S.: Runtime enforcement with event reordering. In: Anutariya, C., Bonsangue, M.M. (eds.) Theoretical Aspects of Computing - ICTAC 2024 - 21st International Colloquium, Bangkok, Thailand, November 25-29, 2024, Proceedings. Lecture Notes in Computer Science, vol. 15373, pp. 386\u2013407. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-77019-7_22","DOI":"10.1007\/978-3-031-77019-7_22"},{"issue":"1","key":"7_CR16","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":"2","key":"7_CR17","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1137\/0201010","volume":"1","author":"R Tarjan","year":"1972","unstructured":"Tarjan, R.: Depth-first search and linear graph algorithms. SIAM J. Comput. 1(2), 146\u2013160 (1972)","journal-title":"SIAM J. Comput."},{"key":"7_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1007\/978-3-319-40648-0_6","volume-title":"NASA Formal Methods","author":"M Wu","year":"2016","unstructured":"Wu, M., Zeng, H., Wang, C.: Synthesizing runtime enforcer of safety properties under burst error. In: Rayadurgam, S., Tkachuk, O. (eds.) NFM 2016. LNCS, vol. 9690, pp. 65\u201381. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40648-0_6"},{"key":"7_CR19","unstructured":"Zuzak, I., Jankovic, V.: FSM simulator. https:\/\/ivanzuzak.info\/noam\/webapps\/fsm_simulator\/. Accessed 21 Apr 2025"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-08707-2_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,25]],"date-time":"2025-10-25T22:33:32Z","timestamp":1761431612000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-08707-2_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,26]]},"ISBN":["9783032087065","9783032087072"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-08707-2_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10,26]]},"assertion":[{"value":"26 October 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ATVA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Automated Technology for Verification and Analysis","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Bengaluru","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"India","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 October 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31 October 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"atva2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/atva-2025","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}