{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T14:10:12Z","timestamp":1746195012524,"version":"3.40.3"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030393212"},{"type":"electronic","value":"9783030393229"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-39322-9_20","type":"book-chapter","created":{"date-parts":[[2020,1,14]],"date-time":"2020-01-14T19:03:59Z","timestamp":1579028639000},"page":"426-448","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["How to Win First-Order Safety Games"],"prefix":"10.1007","author":[{"given":"Helmut","family":"Seidl","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christian","family":"M\u00fcller","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bernd","family":"Finkbeiner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,1,13]]},"reference":[{"key":"20_CR1","doi-asserted-by":"publisher","first-page":"390","DOI":"10.1007\/BF01448035","volume":"110","author":"W Ackermann","year":"1935","unstructured":"Ackermann, W.: Untersuchungen \u00fcber das Eliminationsproblem der mathematischen Logik. Math. Ann. 110, 390\u2013413 (1935)","journal-title":"Math. Ann."},{"key":"20_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1007\/978-3-540-74407-8_6","volume-title":"CONCUR 2007 \u2013 Concurrency Theory","author":"L de Alfaro","year":"2007","unstructured":"de Alfaro, L., Roy, P.: Solving games via three-valued abstraction refinement. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 74\u201389. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-74407-8_6"},{"key":"20_CR3","doi-asserted-by":"crossref","unstructured":"Ball, T., et al.: Vericon: towards verifying controller programs in software-defined networks. In: ACM Sigplan Notices, vol. 49, pp. 282\u2013293. ACM (2014)","DOI":"10.1145\/2666356.2594317"},{"issue":"3\u20134","key":"20_CR4","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/BF01457985","volume":"86","author":"H Behmann","year":"1922","unstructured":"Behmann, H.: Beitr\u00e4ge zur Algebra der Logik, insbesondere zum Entscheidungsproblem. Math. Ann. 86(3\u20134), 163\u2013229 (1922)","journal-title":"Math. Ann."},{"key":"20_CR5","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/978-3-642-18216-7_9","volume-title":"Abstract State Machines","author":"E B\u00f6rger","year":"2003","unstructured":"B\u00f6rger, E., St\u00e4rk, R.: History and survey of ASM research. In: B\u00f6rger, E., St\u00e4rk, R. (eds.) Abstract State Machines, pp. 343\u2013367. Springer, Berlin (2003). https:\/\/doi.org\/10.1007\/978-3-642-18216-7_9"},{"key":"20_CR6","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/978-3-642-18216-7_8","volume-title":"Abstract State Machines","author":"E B\u00f6rger","year":"2003","unstructured":"B\u00f6rger, E., St\u00e4rk, R.: Tool support for ASMs. In: B\u00f6rger, E., St\u00e4rk, R. (eds.) Abstract State Machines, pp. 313\u2013342. Springer, Berlin (2003). https:\/\/doi.org\/10.1007\/978-3-642-18216-7_8"},{"key":"20_CR7","volume-title":"Knowledge Representation","author":"RJ Brachman","year":"1992","unstructured":"Brachman, R.J., Levesque, H.J., Reiter, R.: Knowledge Representation. MIT Press, Cambridge (1992)"},{"key":"20_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-642-18275-4_7","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"AR Bradley","year":"2011","unstructured":"Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 70\u201387. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-18275-4_7"},{"key":"20_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"20_CR10","unstructured":"Dimitrova, R., Finkbeiner, B.: Abstraction refinement for games with incomplete information. In: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science FSTTCS, vol. 2008, pp. 175\u2013186 (2008)"},{"key":"20_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-642-33365-1_9","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"R Dimitrova","year":"2012","unstructured":"Dimitrova, R., Finkbeiner, B.: Counterexample-guided synthesis of observation predicates. In: Jurdzi\u0144ski, M., Ni\u010dkovi\u0107, D. (eds.) FORMATS 2012. LNCS, vol. 7595, pp. 107\u2013122. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33365-1_9"},{"key":"20_CR12","doi-asserted-by":"publisher","unstructured":"Finkbeiner, B., M\u00fcller, C., Seidl, H., Zalinescu, E.: Verifying security policies in multi-agent workflows with loops. In: Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS 2017, Dallas, TX, USA, 30 October\u201303 November 2017, pp. 633\u2013645. IEEE (2017). https:\/\/doi.org\/10.1145\/3133956.3134080","DOI":"10.1145\/3133956.3134080"},{"key":"20_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/978-3-319-46520-3_11","volume-title":"Automated Technology for Verification and Analysis","author":"B Finkbeiner","year":"2016","unstructured":"Finkbeiner, B., Seidl, H., M\u00fcller, C.: Specifying and verifying secrecy in workflows with arbitrarily many agents. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 157\u2013173. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-46520-3_11"},{"key":"20_CR14","series-title":"Computational Aspects and Applications","volume-title":"Second Order Quantifier Elimination: Foundations","author":"DM Gabbay","year":"2008","unstructured":"Gabbay, D.M., Schmidt, R., Szalas, A.: Second Order Quantifier Elimination: Foundations. Computational Aspects and Applications. College Publications, Michigan (2008)"},{"key":"20_CR15","unstructured":"Gurevich, Y.: Evolving algebras 1993: Lipari guide. arXiv preprint arXiv:1808.06255 (2018)"},{"key":"20_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"886","DOI":"10.1007\/3-540-45061-0_69","volume-title":"Automata, Languages and Programming","author":"TA Henzinger","year":"2003","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R.: Counterexample-guided control. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. LNCS, vol. 2719, pp. 886\u2013902. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-45061-0_69"},{"issue":"1\u20132","key":"20_CR17","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1016\/j.tcs.2010.08.024","volume":"412","author":"M Holzer","year":"2011","unstructured":"Holzer, M., Kutrib, M., Malcher, A.: Complexity of multi-head finite automata: origins and directions. Theoret. Comput. Sci. 412(1\u20132), 83\u201396 (2011)","journal-title":"Theoret. Comput. Sci."},{"issue":"1","key":"20_CR18","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1145\/3022187","volume":"64","author":"A Karbyshev","year":"2017","unstructured":"Karbyshev, A., Bj\u00f8rner, N., Itzhaky, S., Rinetzky, N., Shoham, S.: Property-directed inference of universal invariants or proving their absence. J. ACM (JACM) 64(1), 7 (2017)","journal-title":"J. ACM (JACM)"},{"key":"20_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"448","DOI":"10.1007\/3-540-16492-8_94","volume-title":"Third International Conference on Logic Programming","author":"DA Miller","year":"1986","unstructured":"Miller, D.A., Nadathur, G.: Higher-order logic programming. In: Shapiro, E. (ed.) ICLP 1986. LNCS, vol. 225, pp. 448\u2013462. Springer, Heidelberg (1986). https:\/\/doi.org\/10.1007\/3-540-16492-8_94"},{"issue":"1","key":"20_CR20","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1016\/S0743-1066(96)00121-5","volume":"31","author":"HJ Levesque","year":"1997","unstructured":"Levesque, H.J., Reiter, R., Lesp\u00e9rance, Y., Lin, F., Scherl, R.B.: GOLOG: a logic programming language for dynamic domains. J. Logic Programm. 31(1), 59\u201383 (1997). https:\/\/doi.org\/10.1016\/S0743-1066(96)00121-5","journal-title":"J. Logic Programm."},{"key":"20_CR21","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.: Infinite games. In: Gr\u00e4del, E., Thomas, W., Wilke, T. (eds.) Automata Logics, and Infinite Games. LNCS, vol. 2500, pp. 23\u201338. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-36387-4_2"},{"key":"20_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/978-3-319-99725-4_4","volume-title":"Static Analysis","author":"KL McMillan","year":"2018","unstructured":"McMillan, K.L., Padon, O.: Deductive verification in decidable fragments with ivy. In: Podelski, A. (ed.) SAS 2018. LNCS, vol. 11002, pp. 43\u201355. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-99725-4_4"},{"key":"20_CR23","doi-asserted-by":"publisher","unstructured":"M\u00fcller, C., Seidl, H., Zalinescu, E.: Inductive invariants for noninterference in multi-agent workflows. In: 31st IEEE Computer Security Foundations Symposium, CSF 2018, Oxford, UK, 9\u201312 July 2018, pp. 247\u2013261. IEEE (2018). https:\/\/doi.org\/10.1109\/CSF.2018.00025","DOI":"10.1109\/CSF.2018.00025"},{"issue":"1","key":"20_CR24","doi-asserted-by":"publisher","first-page":"663","DOI":"10.1145\/2775051.2676990","volume":"50","author":"Oded Padon","year":"2015","unstructured":"Padon, O., Immerman, N., Karbyshev, A., Lahav, O., Sagiv, M., Shoham, S.: Decentralizing SDN policies. In: ACM SIGPLAN Notices, vol. 50, pp. 663\u2013676. ACM (2015)","journal-title":"ACM SIGPLAN Notices"},{"key":"20_CR25","doi-asserted-by":"publisher","unstructured":"Padon, O., Immerman, N., Shoham, S., Karbyshev, A., Sagiv, M.: Decidability of inferring inductive invariants. In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, pp. 217\u2013231. ACM (2016). https:\/\/doi.org\/10.1145\/2837614.2837640","DOI":"10.1145\/2837614.2837640"},{"issue":"OOPSLA","key":"20_CR26","first-page":"108","volume":"1","author":"O Padon","year":"2017","unstructured":"Padon, O., Losa, G., Sagiv, M., Shoham, S.: Paxos made EPR: decidable reasoning about distributed protocols. Proc. ACM Programm. Lang. 1(OOPSLA), 108 (2017)","journal-title":"Proc. ACM Programm. Lang."},{"issue":"6","key":"20_CR27","doi-asserted-by":"publisher","first-page":"614","DOI":"10.1145\/2980983.2908118","volume":"51","author":"O Padon","year":"2016","unstructured":"Padon, O., McMillan, K.L., Panda, A., Sagiv, M., Shoham, S.: Ivy: safety verification by interactive generalization. ACM SIGPLAN Notices 51(6), 614\u2013630 (2016)","journal-title":"ACM SIGPLAN Notices"},{"key":"20_CR28","series-title":"Modern Birkh\u00e4user Classics","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-0-8176-4842-8_1","volume-title":"Classic Papers in Combinatorics","author":"FP Ramsey","year":"2009","unstructured":"Ramsey, F.P.: On a problem of formal logic. In: Gessel, I., Rota, G.C. (eds.) Classic Papers in Combinatorics. MBC, pp. 1\u201324. Birkh\u00e4user, Boston (2009). https:\/\/doi.org\/10.1007\/978-0-8176-4842-8_1"},{"issue":"5","key":"20_CR29","doi-asserted-by":"publisher","first-page":"388","DOI":"10.1147\/rd.105.0388","volume":"10","author":"AL Rosenberg","year":"1966","unstructured":"Rosenberg, A.L.: On multi-head finite automata. IBM J. Res. Dev. 10(5), 388\u2013394 (1966)","journal-title":"IBM J. Res. Dev."},{"key":"20_CR30","volume-title":"Artificial Intelligence: A Modern Approach","author":"SJ Russell","year":"2016","unstructured":"Russell, S.J., Norvig, P.: Artificial Intelligence: A Modern Approach. Pearson Education Limited, Kuala Lumpur (2016)"},{"key":"20_CR31","doi-asserted-by":"crossref","unstructured":"Seidl, H., M\u00fcller, C., Finkbeiner, B.: How to win first-order safety games. arXiv preprint arXiv:1908.05964 (2019)","DOI":"10.1007\/978-3-030-39322-9_20"},{"key":"20_CR32","doi-asserted-by":"publisher","unstructured":"Seidl, H., M\u00fcller, C., Finkbeiner, B.: How to win first order safety games - software artifact, October 2019. https:\/\/doi.org\/10.5281\/zenodo.3514277","DOI":"10.5281\/zenodo.3514277"},{"key":"20_CR33","unstructured":"Spielmann, M.: Abstract state machines: verification problems and complexity. Ph.D. thesis, RWTH Aachen University, Germany (2000). http:\/\/sylvester.bth.rwth-aachen.de\/dissertationen\/2001\/008\/01_008.pdf"},{"key":"20_CR34","doi-asserted-by":"publisher","unstructured":"Walker, A., Ryzhyk, L.: Predicate abstraction for reactive synthesis. In: 2014 Formal Methods in Computer-Aided Design (FMCAD), pp. 219\u2013226, October 2014. https:\/\/doi.org\/10.1109\/FMCAD.2014.6987617","DOI":"10.1109\/FMCAD.2014.6987617"},{"key":"20_CR35","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/978-3-319-24312-2_18","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"C Wernhard","year":"2015","unstructured":"Wernhard, C.: Second-order quantifier elimination on relational monadic formulas \u2013 a basic method and some less expected applications. In: De Nivelle, H. (ed.) TABLEAUX 2015. LNCS (LNAI), vol. 9323, pp. 253\u2013269. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-24312-2_18"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-39322-9_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,12]],"date-time":"2024-03-12T18:43:23Z","timestamp":1710269003000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-39322-9_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030393212","9783030393229"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-39322-9_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"13 January 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"VMCAI","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Verification, Model Checking, and Abstract Interpretation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"New Orleans, LA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 January 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 January 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vmcai2020a","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/popl20.sigplan.org\/home\/VMCAI-2020","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"44","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"21","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"48% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4,4","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}