{"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":1777499731929,"version":"3.51.4"},"reference-count":29,"publisher":"Springer Science and Business Media LLC","issue":"1-3","license":[{"start":{"date-parts":[[2021,12,1]],"date-time":"2021-12-01T00:00:00Z","timestamp":1638316800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2021,12,1]],"date-time":"2021-12-01T00:00:00Z","timestamp":1638316800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"funder":[{"DOI":"10.13039\/501100004541","name":"Ministry of Human Resource Development","doi-asserted-by":"crossref","award":["SPARC Project Number 701"],"award-info":[{"award-number":["SPARC Project Number 701"]}],"id":[{"id":"10.13039\/501100004541","id-type":"DOI","asserted-by":"crossref"}]},{"name":"Indian Institute of Technology Bhubaneswar","award":["Seed grant SP093"],"award-info":[{"award-number":["Seed grant SP093"]}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["SaTC Award Number 1801546"],"award-info":[{"award-number":["SaTC Award Number 1801546"]}],"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":[[2021,12]]},"DOI":"10.1007\/s10703-022-00401-y","type":"journal-article","created":{"date-parts":[[2022,10,26]],"date-time":"2022-10-26T16:03:17Z","timestamp":1666800197000},"page":"205-252","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Compositional runtime enforcement revisited"],"prefix":"10.1007","volume":"59","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":"Ankit","family":"Pradhan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Partha","family":"Roop","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stavros","family":"Tripakis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,10,26]]},"reference":[{"issue":"POPL","key":"401_CR1","doi-asserted-by":"publisher","first-page":"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 (2019) Adventures in monitorability: from branching to linear time and back again. Proc ACM Program Lang 3(POPL):1\u201329","journal-title":"Proc ACM Program Lang"},{"issue":"2","key":"401_CR2","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 (2021) An operational guide to monitorability with applications to regular properties. Softw Syst Model 20(2):335\u2013361","journal-title":"Softw Syst Model"},{"issue":"3","key":"401_CR3","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1525880.1525882","volume":"18","author":"L Bauer","year":"2009","unstructured":"Bauer L, Ligatti J, Walker D (2009) Composing expressive runtime security policies. ACM Trans Softw Eng Methodol 18(3):1\u201343","journal-title":"ACM Trans Softw Eng Methodol"},{"key":"401_CR4","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","DOI":"10.1007\/978-3-662-46681-0_51"},{"key":"401_CR5","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 TC, Demangeon R, Honda K, Yoshida N (2017) Monitoring networks through multiparty session types. Theor Comput Sci 669:33\u201358","journal-title":"Theor Comput Sci"},{"key":"401_CR6","doi-asserted-by":"crossref","unstructured":"Clarke E, Long D, McMillan K (1989) Compositional model checking. In: Logic in computer science, 1989. LICS \u201989, Proceedings., Fourth annual symposium on, pp 353\u2013362","DOI":"10.1109\/LICS.1989.39190"},{"issue":"1","key":"401_CR7","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/s10270-013-0323-y","volume":"14","author":"Y Falcone","year":"2015","unstructured":"Falcone Y, Jaber M, Nguyen TH, Bozga M, Bensalem S (2015) Runtime verification of component-based systems in the BIP framework with formally-proved sound and complete instrumentation. Softw Syst Model 14(1):173\u2013199","journal-title":"Softw Syst Model"},{"issue":"3","key":"401_CR8","first-page":"223","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. FMSD 38(3):223\u2013262","journal-title":"FMSD"},{"key":"401_CR9","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"},{"issue":"3","key":"401_CR10","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1007\/s10703-014-0217-9","volume":"46","author":"A Francalanza","year":"2015","unstructured":"Francalanza A, Seychell A (2015) Synthesising correct concurrent runtime monitors. Form Methods Syst Des 46(3):226\u2013261","journal-title":"Form Methods Syst Des"},{"key":"401_CR11","doi-asserted-by":"crossref","unstructured":"Godefroid P (2007) Compositional dynamic test generation. In: Proceedings of the 34th annual ACM SIGPLAN-SIGACT, POPL, ACM, New York, pp 47\u201354","DOI":"10.1145\/1190215.1190226"},{"issue":"3","key":"401_CR12","doi-asserted-by":"publisher","first-page":"843","DOI":"10.1145\/177492.177725","volume":"16","author":"O Grumberg","year":"1994","unstructured":"Grumberg O, Long DE (1994) Model checking and modular verification. ACM Trans Program Lang Syst 16(3):843\u2013871","journal-title":"ACM Trans Program Lang Syst"},{"key":"401_CR13","doi-asserted-by":"publisher","first-page":"1591","DOI":"10.1631\/FITEE.2000203","volume":"21","author":"C Hu","year":"2020","unstructured":"Hu C, Dong W, Yang Y, Shi H, Deng F (2020) Decentralized runtime enforcement for robotic swarms. Front Inf Technol Electron Eng 21:1591\u20131606","journal-title":"Front Inf Technol Electron Eng"},{"issue":"2","key":"401_CR14","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 LR, K\u00f6nighofer R, Topcu U, Wang C (2017) Shield synthesis. Form Methods Syst Des 51(2):332\u2013361","journal-title":"Form Methods Syst Des"},{"key":"401_CR15","doi-asserted-by":"crossref","unstructured":"Kugler H, Segall I (2009) Compositional synthesis of reactive systems from live sequence chart specifications. In: TACAS, York, Proceedings, pp 77\u201391","DOI":"10.1007\/978-3-642-00768-2_9"},{"issue":"4","key":"401_CR16","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1016\/S1571-0661(04)80580-2","volume":"70","author":"J Levy","year":"2002","unstructured":"Levy J, Sa\u00efdi H, Uribe TE (2002) Combining monitors for runtime system verification. Electron Notes Theor Comput Sci 70(4):112\u2013127","journal-title":"Electron Notes Theor Comput Sci"},{"issue":"3","key":"401_CR17","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-19:41","journal-title":"ACM Trans Inf Syst Secur"},{"issue":"3","key":"401_CR18","first-page":"381","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. FMSD 45(3):381\u2013422","journal-title":"FMSD"},{"key":"401_CR19","doi-asserted-by":"crossref","unstructured":"Pinisetty S, Preoteasa V, Tripakis S, J\u00e9ron T, Falcone Y, Marchand H (2016) Predictive runtime enforcement. In: Symposium on applied computing (SAC-SVT). ACM","DOI":"10.1145\/2851613.2851827"},{"issue":"1","key":"401_CR20","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 (2017) Predictive runtime enforcement. Form Methods Syst Des 51(1):154\u2013199","journal-title":"Form Methods Syst Des"},{"issue":"5s","key":"401_CR21","doi-asserted-by":"publisher","first-page":"178:1","DOI":"10.1145\/3126500","volume":"16","author":"S Pinisetty","year":"2017","unstructured":"Pinisetty S, Roop PS, Smyth S, Allen N, Tripakis S, von Hanxleden R (2017) Runtime enforcement of cyber-physical systems. ACM Trans Embed Comput Syst 16(5s):178:1-178:25","journal-title":"ACM Trans Embed Comput Syst"},{"key":"401_CR22","doi-asserted-by":"publisher","unstructured":"Pinisetty S, Roop PS, Smyth S, Tripakis S, von Hanxleden R (2017) 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, ACM, pp 80\u201389 https:\/\/doi.org\/10.1145\/3092282.3092291","DOI":"10.1145\/3092282.3092291"},{"key":"401_CR23","doi-asserted-by":"crossref","unstructured":"Pinisetty S, Tripakis S (2016) Compositional runtime enforcement. In: NASA formal methods, Springer International Publishing, pp 82\u201399","DOI":"10.1007\/978-3-319-40648-0_7"},{"issue":"8","key":"401_CR24","doi-asserted-by":"publisher","first-page":"793","DOI":"10.1109\/TVLSI.2004.831467","volume":"12","author":"P Pop","year":"2004","unstructured":"Pop P, Eles P, Zebo P, Pop T (2004) Scheduling and mapping in an incremental design methodology for distributed real-time embedded systems. IEEE Trans Very Large Scale Integr (VLSI) Syst 12(8):793\u2013811","journal-title":"IEEE Trans Very Large Scale Integr (VLSI) Syst"},{"key":"401_CR25","doi-asserted-by":"publisher","unstructured":"Renard M, Rollet A, Falcone Y (2017) Runtime enforcement using b\u00fcchi games. In: Erdogmus H, Havelund K (eds) Proceedings of the 24th ACM SIGSOFT international SPIN symposium on model checking of software, Santa Barbara 2017, ACM, pp 70\u201379 https:\/\/doi.org\/10.1145\/3092282.3092296","DOI":"10.1145\/3092282.3092296"},{"key":"401_CR26","unstructured":"Samadi M, Ghassemi F, Khosravi R (2020) Decentralized runtime enforcement of message sequences in message-based systems. In: 24th International conference on principles of distributed systems, OPODIS 2020. LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, vol 184. pp 21:1\u201321:18"},{"issue":"1","key":"401_CR27","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","journal-title":"ACM Trans Inf Syst Secur"},{"issue":"1","key":"401_CR28","first-page":"13:1","volume":"20","author":"R Sinha","year":"2014","unstructured":"Sinha R, Girault A, Goessler G, Roop PS (2014) A formal approach to incremental converter synthesis for system-on-chip design. ACM Trans Des Autom Electr Syst 20(1):13:1-13:30","journal-title":"ACM Trans Des Autom Electr Syst"},{"issue":"5","key":"401_CR29","doi-asserted-by":"publisher","first-page":"960","DOI":"10.1109\/JPROC.2015.2510366","volume":"104","author":"S Tripakis","year":"2016","unstructured":"Tripakis S (2016) Compositionality in the science of system design. Proc IEEE 104(5):960\u2013972","journal-title":"Proc IEEE"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-022-00401-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-022-00401-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-022-00401-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,27]],"date-time":"2022-12-27T10:18:22Z","timestamp":1672136302000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-022-00401-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,12]]},"references-count":29,"journal-issue":{"issue":"1-3","published-print":{"date-parts":[[2021,12]]}},"alternative-id":["401"],"URL":"https:\/\/doi.org\/10.1007\/s10703-022-00401-y","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,12]]},"assertion":[{"value":"7 July 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"23 September 2022","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"26 October 2022","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}