{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T21:55:31Z","timestamp":1777499731989,"version":"3.51.4"},"reference-count":31,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2017,2,23]],"date-time":"2017-02-23T00:00:00Z","timestamp":1487808000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2017,2,23]],"date-time":"2017-02-23T00:00:00Z","timestamp":1487808000000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100002341","name":"Suomen Akatemia","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100002341","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1139138"],"award-info":[{"award-number":["1139138"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1329759"],"award-info":[{"award-number":["1329759"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2017,8]]},"DOI":"10.1007\/s10703-017-0271-1","type":"journal-article","created":{"date-parts":[[2017,2,23]],"date-time":"2017-02-23T12:37:28Z","timestamp":1487853448000},"page":"154-199","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":21,"title":["Predictive runtime enforcement"],"prefix":"10.1007","volume":"51","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7779-8231","authenticated-orcid":false,"given":"Srinivas","family":"Pinisetty","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Viorel","family":"Preoteasa","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stavros","family":"Tripakis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thierry","family":"J\u00e9ron","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yli\u00e8s","family":"Falcone","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Herv\u00e9","family":"Marchand","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,2,23]]},"reference":[{"key":"271_CR1","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur R, Dill DL (1994) A theory of timed automata. Theor Comput Sci 126:183\u2013235. doi: 10.1016\/0304-3975(94)90010-8","journal-title":"Theor Comput Sci"},{"key":"271_CR2","doi-asserted-by":"publisher","unstructured":"Baier C, Bertrand N, Bouyer P, Brihaye T (2009) When are timed automata determinizable? In: Albers S, Marchetti-Spaccamela A, Matias Y, Nikoletseas SE, Thomas W (eds) 36th international colloquium on automata, languages and programming, ICALP 2009, Rhodes, Greece, July 5\u201312, 2009, proceedings, part II. Lecture notes in computer science, vol 5556. Springer, pp 43\u201354. doi: 10.1007\/978-3-642-02930-1_4","DOI":"10.1007\/978-3-642-02930-1_4"},{"key":"271_CR3","doi-asserted-by":"crossref","unstructured":"Bloem R, K\u00f6nighofer B, K\u00f6nighofer R, Wang C (2015) Shield synthesis: runtime enforcement for reactive systems. In: TACAS. LNCS, vol 9035. Springer, Berlin","DOI":"10.1007\/978-3-662-46681-0_51"},{"key":"271_CR4","volume-title":"Introduction to discrete event systems","author":"CG Cassandras","year":"2006","unstructured":"Cassandras CG, Lafortune S (2006) Introduction to discrete event systems. Springer, Secaucus"},{"issue":"4","key":"271_CR5","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1016\/j.cose.2010.11.004","volume":"30","author":"H Chabot","year":"2011","unstructured":"Chabot H, Khoury R, Tawbi N (2011) Extending the enforcement power of truncation monitors using static analysis. Comput Secur 30(4):194\u2013207","journal-title":"Comput Secur"},{"issue":"1","key":"271_CR6","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 (2015) Modeling runtime enforcement with mandatory results automata. Int J Inf Secur 14(1):47\u201360. doi: 10.1007\/s10207-014-0239-8","journal-title":"Int J Inf Secur"},{"issue":"7","key":"271_CR7","doi-asserted-by":"publisher","first-page":"1165","DOI":"10.1109\/TCAD.2008.923410","volume":"27","author":"V D\u2019Silva","year":"2008","unstructured":"D\u2019Silva V, Kroening D, Weissenbacher G (2008) A survey of automated techniques for formal software verification. IEEE Trans CAD Integr Circuits Syst 27(7):1165\u20131178. doi: 10.1109\/TCAD.2008.923410","journal-title":"IEEE Trans CAD Integr Circuits Syst"},{"issue":"1","key":"271_CR8","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1109\/52.976940","volume":"19","author":"D Evans","year":"2002","unstructured":"Evans D, Larochelle D (2002) Improving security using extensible lightweight static analysis. IEEE Softw 19(1):42\u201351. doi: 10.1109\/52.976940","journal-title":"IEEE Softw"},{"issue":"3","key":"271_CR9","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, Mounier L (2012) What can you verify and enforce at runtime? STTT 14(3):349\u2013382","journal-title":"STTT"},{"issue":"3","key":"271_CR10","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 JC, Richier JL (2011) Runtime enforcement monitors: composition, synthesis, and enforcement abilities. Form Methods Syst Des 38(3):223\u2013262","journal-title":"Form Methods Syst Des"},{"key":"271_CR11","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 (2016) Runtime enforcement of regular timed properties by suppressing and delaying events. Sci Comput Program 123:2\u201341","journal-title":"Sci Comput Program"},{"key":"#cr-split#-271_CR12.1","doi-asserted-by":"crossref","unstructured":"Finkel O (2006) Undecidable problems about timed automata. In: Asarin E, Bouyer P","DOI":"10.1007\/11867340_14"},{"key":"#cr-split#-271_CR12.2","unstructured":"(ed) Formal modeling and analysis of timed systems: 4th international conference, FORMATS 2006, Paris, France, September 25-27, 2006. Springer, Berlin, pp 187-199"},{"issue":"3","key":"271_CR13","doi-asserted-by":"publisher","first-page":"19:1","DOI":"10.1145\/1455526.1455532","volume":"12","author":"J Ligatti","year":"2009","unstructured":"Ligatti J, Bauer L, Walker D (2009) Run-time enforcement of nonsafety policies. ACM Trans Inf Syst Secur 12(3):19:1\u201319:41","journal-title":"ACM Trans Inf Syst Secur"},{"key":"271_CR14","doi-asserted-by":"crossref","unstructured":"Malan GR, Watson D, Jahanian F, Howell P (2000) Transport and application protocol scrubbing. In: Proceedings IEEE INFOCOM 2000, Israel, pp 1381\u20131390","DOI":"10.1109\/INFCOM.2000.832535"},{"key":"271_CR15","doi-asserted-by":"crossref","unstructured":"Nipkow T, Paulson LC, Wenzel M (2002) Isabelle\/HOL\u2014a proof assistant for higher-order logic. In: LNCS, vol 2283. Springer, Berlin","DOI":"10.1007\/3-540-45949-9"},{"key":"271_CR16","doi-asserted-by":"crossref","unstructured":"Pinisetty S, Falcone Y, J\u00e9ron T, Marchand H (2014) Runtime enforcement of parametric timed properties with practical applications. In: Lesage J, Faure J, Cury JER, Lennartson B (eds) 12th international workshop on discrete event systems, WODES 2014. International federation of automatic control, pp. 420\u2013427. http:\/\/www.ifac-papersonline.net\/Discrete_Event_Systems\/12th_International_Workshop_on_Discrete_Event_Systems__2014_\/index.html","DOI":"10.3182\/20140514-3-FR-4046.00041"},{"key":"271_CR17","doi-asserted-by":"crossref","unstructured":"Pinisetty S, Falcone Y, J\u00e9ron T, Marchand H (2014) Runtime enforcement of regular timed properties. In: Proceedings of the ACM symposium on applied computing (SAC-SVT). ACM, pp 1279\u20131286","DOI":"10.1145\/2554850.2554967"},{"key":"271_CR18","unstructured":"Pinisetty S, Falcone Y, J\u00e9ron T, Marchand H, Rollet A, Timo OLN (2012) Runtime enforcement of timed properties. In: Qadeer S, Tasiran S (eds) Proceedings of the third international conference on runtime verification (RV 2012). Lecture notes in computer science, vol 7687. Springer, Berlin, pp 229\u2013244"},{"issue":"3","key":"271_CR19","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 (2014) Runtime enforcement of timed properties revisited. Form Methods Syst Des 45(3):381\u2013422","journal-title":"Form Methods Syst Des"},{"key":"271_CR20","doi-asserted-by":"crossref","unstructured":"Pinisetty S, Preoteasa V, Tripakis S, J\u00e9ron T, Falcone Y, Marchand H (2016) Predictive runtime enforcement. In: Proceedings of the ACM symposium on applied computing (SAC-SVT). ACM (to appear)","DOI":"10.1145\/2851613.2851827"},{"key":"#cr-split#-271_CR21.1","doi-asserted-by":"crossref","unstructured":"Pitt J, Mamdani EH (1999) A protocol-based semantics for an agent communication language. In: Dean T","DOI":"10.1023\/A:1010016503852"},{"key":"#cr-split#-271_CR21.2","unstructured":"(ed) Proceedings of the sixteenth international joint conference on artificial intelligence, IJCAI 99, Stockholm, Sweden, July 31-August 6, 1999, 2 vol. Morgan Kaufmann, pp 486-491"},{"issue":"5","key":"271_CR22","doi-asserted-by":"publisher","first-page":"393","DOI":"10.1007\/s10009-009-0111-8","volume":"11","author":"H Raffelt","year":"2009","unstructured":"Raffelt H, Steffen B, Berg T, Margaria T (2009) Learnlib: a framework for extrapolating behavioral models. Int J Softw Tools Technol Transf 11(5):393\u2013407. doi: 10.1007\/s10009-009-0111-8","journal-title":"Int J Softw Tools Technol Transf"},{"key":"271_CR23","doi-asserted-by":"crossref","unstructured":"Renard M, Falcone Y, Rollet A, Pinisetty S, J\u00e9ron T, Marchand H (2015) Enforcement of (timed) properties with uncontrollable events. In: Leucker M, Rueda C, Valencia FD (eds) 12th international colloquium on theoretical aspects of computing\u2013ICTAC 2015, Cali, Colombia, October 29\u201331, 2015, proceedings. Lecture notes in computer science, vol 9399. Springer, Berlin, pp 542\u2013560","DOI":"10.1007\/978-3-319-25150-9_31"},{"issue":"2","key":"271_CR24","first-page":"327","volume":"22","author":"G Rosu","year":"2012","unstructured":"Rosu G (2012) On safety properties and their monitoring. Sci Ann Comput Sci 22(2):327\u2013365","journal-title":"Sci Ann Comput Sci"},{"issue":"1","key":"271_CR25","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1145\/353323.353382","volume":"3","author":"FB Schneider","year":"2000","unstructured":"Schneider FB (2000) Enforceable security policies. ACM Trans Inf Syst Secur 3(1):30\u201350. doi: 10.1145\/353323.353382","journal-title":"ACM Trans Inf Syst Secur"},{"issue":"6","key":"271_CR26","doi-asserted-by":"publisher","first-page":"222","DOI":"10.1016\/j.ipl.2006.04.015","volume":"99","author":"S Tripakis","year":"2006","unstructured":"Tripakis S (2006) Folk theorems on the determinization and minimization of timed automata. Inf Process Lett 99(6):222\u2013226. doi: 10.1016\/j.ipl.2006.04.015","journal-title":"Inf Process Lett"},{"key":"271_CR27","doi-asserted-by":"crossref","unstructured":"Tuglular T, Belli F (2009) Protocol-based testing of firewalls. In: 2009 fourth south-east European workshop on formal methods (SEEFM), pp 53\u201359","DOI":"10.1109\/SEEFM.2009.14"},{"key":"271_CR28","volume-title":"An introduction to multiagent systems","author":"M Wooldridge","year":"2009","unstructured":"Wooldridge M (2009) An introduction to multiagent systems, 2nd edn. Wiley Publishing, New York","edition":"2"},{"key":"271_CR29","doi-asserted-by":"crossref","unstructured":"Zhang X, Leucker M, Dong W (2012) Runtime verification with predictive semantics. In: 4th international symposium on NASA formal methods. LNCS, vol 7226. Springer, Berlin, pp 418\u2013432","DOI":"10.1007\/978-3-642-28891-3_37"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-017-0271-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-017-0271-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-017-0271-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,15]],"date-time":"2025-06-15T16:33:10Z","timestamp":1750005190000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-017-0271-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,2,23]]},"references-count":31,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2017,8]]}},"alternative-id":["271"],"URL":"https:\/\/doi.org\/10.1007\/s10703-017-0271-1","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,2,23]]},"assertion":[{"value":"23 February 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}