Document Open Access Logo

Pareto Fronts for Compositionally Solving String Diagrams of Parity Games

Author Kazuki Watanabe

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.CALCO.2025.14.pdf
  • Filesize: 1.36 MB
  • 20 pages
HTML5 Logo HTML (experimental)
LIPIcs.CALCO.2025.14.html

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Verification by model checking
Keywords
  • parity game
  • compositionality
  • string diagram

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

Open parity games are proposed as a compositional extension of parity games with algebraic operations, forming string diagrams of parity games. A potential application of string diagrams of parity games is to describe a large parity game with a given compositional structure and solve it efficiently as a divide-and-conquer algorithm by exploiting its compositional structure.
Building on our recent progress in open Markov decision processes, we introduce Pareto fronts of open parity games, offering a framework for multi-objective solutions. We establish the positional determinacy of open parity games with respect to their Pareto fronts through a novel translation method. Our translation converts an open parity game into a parity game tailored to a given single-objective. Furthermore, we present a simple algorithm for solving open parity games, derived from this translation that allows the application of existing efficient algorithms for parity games. Expanding on this foundation, we develop a compositional algorithm for string diagrams of parity games.

Cite As Get BibTex

Kazuki Watanabe. Pareto Fronts for Compositionally Solving String Diagrams of Parity Games. In 11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 342, pp. 14:1-14:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.CALCO.2025.14

Author Details

Kazuki Watanabe
  • National Institute of Informatics, Tokyo, Japan
  • The Graduate University for Advanced Studies (SOKENDAI), Hayama, Japan

Funding

We are supported by the JST grant No. JPMJAX23CU.

Acknowledgements

We would like to thank the anonymous referees for their helpful suggestions, which have enabled us to improve this article.

References

  1. Samson Abramsky. Domain theory in logical form. In LICS, pages 47-53. IEEE Computer Society, 1987. Google Scholar
  2. John C Baez and Jason Erbele. Categories in control. arXiv preprint arXiv:1405.6881, 2014. Google Scholar
  3. John C. Baez, Fabrizio Genovese, Jade Master, and Michael Shulman. Categories of nets. In LICS, pages 1-13. IEEE, 2021. URL: https://doi.org/10.1109/LICS52264.2021.9470566.
  4. Dietmar Berwanger, Anuj Dawar, Paul Hunter, and Stephan Kreutzer. Dag-width and parity games. In STACS, volume 3884 of Lecture Notes in Computer Science, pages 524-536. Springer, 2006. URL: https://doi.org/10.1007/11672142_43.
  5. Filippo Bonchi, Fabio Gadducci, Aleks Kissinger, Pawel Sobocinski, and Fabio Zanasi. String diagram rewrite theory I: rewriting with Frobenius structure. J. ACM, 69(2):14:1-14:58, 2022. URL: https://doi.org/10.1145/3502719.
  6. Filippo Bonchi, Joshua Holland, Robin Piedeleu, Pawel Sobocinski, and Fabio Zanasi. Diagrammatic algebra: from linear to concurrent systems. Proc. ACM Program. Lang., 3(POPL):25:1-25:28, 2019. URL: https://doi.org/10.1145/3290338.
  7. Filippo Bonchi, Pawel Sobocinski, and Fabio Zanasi. Full abstraction for signal flow graphs. In POPL, pages 515-526. ACM, 2015. URL: https://doi.org/10.1145/2676726.2676993.
  8. Filippo Bonchi, Pawel Sobocinski, and Fabio Zanasi. The calculus of signal flow diagrams I: linear relations on streams. Inf. Comput., 252:2-29, 2017. URL: https://doi.org/10.1016/J.IC.2016.03.002.
  9. Véronique Bruyère, Jean-François Raskin, and Clément Tamines. Pareto-rational verification. In CONCUR, volume 243 of LIPIcs, pages 33:1-33:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPICS.CONCUR.2022.33.
  10. Cristian S. Calude, Sanjay Jain, Bakhadyr Khoussainov, Wei Li, and Frank Stephan. Deciding parity games in quasi-polynomial time. SIAM J. Comput., 51(2):17-152, 2022. URL: https://doi.org/10.1137/17M1145288.
  11. Taolue Chen, Vojtech Forejt, Marta Z. Kwiatkowska, Aistis Simaitis, and Clemens Wiltsche. On stochastic games with multiple objectives. In MFCS, volume 8087 of Lecture Notes in Computer Science, pages 266-277. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-40313-2_25.
  12. Edmund M. Clarke, David E. Long, and Kenneth L. McMillan. Compositional model checking. In LICS, pages 353-362. IEEE Computer Society, 1989. URL: https://doi.org/10.1109/LICS.1989.39190.
  13. Bob Coecke and Ross Duncan. Interacting quantum observables. In ICALP (2), volume 5126 of Lecture Notes in Computer Science, pages 298-310. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-70583-3_25.
  14. Bob Coecke and Aleks Kissinger. Picturing Quantum Processes: A First Course in Quantum Theory and Diagrammatic Reasoning. Cambridge University Press, 2017. URL: https://doi.org/10.1017/9781316219317.
  15. E. Allen Emerson. Automata, tableaux and temporal logics (extended abstract). In Logic of Programs, volume 193 of Lecture Notes in Computer Science, pages 79-88. Springer, 1985. URL: https://doi.org/10.1007/3-540-15648-8_7.
  16. E. Allen Emerson and Charanjit S. Jutla. Tree automata, mu-calculus and determinacy (extended abstract). In FOCS, pages 368-377. IEEE Computer Society, 1991. URL: https://doi.org/10.1109/SFCS.1991.185392.
  17. E. Allen Emerson, Charanjit S. Jutla, and A. Prasad Sistla. On model checking for the μ-calculus and its fragments. Theor. Comput. Sci., 258(1-2):491-522, 2001. URL: https://doi.org/10.1016/S0304-3975(00)00034-7.
  18. Kousha Etessami, Marta Z. Kwiatkowska, Moshe Y. Vardi, and Mihalis Yannakakis. Multi-objective model checking of Markov decision processes. Log. Methods Comput. Sci., 4(4), 2008. URL: https://doi.org/10.2168/LMCS-4(4:8)2008.
  19. John Fearnley, Sanjay Jain, Bart de Keijzer, Sven Schewe, Frank Stephan, and Dominik Wojtczak. An ordered approach to solving parity games in quasi-polynomial time and quasi-linear space. Int. J. Softw. Tools Technol. Transf., 21(3):325-349, 2019. URL: https://doi.org/10.1007/S10009-019-00509-3.
  20. John Fearnley and Sven Schewe. Time and space results for parity games with bounded treewidth. Log. Methods Comput. Sci., 9(2), 2013. URL: https://doi.org/10.2168/LMCS-9(2:6)2013.
  21. Vojtech Forejt, Marta Z. Kwiatkowska, and David Parker. Pareto curves for probabilistic model checking. In ATVA, volume 7561 of Lecture Notes in Computer Science, pages 317-332. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-33386-6_25.
  22. Koichi Fujima, Sohei Ito, and Naoki Kobayashi. Practical alternating parity tree automata model checking of higher-order recursion schemes. In APLAS, volume 8301 of Lecture Notes in Computer Science, pages 17-32. Springer, 2013. URL: https://doi.org/10.1007/978-3-319-03542-0_2.
  23. Neil Ghani, Jules Hedges, Viktor Winschel, and Philipp Zahn. Compositional game theory. In LICS, pages 472-481. ACM, 2018. URL: https://doi.org/10.1145/3209108.3209165.
  24. Charles Grellois and Paul-André Melliès. Finitary semantics of linear logic and higher-order model-checking. In MFCS (1), volume 9234 of Lecture Notes in Computer Science, pages 256-268. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-48057-1_20.
  25. Marcin Jurdzinski and Ranko Lazic. Succinct progress measures for solving parity games. In LICS, pages 1-9. IEEE Computer Society, 2017. URL: https://doi.org/10.1109/LICS.2017.8005092.
  26. Roope Kaivola. Compositional model checking for linear-time temporal logic. In CAV, volume 663 of Lecture Notes in Computer Science, pages 248-259. Springer, 1992. URL: https://doi.org/10.1007/3-540-56496-9_20.
  27. Naoki Kobayashi and C.-H. Luke Ong. A type system equivalent to the modal mu-calculus model checking of higher-order recursion schemes. In LICS, pages 179-188. IEEE Computer Society, 2009. URL: https://doi.org/10.1109/LICS.2009.29.
  28. Dexter Kozen. Results on the propositional mu-calculus. Theor. Comput. Sci., 27:333-354, 1983. URL: https://doi.org/10.1016/0304-3975(82)90125-6.
  29. Orna Kupferman and Moshe Y. Vardi. Weak alternating automata and tree automata emptiness. In STOC, pages 224-233. ACM, 1998. URL: https://doi.org/10.1145/276698.276748.
  30. Marta Z. Kwiatkowska, Gethin Norman, David Parker, and Hongyang Qu. Compositional probabilistic verification through multi-objective model checking. Inf. Comput., 232:38-65, 2013. URL: https://doi.org/10.1016/J.IC.2013.10.001.
  31. Elena Di Lavore, Jules Hedges, and Pawel Sobocinski. Compositional modelling of network games. In CSL, volume 183 of LIPIcs, pages 30:1-30:24. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPICS.CSL.2021.30.
  32. Karoliina Lehtinen. A modal μ perspective on solving parity games in quasi-polynomial time. In LICS, pages 639-648. ACM, 2018. URL: https://doi.org/10.1145/3209108.3209115.
  33. Michael Luttenberger, Philipp J. Meyer, and Salomon Sickert. Practical synthesis of reactive systems from LTL specifications via parity games. Acta Informatica, 57(1-2):3-36, 2020. URL: https://doi.org/10.1007/S00236-019-00349-3.
  34. Jan Obdrzálek. Fast mu-calculus model checking when tree-width is bounded. In CAV, volume 2725 of Lecture Notes in Computer Science, pages 80-92. Springer, 2003. URL: https://doi.org/10.1007/978-3-540-45069-6_7.
  35. C.-H. Luke Ong. On model-checking trees generated by higher-order recursion schemes. In LICS, pages 81-90. IEEE Computer Society, 2006. URL: https://doi.org/10.1109/LICS.2006.38.
  36. Christos H. Papadimitriou and Mihalis Yannakakis. On the approximability of trade-offs and optimal access of web sources. In FOCS, pages 86-92. IEEE Computer Society, 2000. URL: https://doi.org/10.1109/SFCS.2000.892068.
  37. Robin Piedeleu. The algebra of parity games. CoRR, abs/2501.18499, 2025. URL: https://doi.org/10.48550/arXiv.2501.18499.
  38. Julian Rathke, Pawel Sobocinski, and Owen Stephens. Compositional reachability in Petri nets. In RP, volume 8762 of Lecture Notes in Computer Science, pages 230-243. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-11439-2_18.
  39. Sylvain Salvati and Igor Walukiewicz. Krivine machines and higher-order schemes. Inf. Comput., 239:340-355, 2014. URL: https://doi.org/10.1016/J.IC.2014.07.012.
  40. Takeshi Tsukada and C.-H. Luke Ong. Compositional higher-order model checking via ω-regular games over Böhm trees. In CSL-LICS, pages 78:1-78:10. ACM, 2014. URL: https://doi.org/10.1145/2603088.2603133.
  41. Yaron Velner, Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger, Alexander Moshe Rabinovich, and Jean-François Raskin. The complexity of multi-mean-payoff and multi-energy games. Inf. Comput., 241:177-196, 2015. URL: https://doi.org/10.1016/J.IC.2015.03.001.
  42. Jens Vöge and Marcin Jurdzinski. A discrete strategy improvement algorithm for solving parity games. In CAV, volume 1855 of Lecture Notes in Computer Science, pages 202-215. Springer, 2000. URL: https://doi.org/10.1007/10722167_18.
  43. Kazuki Watanabe, Clovis Eberhart, Kazuyuki Asada, and Ichiro Hasuo. A compositional approach to parity games. In MFPS, volume 351 of EPTCS, pages 278-295, 2021. URL: https://doi.org/10.4204/EPTCS.351.17.
  44. Kazuki Watanabe, Clovis Eberhart, Kazuyuki Asada, and Ichiro Hasuo. Compositional probabilistic model checking with string diagrams of MDPs. In CAV (3), volume 13966 of Lecture Notes in Computer Science, pages 40-61. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-37709-9_3.
  45. Kazuki Watanabe, Clovis Eberhart, Kazuyuki Asada, and Ichiro Hasuo. Compositional solution of mean payoff games by string diagrams. In Principles of Verification (3), volume 15262 of Lecture Notes in Computer Science, pages 423-445. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-75778-5_20.
  46. Kazuki Watanabe, Marck van der Vegt, Ichiro Hasuo, Jurriaan Rot, and Sebastian Junges. Pareto curves for compositionally model checking string diagrams of MDPs. In TACAS (2), volume 14571 of Lecture Notes in Computer Science, pages 279-298. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-57249-4_14.
  47. Kazuki Watanabe, Marck van der Vegt, Sebastian Junges, and Ichiro Hasuo. Compositional value iteration with pareto caching. In CAV (3), volume 14683 of Lecture Notes in Computer Science, pages 467-491. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-65633-0_21.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact