{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,7]],"date-time":"2026-05-07T02:45:19Z","timestamp":1778121919774,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662466803","type":"print"},{"value":"9783662466810","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-46681-0_51","type":"book-chapter","created":{"date-parts":[[2015,3,30]],"date-time":"2015-03-30T18:56:36Z","timestamp":1427741796000},"page":"533-548","source":"Crossref","is-referenced-by-count":90,"title":["Shield Synthesis:"],"prefix":"10.1007","author":[{"given":"Roderick","family":"Bloem","sequence":"first","affiliation":[]},{"given":"Bettina","family":"K\u00f6nighofer","sequence":"additional","affiliation":[]},{"given":"Robert","family":"K\u00f6nighofer","sequence":"additional","affiliation":[]},{"given":"Chao","family":"Wang","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"51_CR1","unstructured":"CUDD: CU Decision Diagram Package, \n                      \n                        ftp:\/\/vlsi.colorado.edu\/pub\/"},{"key":"51_CR2","unstructured":"LTL Specification Patterns, \n                      \n                        http:\/\/patterns.projects.cis.ksu.edu\/documentation\/patterns\/ltl.shtml"},{"key":"51_CR3","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/s00236-013-0191-5","volume":"51","author":"R. Bloem","year":"2014","unstructured":"Bloem, R., Chatterjee, K., Greimel, K., Henzinger, T., Hofferek, G., Jobstmann, B., K\u00f6nighofer, B., K\u00f6nighofer, R.: Synthesizing robust systems. Acta Inf.\u00a051, 193\u2013220 (2014)","journal-title":"Acta Inf."},{"issue":"3","key":"51_CR4","doi-asserted-by":"publisher","first-page":"911","DOI":"10.1016\/j.jcss.2011.08.007","volume":"78","author":"R. Bloem","year":"2012","unstructured":"Bloem, R., Jobstmann, B., Piterman, N., Pnueli, A., Sa\u2019ar, Y.: Synthesis of reactive(1) designs. J. Comput. Syst. Sci.\u00a078(3), 911\u2013938 (2012)","journal-title":"J. Comput. Syst. Sci."},{"key":"51_CR5","doi-asserted-by":"crossref","unstructured":"Bloem, R., K\u00f6nighofer, B., K\u00f6nighofer, R., Wang, C.: Shield synthesis: Runtime enforcement for reactive systems. CoRR, abs\/1501.02573\u00a002573 (2015)","DOI":"10.1007\/978-3-662-46681-0_51"},{"key":"51_CR6","unstructured":"Brayton, R.K., et al.: VIS: A system for verification and synthesis. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 428\u2013432. Springer, Heidelberg (1996)"},{"key":"51_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/978-3-642-14295-6_5","volume-title":"Computer Aided Verification","author":"R. Brayton","year":"2010","unstructured":"Brayton, R., Mishchenko, A.: ABC: An academic industrial-strength verification tool. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 24\u201340. Springer, Heidelberg (2010)"},{"key":"51_CR8","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1090\/S0002-9947-1969-0280205-0","volume":"138","author":"J.R. B\u00fcchi","year":"1969","unstructured":"B\u00fcchi, J.R., Landweber, L.H.: Solving sequential conditions by finite-state strategies. Trans. Amer. Math. Soc.\u00a0138, 367\u2013378 (1969)","journal-title":"Trans. Amer. Math. Soc."},{"key":"51_CR9","unstructured":"Church, A.: Logic, arithmetic, and automata. Int. Congr. Math, 23\u201335 (1962,1963)"},{"key":"51_CR10","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol.\u00a0131, pp. 52\u201371. Springer, Heidelberg (1982)","DOI":"10.1007\/BFb0025774"},{"key":"51_CR11","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: ICSE, pp. 411\u2013420. ACM (1999)","DOI":"10.1145\/302405.302672"},{"key":"51_CR12","doi-asserted-by":"crossref","unstructured":"Ehlers, R., Topcu, U.: Resilience to intermittent assumption violations in reactive synthesis. In: HSCC, pp. 203\u2013212. ACM (2014)","DOI":"10.1145\/2562059.2562128"},{"issue":"3","key":"51_CR13","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? STTT\u00a014(3), 349\u2013382 (2012)","journal-title":"STTT"},{"key":"51_CR14","doi-asserted-by":"crossref","unstructured":"Ligatti, J., Bauer, L., Walker, D.: Run-time enforcement of nonsafety policies. ACM Trans. Inf. Syst. Secur.\u00a012(3) (2009)","DOI":"10.1145\/1455526.1455532"},{"key":"51_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/3-540-36387-4_2","volume-title":"Automata, Logics, and Infinite Games","author":"R. Mazala","year":"2002","unstructured":"Mazala, R.: 2 infinite games. In: Gr\u00e4del, E., Thomas, W., Wilke, T. (eds.) Automata, Logics, and Infinite Games. LNCS, vol.\u00a02500, pp. 23\u201338. Springer, Heidelberg (2002)"},{"key":"51_CR16","unstructured":"Mead, C., Conway, L.: Introduction to VLSI systems. Addison-Wesley (1980)"},{"key":"51_CR17","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: POPL, pp. 179\u2013190. ACM (1989)","DOI":"10.1145\/75277.75293"},{"key":"51_CR18","series-title":"Lecture Notes in Computer Science","volume-title":"International Symposium on Programming","author":"J.P. Quielle","year":"1982","unstructured":"Quielle, J.P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Programming 1982. LNCS, vol.\u00a0137, Springer, Heidelberg (1982)"},{"key":"51_CR19","doi-asserted-by":"crossref","unstructured":"Rabin, M.O.: Automata on Infinite Objects and Church\u2019s Problem. In: Regional Conference Series in Mathematics, American Mathematical Society (1972)","DOI":"10.1090\/cbms\/013"},{"key":"51_CR20","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1145\/353323.353382","volume":"3","author":"F.B. Schneider","year":"2000","unstructured":"Schneider, F.B.: Enforceable security policies. ACM Trans. Inf. Syst. Secur.\u00a03, 30\u201350 (2000)","journal-title":"ACM Trans. Inf. Syst. Secur."}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-46681-0_51","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T23:34:25Z","timestamp":1558308865000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-46681-0_51"}},"subtitle":["Runtime Enforcement for Reactive Systems"],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662466803","9783662466810"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-46681-0_51","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]}}}