{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,8,10]],"date-time":"2024-08-10T04:36:21Z","timestamp":1723264581273},"reference-count":33,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2017,9,25]],"date-time":"2017-09-25T00:00:00Z","timestamp":1506297600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100002428","name":"Austrian Science Fund","doi-asserted-by":"publisher","award":["S11406-N23"],"id":[{"id":"10.13039\/501100002428","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,11]]},"DOI":"10.1007\/s10703-017-0276-9","type":"journal-article","created":{"date-parts":[[2017,9,25]],"date-time":"2017-09-25T11:36:03Z","timestamp":1506339363000},"page":"332-361","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":36,"title":["Shield synthesis"],"prefix":"10.1007","volume":"51","author":[{"ORCID":"http:\/\/orcid.org\/0000-0001-5183-5452","authenticated-orcid":false,"given":"Bettina","family":"K\u00f6nighofer","sequence":"first","affiliation":[]},{"given":"Mohammed","family":"Alshiekh","sequence":"additional","affiliation":[]},{"given":"Roderick","family":"Bloem","sequence":"additional","affiliation":[]},{"given":"Laura","family":"Humphrey","sequence":"additional","affiliation":[]},{"given":"Robert","family":"K\u00f6nighofer","sequence":"additional","affiliation":[]},{"given":"Ufuk","family":"Topcu","sequence":"additional","affiliation":[]},{"given":"Chao","family":"Wang","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,9,25]]},"reference":[{"key":"276_CR1","unstructured":"LTL Specification Patterns. \n http:\/\/patterns.projects.cis.ksu.edu\/documentation\/patterns\/ltl.shtml"},{"issue":"4","key":"276_CR2","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1016\/0020-0190(85)90056-0","volume":"21","author":"B Alpern","year":"1985","unstructured":"Alpern B, Schneider FB (1985) Defining liveness. Inf Process Lett 21(4):181\u2013185","journal-title":"Inf Process Lett"},{"issue":"3","key":"276_CR3","first-page":"261","volume":"36","author":"J Bernet","year":"2002","unstructured":"Bernet J, Janin D, Walukiewicz I (2002) Permissive strategies: from parity games to safety games. ITA 36(3):261\u2013275","journal-title":"ITA"},{"issue":"3\u20134","key":"276_CR4","doi-asserted-by":"crossref","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 TA, Hofferek G, Jobstmann B, K\u00f6nighofer B, K\u00f6nighofer R (2014) Synthesizing robust systems. Acta Inf 51(3\u20134):193\u2013220","journal-title":"Acta Inf"},{"key":"276_CR5","doi-asserted-by":"crossref","unstructured":"Bloem R, Chatterjee K, Greimel K, Henzinger TA, Jobstmann B (2010) Robustness in the presence of liveness. In: Proceedings of computer aided verification, 22nd international conference, CAV 2010, Edinburgh, 5\u201319 July 2010, pp 410\u2013424","DOI":"10.1007\/978-3-642-14295-6_36"},{"key":"276_CR6","doi-asserted-by":"publisher","unstructured":"Bloem R, Ehlers E, K\u00f6nighofer R (2015) Cooperative reactive synthesis. In: ATVA, LNCS, vol. 9364. Springer, pp 394\u2013410. doi:\n 10.1007\/978-3-319-24953-7","DOI":"10.1007\/978-3-319-24953-7"},{"issue":"3","key":"276_CR7","doi-asserted-by":"crossref","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 (2012) Synthesis of reactive(1) designs. J Comput Syst Sci 78(3):911\u2013938","journal-title":"J Comput Syst Sci"},{"key":"276_CR8","doi-asserted-by":"crossref","unstructured":"Bloem R, K\u00f6nighofer B, K\u00f6nighofer R, Wang C (2015) Shield synthesis: runtime enforcement for reactive systems. In: Tools and algorithms for the construction and analysis of systems\u201421st international conference, TACAS 2015, London, 11\u201318 Apr 2015, LNCS, vol. 9035. Springer, pp 533\u2013548","DOI":"10.1007\/978-3-662-46681-0_51"},{"key":"276_CR9","doi-asserted-by":"crossref","unstructured":"Brayton RK, Mishchenko A (2010) ABC: an academic industrial-strength verification tool. In: CAV, LNCS, vol 6174, Springer, pp 24\u201340","DOI":"10.1007\/978-3-642-14295-6_5"},{"issue":"8","key":"276_CR10","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"RE Bryant","year":"1986","unstructured":"Bryant RE (1986) Graph-based algorithms for boolean function manipulation. IEEE Trans Comput 35(8):677\u2013691","journal-title":"IEEE Trans Comput"},{"issue":"1","key":"276_CR11","doi-asserted-by":"crossref","first-page":"36","DOI":"10.1007\/s12555-010-0105-z","volume":"8","author":"H Chao","year":"2010","unstructured":"Chao H, Cao Y, Chen Y (2010) Autopilots for small unmanned aerial vehicles: a survey. Int J Control Autom Syst 8(1):36\u201344","journal-title":"Int J Control Autom Syst"},{"key":"276_CR12","doi-asserted-by":"crossref","unstructured":"Cimatti A, Roveri M, Schuppan V, Tchaltsev A (2008) Diagnostic information for realizability. In: Proceedings of verification, model checking, and abstract interpretation, 9th international conference, VMCAI 2008, San Francisco, 7\u20139 Jan 2008, pp 52\u201367","DOI":"10.1007\/978-3-540-78163-9_9"},{"key":"276_CR13","volume-title":"On integrating unmanned aircraft systems into the national airspace system: issues, challenges, operational restrictions, certification, and recommendations","author":"K Dalamagkidis","year":"2011","unstructured":"Dalamagkidis K, Valavanis KP, Piegl LA (2011) On integrating unmanned aircraft systems into the national airspace system: issues, challenges, operational restrictions, certification, and recommendations, vol 54. Springer, Berlin"},{"issue":"6","key":"276_CR14","doi-asserted-by":"crossref","first-page":"1180","DOI":"10.1109\/TSMCA.2010.2046731","volume":"40","author":"B Donmez","year":"2010","unstructured":"Donmez B, Nehme C, Cummings ML (2010) Modeling workload impact in multiple unmanned vehicle supervisory control. IEEE Trans Syst Man Cybern A Syst Hum 40(6):1180\u20131190","journal-title":"IEEE Trans Syst Man Cybern A Syst Hum"},{"key":"276_CR15","doi-asserted-by":"crossref","unstructured":"Duquette M (2009) Effects-level models for UAV simulation. In: AIAA modeling and simulation technologies conference","DOI":"10.2514\/6.2009-6139"},{"key":"276_CR16","doi-asserted-by":"crossref","unstructured":"Dwyer MB, Avrunin GS, Corbett JC (1999) Patterns in property specifications for finite-state verification. In: ICSE, ACM, pp 411\u2013420","DOI":"10.1145\/302405.302672"},{"key":"276_CR17","doi-asserted-by":"crossref","unstructured":"Ehlers R, K\u00f6nighofer R, Bloem R (2015) Synthesizing cooperative reactive mission plans. In: 2015 IEEE\/RSJ international conference on intelligent robots and systems, IROS 2015, Hamburg, 2015, IEEE, pp 3478\u20133485","DOI":"10.1109\/IROS.2015.7353862"},{"key":"276_CR18","doi-asserted-by":"publisher","unstructured":"Ehlers R, Topcu U (2014) Resilience to intermittent assumption violations in reactive synthesis. In: 17th international conference on hybrid systems: computation and control, HSCC\u201914, Berlin, 15\u201317 Apr 2014, ACM, pp 203\u2013212. doi:\n 10.1145\/2562059.2562128","DOI":"10.1145\/2562059.2562128"},{"key":"276_CR19","doi-asserted-by":"crossref","unstructured":"Faella M (2009) Admissible strategies in infinite games over graphs. In: Mathematical foundations of computer science 2009, 34th international symposium, MFCS 2009, Novy Smokovec, 2009, LNCS, vol. 5734. Springer, pp 307\u2013318","DOI":"10.1007\/978-3-642-03816-7_27"},{"issue":"3","key":"276_CR20","doi-asserted-by":"crossref","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"},{"key":"276_CR21","doi-asserted-by":"crossref","unstructured":"Feng L, Wiltsche C, Humphrey L, Topcu U (2016) Synthesis of human-in-the-loop control protocols for autonomous systems. In: IEEE\/RSJ international conference on intelligent robots and systems (IROS)","DOI":"10.1109\/TASE.2016.2530623"},{"key":"276_CR22","doi-asserted-by":"crossref","unstructured":"Humphrey L, K\u00f6nighofer B, K\u00f6nighofer R, Topcu U (2016) Synthesis of admissible shields. In: Proceedings of hardware and software: verification and testing\u201412th international haifa verification conference, HVC 2016, Haifa, 14\u201317 Nov 2016, pp 134\u2013151","DOI":"10.1007\/978-3-319-49052-6_9"},{"issue":"5\u20136","key":"276_CR23","doi-asserted-by":"crossref","first-page":"563","DOI":"10.1007\/s10009-011-0221-y","volume":"15","author":"R K\u00f6nighofer","year":"2013","unstructured":"K\u00f6nighofer R, Hofferek G, Bloem R (2013) Debugging formal specifications: a practical approach using model-based diagnosis and counterstrategies. STTT 15(5\u20136):563\u2013583","journal-title":"STTT"},{"issue":"5","key":"276_CR24","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1016\/j.jlap.2008.08.004","volume":"78","author":"M Leucker","year":"2009","unstructured":"Leucker M, Schallhart S (2009) A brief account of runtime verification. J Log Algebr Program 78(5):293\u2013303","journal-title":"J Log Algebr Program"},{"key":"276_CR25","doi-asserted-by":"crossref","unstructured":"Li W, Sadigh D, Sastry S, Seshia S (2014) Synthesis for human-in-the-loop control systems. In: Proceedings of tools and algorithms for the construction and analysis of systems\u201420th international conference, TACAS 2014, Grenoble, 5\u201313 Apr 2014, LNCS, vol. 8413. Springer, pp 470\u2013484","DOI":"10.1007\/978-3-642-54862-8_40"},{"issue":"1","key":"276_CR26","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/s10817-007-9084-z","volume":"40","author":"MH Liffiton","year":"2008","unstructured":"Liffiton MH, Sakallah KA (2008) Algorithms for computing minimal unsatisfiable subsets of constraints. J Autom Reason 40(1):1\u201333","journal-title":"J Autom Reason"},{"issue":"1","key":"276_CR27","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1109\/MAES.2009.4772749","volume":"24","author":"R Loh","year":"2009","unstructured":"Loh R, Bian Y, Roe T (2009) UAVs in civil airspace: safety requirements. IEEE Aerosp Electr Syst Mag 24(1):5\u201317","journal-title":"IEEE Aerosp Electr Syst Mag"},{"key":"276_CR28","doi-asserted-by":"crossref","first-page":"522","DOI":"10.1109\/9.664155","volume":"43","author":"J Lygeros","year":"1996","unstructured":"Lygeros J, Godbole DN, Sastry S (1996) Verified hybrid controllers for automated vehicles. IEEE Trans Autom Control 43:522\u2013539","journal-title":"IEEE Trans Autom Control"},{"key":"276_CR29","doi-asserted-by":"crossref","unstructured":"Mancini T, Mari F, Massini A, Melatti I, Tronci E (2014) Anytime system level verification via random exhaustive hardware in the loop simulation. In: 17th Euromicro conference on digital system design (DSD), 2014, pp 236\u2013245","DOI":"10.1109\/DSD.2014.91"},{"key":"276_CR30","doi-asserted-by":"publisher","unstructured":"Mazala R (2001) Infinite games. In: Gr\u00e4del E, Thomas W, Wilke T (eds) Automata, Logics, and Infinite Games: A Guide to Current Research [outcome of a Dagstuhl seminar, February 2001]. Lecture Notes in Computer Science, vol 2500, pp 23\u201342. Springer. doi:\n 10.1007\/3-540-36387-4_2","DOI":"10.1007\/3-540-36387-4_2"},{"key":"276_CR31","doi-asserted-by":"crossref","unstructured":"Piterman N, Pnueli A (2006) Faster solutions of Rabin and Streett games. In: 21st symposium on logic in computer science, IEEE press, pp 275\u2013284","DOI":"10.1109\/LICS.2006.23"},{"key":"276_CR32","doi-asserted-by":"crossref","unstructured":"Pnueli A (1977) The temporal logic of programs. In: 18th annual symposium on foundations of computer science, Providence, 31 Oct\u20131 Nov 1977, pp 46\u201357","DOI":"10.1109\/SFCS.1977.32"},{"key":"276_CR33","unstructured":"Pnueli A, Rosner R (1989) Automata, languages and programming. In: Proceedings of 16th international colloquium Stresa, 11\u201315 July 1989, chap. On the synthesis of an asynchronous reactive module, Springer, Berlin, Heidelberg, pp 652\u2013671"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-017-0276-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-017-0276-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-017-0276-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,11,15]],"date-time":"2017-11-15T16:29:03Z","timestamp":1510763343000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-017-0276-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,9,25]]},"references-count":33,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2017,11]]}},"alternative-id":["276"],"URL":"https:\/\/doi.org\/10.1007\/s10703-017-0276-9","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,9,25]]}}}