{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T01:34:13Z","timestamp":1742952853290,"version":"3.40.3"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031314759"},{"type":"electronic","value":"9783031314766"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"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":[[2023]]},"DOI":"10.1007\/978-3-031-31476-6_9","type":"book-chapter","created":{"date-parts":[[2023,5,16]],"date-time":"2023-05-16T07:02:46Z","timestamp":1684220566000},"page":"170-187","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Justifications and\u00a0a\u00a0Reconstruction of\u00a0Parity Game Solving Algorithms"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8190-8296","authenticated-orcid":false,"given":"Ruben","family":"Lapauw","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6881-1462","authenticated-orcid":false,"given":"Maurice","family":"Bruynooghe","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0422-7339","authenticated-orcid":false,"given":"Marc","family":"Denecker","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,5,17]]},"reference":[{"key":"9_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/978-3-319-49052-6_8","volume-title":"Hardware and Software: Verification and Testing","author":"M Benerecetti","year":"2016","unstructured":"Benerecetti, M., Dell\u2019Erba, D., Mogavero, F.: Improving priority promotion for parity games. In: Bloem, R., Arbel, E. (eds.) HVC 2016. LNCS, vol. 10028, pp. 117\u2013133. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-49052-6_8"},{"key":"9_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"270","DOI":"10.1007\/978-3-319-41540-6_15","volume-title":"Computer Aided Verification","author":"M Benerecetti","year":"2016","unstructured":"Benerecetti, M., Dell\u2019Erba, D., Mogavero, F.: Solving parity games via priority promotion. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 270\u2013290. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41540-6_15"},{"key":"9_CR3","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1016\/j.ic.2018.09.005","volume":"262","author":"M Benerecetti","year":"2018","unstructured":"Benerecetti, M., Dell\u2019Erba, D., Mogavero, F.: A delayed promotion policy for parity games. Inf. Comput. 262, 221\u2013240 (2018). https:\/\/doi.org\/10.1016\/j.ic.2018.09.005","journal-title":"Inf. Comput."},{"key":"9_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/3-540-58179-0_50","volume-title":"Computer Aided Verification","author":"O Bernholtz","year":"1994","unstructured":"Bernholtz, O., Vardi, M.Y., Wolper, P.: An automata-theoretic approach to branching-time model checking (Extended abstract). In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 142\u2013155. Springer, Heidelberg (1994). https:\/\/doi.org\/10.1007\/3-540-58179-0_50"},{"key":"9_CR5","doi-asserted-by":"publisher","unstructured":"Bloem, R., Schewe, S., Khalimov, A.: CTL* synthesis via LTL synthesis. In: Fisman, D., Jacobs, S. (eds.) Proceedings Sixth Workshop on Synthesis, SYNT@CAV 2017, Heidelberg, Germany, 22nd July 2017. EPTCS, vol. 260, pp. 4\u201322 (2017). https:\/\/doi.org\/10.4204\/EPTCS.260.4","DOI":"10.4204\/EPTCS.260.4"},{"key":"9_CR6","doi-asserted-by":"publisher","unstructured":"Bruse, F., Falk, M., Lange, M.: The fixpoint-iteration algorithm for parity games. In: Peron, A., Piazza, C. (eds.) Proceedings Fifth International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2014, Verona, Italy, 10\u201312 September 2014. EPTCS, vol. 161, pp. 116\u2013130 (2014). https:\/\/doi.org\/10.4204\/EPTCS.161.12","DOI":"10.4204\/EPTCS.161.12"},{"key":"9_CR7","doi-asserted-by":"publisher","unstructured":"Calude, C.S., Jain, S., Khoussainov, B., Li, W., Stephan, F.: Deciding parity games in quasipolynomial time. In: Hatami, H., McKenzie, P., King, V. (eds.) Proceedings of the 49th Annual ACM SIGACT Symposium on Theory of Computing, STOC 2017, Montreal, QC, Canada, 19\u201323 June 2017, pp. 252\u2013263. ACM (2017). https:\/\/doi.org\/10.1145\/3055399.3055409","DOI":"10.1145\/3055399.3055409"},{"key":"9_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/978-3-642-36742-7_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Cranen","year":"2013","unstructured":"Cranen, S., et al.: An overview of the mCRL2 toolset and its recent advances. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 199\u2013213. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_15"},{"issue":"28","key":"9_CR9","doi-asserted-by":"publisher","first-page":"3129","DOI":"10.1016\/j.tcs.2011.02.034","volume":"412","author":"S Cranen","year":"2011","unstructured":"Cranen, S., Groote, J.F., Reniers, M.A.: A linear translation from CTL* to the first-order modal $$\\mu $$ -calculus. Theor. Comput. Sci. 412(28), 3129\u20133139 (2011). https:\/\/doi.org\/10.1016\/j.tcs.2011.02.034","journal-title":"Theor. Comput. Sci."},{"key":"9_CR10","doi-asserted-by":"publisher","unstructured":"van Dijk, T., Rubbens, B.: Simple fixpoint iteration to solve parity games. In: Leroux, J., Raskin, J. (eds.) Proceedings Tenth International Symposium on Games, Automata, Logics, and Formal Verification, GandALF 2019, Bordeaux, France, 2\u20133rd September 2019. EPTCS, vol. 305, pp. 123\u2013139 (2019). https:\/\/doi.org\/10.4204\/EPTCS.305.9","DOI":"10.4204\/EPTCS.305.9"},{"key":"9_CR11","doi-asserted-by":"publisher","unstructured":"Emerson, E.A., Jutla, C.S.: Tree automata, mu-calculus and determinacy (extended abstract). In: 32nd Annual Symposium on Foundations of Computer Science, San Juan, Puerto Rico, 1\u20134 October 1991, pp. 368\u2013377. IEEE Computer Society (1991). https:\/\/doi.org\/10.1109\/SFCS.1991.185392","DOI":"10.1109\/SFCS.1991.185392"},{"key":"9_CR12","doi-asserted-by":"publisher","unstructured":"Fearnley, J., Jain, S., Schewe, S., Stephan, F., Wojtczak, D.: An ordered approach to solving parity games in quasi polynomial time and quasi linear space. In: Erdogmus, H., Havelund, K. (eds.) Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software, Santa Barbara, CA, USA, 10\u201314 July 2017, pp. 112\u2013121. ACM (2017). https:\/\/doi.org\/10.1145\/3092282.3092286","DOI":"10.1145\/3092282.3092286"},{"key":"9_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36387-4","volume-title":"Automata Logics, and Infinite Games","year":"2002","unstructured":"Gr\u00e4del, E., Thomas, W., Wilke, T. (eds.): LNCS, vol. 2500. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-36387-4"},{"issue":"4\u20136","key":"9_CR14","doi-asserted-by":"publisher","first-page":"581","DOI":"10.1017\/S1471068410000293","volume":"10","author":"P Hou","year":"2010","unstructured":"Hou, P., Cat, B.D., Denecker, M.: FO(FD): extending classical logic with rule-based fixpoint definitions. TPLP 10(4\u20136), 581\u2013596 (2010). https:\/\/doi.org\/10.1017\/S1471068410000293","journal-title":"TPLP"},{"key":"9_CR15","unstructured":"Jacobs, S., et al.: The 5th reactive synthesis competition (SYNTCOMP 2018): Benchmarks, participants & results. CoRR (2019). http:\/\/arxiv.org\/abs\/1904.07736"},{"key":"9_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"290","DOI":"10.1007\/3-540-46541-3_24","volume-title":"STACS 2000","author":"M Jurdzi\u0144ski","year":"2000","unstructured":"Jurdzi\u0144ski, M.: Small progress measures for solving parity games. In: Reichel, H., Tison, S. (eds.) STACS 2000. LNCS, vol. 1770, pp. 290\u2013301. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-46541-3_24"},{"key":"9_CR17","doi-asserted-by":"publisher","unstructured":"Kant, G., van de Pol, J.: Efficient instantiation of parameterised Boolean equation systems to parity games. In: Wijs, A., Bosnacki, D., Edelkamp, S. (eds.) Proceedings First Workshop on GRAPH Inspection and Traversal Engineering, GRAPHITE 2012, Tallinn, Estonia, 1st April 2012. EPTCS, vol. 99, pp. 50\u201365 (2012). https:\/\/doi.org\/10.4204\/EPTCS.99.7","DOI":"10.4204\/EPTCS.99.7"},{"key":"9_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/3-540-56922-7_9","volume-title":"Computer Aided Verification","author":"Y Kesten","year":"1993","unstructured":"Kesten, Y., Manna, Z., McGuire, H., Pnueli, A.: A decision algorithm for full propositional temporal logic. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 97\u2013109. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/3-540-56922-7_9"},{"key":"9_CR19","unstructured":"Lapauw, R.: Reconstructing and Improving Parity Game Solvers with Justifications. Ph.D. thesis, Department of Computer Science, KU Leuven, Leuven, Belgium (2021). [To appear]"},{"key":"9_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"449","DOI":"10.1007\/978-3-030-39322-9_21","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"R Lapauw","year":"2020","unstructured":"Lapauw, R., Bruynooghe, M., Denecker, M.: Improving parity game solvers with justifications. In: Beyer, D., Zufferey, D. (eds.) VMCAI 2020. LNCS, vol. 11990, pp. 449\u2013470. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-39322-9_21"},{"key":"9_CR21","doi-asserted-by":"publisher","unstructured":"Luttenberger, M., Meyer, P.J., Sickert, S.: Practical synthesis of reactive systems from LTL specifications via parity games. Acta Inf. 57(1), 3\u201336 (2020). https:\/\/doi.org\/10.1007\/s00236-019-00349-3","DOI":"10.1007\/s00236-019-00349-3"},{"key":"9_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"578","DOI":"10.1007\/978-3-319-96145-3_31","volume-title":"Computer Aided Verification","author":"PJ Meyer","year":"2018","unstructured":"Meyer, P.J., Sickert, S., Luttenberger, M.: Strix: explicit reactive synthesis strikes back! In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 578\u2013586. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_31"},{"key":"9_CR23","unstructured":"Mostowski, A.: Games with forbidden positions. University of Gdansk, Gdansk. Technical report, Poland (1991)"},{"key":"9_CR24","doi-asserted-by":"publisher","unstructured":"Parys, P.: Parity games: Zielonka\u2019s algorithm in quasi-polynomial time. In: Rossmanith, P., Heggernes, P., Katoen, J. (eds.) 44th International Symposium on Mathematical Foundations of Computer Science, MFCS 2019, August 26\u201330, 2019, Aachen, Germany. LIPIcs, vol. 138, pp. 10:1\u201310:13. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2019). https:\/\/doi.org\/10.4230\/LIPIcs.MFCS.2019.10","DOI":"10.4230\/LIPIcs.MFCS.2019.10"},{"key":"9_CR25","doi-asserted-by":"publisher","unstructured":"Piterman, N.: From nondeterministic Buchi and Streett automata to deterministic parity automata. In: 21th IEEE Symposium on Logic in Computer Science (LICS 2006), 12\u201315 August 2006, Seattle, WA, USA, Proceedings, pp. 255\u2013264. IEEE Computer Society (2006). https:\/\/doi.org\/10.1109\/LICS.2006.28","DOI":"10.1109\/LICS.2006.28"},{"key":"9_CR26","doi-asserted-by":"publisher","unstructured":"Safra, S.: On the complexity of omega-automata. In: 29th Annual Symposium on Foundations of Computer Science, White Plains, New York, USA, 24\u201326 October 1988, pp. 319\u2013327. IEEE Computer Society (1988). https:\/\/doi.org\/10.1109\/SFCS.1988.21948","DOI":"10.1109\/SFCS.1988.21948"},{"key":"9_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/978-3-540-87531-4_27","volume-title":"Computer Science Logic","author":"S Schewe","year":"2008","unstructured":"Schewe, S.: An optimal strategy improvement algorithm for solving parity and payoff games. In: Kaminski, M., Martini, S. (eds.) CSL 2008. LNCS, vol. 5213, pp. 369\u2013384. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-87531-4_27"},{"key":"9_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1007\/978-3-319-96142-2_14","volume-title":"Computer Aided Verification","author":"T Dijk","year":"2018","unstructured":"Dijk, T.: Attracting tangles to solve parity games. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10982, pp. 198\u2013215. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96142-2_14"},{"key":"9_CR29","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification (preliminary report). In: Proceedings of the Symposium on Logic in Computer Science (LICS 1986), Cambridge, Massachusetts, USA, 16\u201318 June 1986, pp. 332\u2013344. IEEE Computer Society (1986)"},{"key":"9_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"399","DOI":"10.1007\/3-540-60922-9_33","volume-title":"STACS 96","author":"I Walukiewicz","year":"1996","unstructured":"Walukiewicz, I.: Monadic second order logic on tree-like structures. In: Puech, C., Reischuk, R. (eds.) STACS 1996. LNCS, vol. 1046, pp. 399\u2013413. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-60922-9_33"},{"issue":"1\u20132","key":"9_CR31","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1016\/S0304-3975(98)00009-7","volume":"200","author":"W Zielonka","year":"1998","unstructured":"Zielonka, W.: Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theor. Comput. Sci. 200(1\u20132), 135\u2013183 (1998). https:\/\/doi.org\/10.1016\/S0304-3975(98)00009-7","journal-title":"Theor. Comput. Sci."}],"container-title":["Lecture Notes in Computer Science","Analysis, Verification and Transformation for Declarative Programming and Intelligent Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-31476-6_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,16]],"date-time":"2023-05-16T07:04:26Z","timestamp":1684220666000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-31476-6_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031314759","9783031314766"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-31476-6_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"17 May 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}