{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,2]],"date-time":"2026-07-02T11:20:04Z","timestamp":1782991204154,"version":"3.54.5"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032227294","type":"print"},{"value":"9783032227300","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-22730-0_25","type":"book-chapter","created":{"date-parts":[[2026,4,15]],"date-time":"2026-04-15T16:24:50Z","timestamp":1776270290000},"page":"527-548","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["The Modal Logic of Abstraction Refinement"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4829-0476","authenticated-orcid":false,"given":"Jakob","family":"Piribauer","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Vinzent","family":"Zschuppe","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,4,15]]},"reference":[{"key":"25_CR1","unstructured":"Christel Baier and Joost-Pieter Katoen. Principles of Model Checking. MIT Press, 2008."},{"key":"25_CR2","doi-asserted-by":"crossref","unstructured":"S\u00f6ren Berger, Alexander\u00a0Christensen Block, and Benedikt L\u00f6we. The modal logic of abelian groups. Algebra universalis, 84(3):25, 2023. 10.1007\/s00012-023-00821-9","DOI":"10.1007\/s00012-023-00821-9"},{"key":"25_CR3","doi-asserted-by":"crossref","unstructured":"Guram Bezhanishvili, Nick Bezhanishvili, Joel Lucero-Bryan, and Jan van Mill. Tree-like constructions in topology and modal logic. Arch. Math. Log., 60(3-4):265\u2013299, 2021. URL: https:\/\/doi.org\/10.1007\/s00153-020-00743-6, 10.1007\/S00153-020-00743-6.","DOI":"10.1007\/s00153-020-00743-6"},{"key":"25_CR4","unstructured":"Patrick Blackburn, Maarten de\u00a0Rijke, and Yde Venema. Modal Logic, volume\u00a053 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2001. 10.1017\/CBO9781107050884."},{"key":"25_CR5","doi-asserted-by":"crossref","unstructured":"Laura Bozzelli, Hans van Ditmarsch, Tim French, James Hales, and Sophie Pinchinat. Refinement modal logic. Inf. Comput., 239:303\u2013339, 2014. URL: https:\/\/doi.org\/10.1016\/j.ic.2014.07.013, 10.1016\/J.IC.2014.07.013.","DOI":"10.1016\/j.ic.2014.07.013"},{"key":"25_CR6","doi-asserted-by":"crossref","unstructured":"Laura Bozzelli, Hans van Ditmarsch, and Sophie Pinchinat. The complexity of one-agent refinement modal logic. Theor. Comput. Sci., 603:58\u201383, 2015. URL: https:\/\/doi.org\/10.1016\/j.tcs.2015.07.015, 10.1016\/J.TCS.2015.07.015.","DOI":"10.1016\/j.tcs.2015.07.015"},{"key":"25_CR7","doi-asserted-by":"crossref","unstructured":"Glenn Bruns and Patrice Godefroid. Generalized model checking: Reasoning about partial state spaces. In Catuscia Palamidessi, editor, CONCUR 2000 \u2014 Concurrency Theory, pages 168\u2013182, Berlin, Heidelberg, 2000. Springer Berlin Heidelberg. 10.1007\/3-540-44618-4_14.","DOI":"10.1007\/3-540-44618-4_14"},{"key":"25_CR8","doi-asserted-by":"crossref","unstructured":"Alexander Chagrov and Michael Zakharyaschev. Modal logic. Oxford University Press, 1997.","DOI":"10.1093\/oso\/9780198537793.001.0001"},{"key":"25_CR9","doi-asserted-by":"crossref","unstructured":"Pankaj Chauhan, Edmund\u00a0M. Clarke, James\u00a0H. Kukula, Samir Sapra, Helmut Veith, and Dong Wang. Automated abstraction refinement for model checking large state spaces using SAT based conflict analysis. In Mark\u00a0D. Aagaard and John\u00a0W. O\u2019Leary, editors, Formal Methods in Computer-Aided Design, 4th International Conference, FMCAD 2002, Portland, OR, USA, November 6-8, 2002, Proceedings, volume 2517 of Lecture Notes in Computer Science, pages 3\u201351. Springer, 2002. 10.1007\/3-540-36126-X_3.","DOI":"10.1007\/3-540-36126-X_3"},{"key":"25_CR10","doi-asserted-by":"crossref","unstructured":"Edmund\u00a0M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. Counterexample-guided abstraction refinement. In E.\u00a0Allen Emerson and A.\u00a0Prasad Sistla, editors, Computer Aided Verification, 12th International Conference, CAV 2000, Chicago, IL, USA, July 15-19, 2000, Proceedings, volume 1855 of Lecture Notes in Computer Science, pages 154\u2013169. Springer, 2000. 10.1007\/10722167_15.","DOI":"10.1007\/10722167_15"},{"key":"25_CR11","doi-asserted-by":"crossref","unstructured":"Edmund\u00a0M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. Counterexample-guided abstraction refinement for symbolic model checking. J. ACM, 50(5):752\u2013794, 2003. 10.1145\/876638.876643.","DOI":"10.1145\/876638.876643"},{"key":"25_CR12","doi-asserted-by":"crossref","unstructured":"Edmund\u00a0M. Clarke, Anubhav Gupta, James\u00a0H. Kukula, and Ofer Strichman. SAT based abstraction-refinement using ILP and machine learning techniques. In Ed\u00a0Brinksma and Kim\u00a0Guldstrand Larsen, editors, Computer Aided Verification, 14th International Conference, CAV 2002,Copenhagen, Denmark, July 27-31, 2002, Proceedings, volume 2404 of Lecture Notes in Computer Science, pages 265\u2013279. Springer, 2002. 10.1007\/3-540-45657-0_20.","DOI":"10.1007\/3-540-45657-0_20"},{"key":"25_CR13","doi-asserted-by":"crossref","unstructured":"Edmund\u00a0M. Clarke, William Klieber, Milos Nov\u00e1cek, and Paolo Zuliani. Model checking and the state explosion problem. In Bertrand Meyer and Martin Nordio, editors, Tools for Practical Software Verification, LASER, International Summer School 2011, Elba Island, Italy, Revised Tutorial Lectures, volume 7682 of Lecture Notes in Computer Science, pages 1\u201330. Springer, 2011. 10.1007\/978-3-642-35746-6_1.","DOI":"10.1007\/978-3-642-35746-6_1"},{"key":"25_CR14","doi-asserted-by":"crossref","unstructured":"Dennis Dams, Rob Gerth, and Orna Grumberg. Abstract interpretation of reactive systems. ACM Trans. Program. Lang. Syst., 19(2):253\u2013291, 1997. 10.1145\/244795.244800.","DOI":"10.1145\/244795.244800"},{"key":"25_CR15","doi-asserted-by":"crossref","unstructured":"Dennis Dams and Orna Grumberg. Abstraction and abstraction refinement. In Edmund\u00a0M. Clarke, Thomas\u00a0A. Henzinger, Helmut Veith, and Roderick Bloem, editors, Handbook of Model Checking, pages 385\u2013419. Springer, 2018. URL: https:\/\/doi.org\/10.1007\/978-3-319-10575-8_13, 10.1007\/978-3-319-10575-8_13.","DOI":"10.1007\/978-3-319-10575-8_13"},{"key":"25_CR16","doi-asserted-by":"crossref","unstructured":"P.\u00a0Godefroid and M.\u00a0Huth. Model checking vs. generalized model checking: semantic minimizations for temporal logics. In 20th Annual IEEE Symposium on Logic in Computer Science (LICS\u2019 05), pages 158\u2013167, 2005. 10.1109\/LICS.2005.28.","DOI":"10.1109\/LICS.2005.28"},{"key":"25_CR17","unstructured":"Patrice Godefroid and Radha Jagadeesan. Automatic abstraction using generalized model checking. In Ed\u00a0Brinksma and Kim\u00a0Guldstrand Larsen, editors, Computer Aided Verification, 14th International Conference, CAV 2002,Copenhagen, Denmark, July 27-31, 2002, Proceedings, volume 2404 of Lecture Notes in Computer Science, pages 137\u2013150. Springer, 2002. 10.1007\/3-540-45657-0_11."},{"key":"25_CR18","doi-asserted-by":"crossref","unstructured":"Patrice Godefroid and Nir Piterman. LTL generalized model checking revisited. Int. J. Softw. Tools Technol. Transf., 13(6):571\u2013584, 2011. URL: https:\/\/doi.org\/10.1007\/s10009-010-0169-3, 10.1007\/S10009-010-0169-3.","DOI":"10.1007\/s10009-010-0169-3"},{"key":"25_CR19","unstructured":"Orna Grumberg, Martin Lange, Martin Leucker, and Sharon Shoham. Don\u2019t Know in the $$\\mu $$-calculus. In Radhia Cousot, editor, Verification, Model Checking, and Abstract Interpretation, 6th International Conference, VMCAI 2005, Paris, France, January 17-19, 2005, Proceedings, volume 3385 of Lecture Notes in Computer Science, pages 233\u2013249. Springer, 2005. 10.1007\/978-3-540-30579-8_16."},{"key":"25_CR20","doi-asserted-by":"crossref","unstructured":"Joel Hamkins and Benedikt L\u00f6we. The modal logic of forcing. Transactions of the American Mathematical Society, 360(4):1793\u20131817, 2008. 10.1090\/S0002-9947-07-04297-3.","DOI":"10.1090\/S0002-9947-07-04297-3"},{"key":"25_CR21","doi-asserted-by":"crossref","unstructured":"Joel\u00a0David Hamkins, George Leibman, and Benedikt L\u00f6we. Structural connections between a forcing class and its modal logic. Israel Journal of Mathematics, 207(2):617\u2013651, 2015. 10.1007\/s11856-015-1185-5.","DOI":"10.1007\/s11856-015-1185-5"},{"key":"25_CR22","doi-asserted-by":"crossref","unstructured":"Joel\u00a0David Hamkins and \u00d8ystein Linnebo. The modal logic of set-theoretic potentialism and the potentialist maximality principles. The Review of Symbolic Logic, 15(1):1\u201335, 2022. 10.1017\/s1755020318000242.","DOI":"10.1017\/S1755020318000242"},{"key":"25_CR23","doi-asserted-by":"crossref","unstructured":"Joel\u00a0David Hamkins and Benedikt L\u00f6we. Moving up and down in the generic multiverse. In Logic and Its Applications: 5th Indian Conference, ICLA 2013, Chennai, India, January 10-12, 2013. Proceedings 5, pages 139\u2013147. Springer, 2013. 10.1007\/978-3-642-36039-8_13.","DOI":"10.1007\/978-3-642-36039-8_13"},{"key":"25_CR24","doi-asserted-by":"crossref","unstructured":"Joel\u00a0David Hamkins and Wojciech\u00a0Aleksander Wo\u0142oszyn. Modal model theory. Notre Dame Journal of Formal Logic, 65(1):1\u201337, 2024. 10.1215\/00294527-2024-0001.","DOI":"10.1215\/00294527-2024-0001"},{"key":"25_CR25","unstructured":"Michael Huth, Radha Jagadeesan, and David\u00a0A. Schmidt. Modal transition systems: A foundation for three-valued program analysis. In David Sands, editor, Programming Languages and Systems, 10th European Symposium on Programming, ESOP 2001 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001 Genova, Italy, April 2-6, 2001, Proceedings, volume 2028 of Lecture Notes in Computer Science, pages 155\u2013169. Springer, 2001. 10.1007\/3-540-45309-1_11."},{"key":"25_CR26","doi-asserted-by":"crossref","unstructured":"Tanmay Inamdar and Benedikt L\u00f6we. The modal logic of inner models. The Journal of Symbolic Logic, 81(1):225\u2013236, 2016. 10.1017\/jsl.2015.67.","DOI":"10.1017\/jsl.2015.67"},{"key":"25_CR27","doi-asserted-by":"crossref","unstructured":"imanshu Jain, Franjo Ivancic, Aarti Gupta, Ilya Shlyakhter, and Chao Wang. Using statically computed invariants inside the predicate abstraction and refinement loop. In Thomas Ball and Robert\u00a0B. Jones, editors, Computer Aided Verification, 18th International Conference, CAV 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings, volume 4144 of Lecture Notes in Computer Science, pages 137\u2013151. Springer, 2006. 10.1007\/11817963_15.","DOI":"10.1007\/11817963_15"},{"key":"25_CR28","unstructured":"Kim\u00a0Guldstrand Larsen. Modal specifications. In Joseph Sifakis, editor, Automatic Verification Methods for Finite State Systems, International Workshop, Grenoble, France, June 12-14, 1989, Proceedings, volume 407 of Lecture Notes in Computer Science, pages 232\u2013246. Springer, 1989. 10.1007\/3-540-52148-8_19."},{"key":"25_CR29","unstructured":"Kim\u00a0Guldstrand Larsen and Bent Thomsen. A modal process logic. In Proceedings of the Third Annual Symposium on Logic in Computer Science (LICS \u201988), Edinburgh, Scotland, UK, July 5-8, 1988, pages 203\u2013210. IEEE Computer Society, 1988. 10.1109\/LICS.1988.5119."},{"key":"25_CR30","doi-asserted-by":"crossref","unstructured":"nneth\u00a0L. McMillan and Nina Amla. Automatic abstraction without counterexamples. In Hubert Garavel and John Hatcliff, editors, Tools and Algorithms for the Construction and Analysis of Systems, 9th International Conference, TACAS 2003, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003, Proceedings, volume 2619 of Lecture Notes in Computer Science, pages 2\u201317. Springer, 2003. 10.1007\/3-540-36577-X_2.","DOI":"10.1007\/3-540-36577-X_2"},{"key":"25_CR31","unstructured":"Jakob Piribauer. The modal logic of generic multiverses, 2017. M. Sc. thesis, Universiteit van Amsterdam."},{"key":"25_CR32","doi-asserted-by":"crossref","unstructured":"Jakob Piribauer and Vinzent Zschuppe. The modal logic of abstraction refinement, 2026. URL: https:\/\/arxiv.org\/abs\/2601.05897, arXiv:2601.05897.","DOI":"10.1007\/978-3-032-22730-0_25"},{"key":"25_CR33","unstructured":"Ilya Shapirovsky. On PSPACE-decidability in transitive modal logic. Advances in Modal Logic, 5:269\u2013287, 2004."},{"key":"25_CR34","doi-asserted-by":"crossref","unstructured":"Ur\u00a0Ya\u2019ar. The modal logic of -centered forcing and related forcing classes. J. Symb. Log., 86(1):1\u201324, 2021. URL: https:\/\/doi.org\/10.1017\/jsl.2019.41, 10.1017\/JSL.2019.41.","DOI":"10.1017\/jsl.2019.41"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-22730-0_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T23:50:55Z","timestamp":1782949855000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-22730-0_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032227294","9783032227300"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-22730-0_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"15 April 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FoSSaCS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Foundations of Software Science and Computation Structures","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Turin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 April 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2026\/conferences\/fossacs\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}