Abstract
We consider parity games on infinite graphs where configurations are represented by control-states and integer vectors. This framework subsumes two classic game problems: parity games on vector addition systems with states (vass) and multidimensional energy parity games. We show that the multidimensional energy parity game problem is inter-reducible with a subclass of single-sided parity games on vass where just one player can modify the integer counters and the opponent can only change control-states. Our main result is that the minimal elements of the upward-closed winning set of these single-sided parity games on vass are computable. This implies that the Pareto frontier of the minimal initial credit needed to win multidimensional energy parity games is also computable, solving an open question from the literature. Moreover, our main result implies the decidability of weak simulation preorder/equivalence between finite-state systems and vass, and the decidability of model checking vass with a large fragment of the modal μ-calculus.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Abdulla, P.A., Bouajjani, A., d’Orso, J.: Deciding monotonic games. In: Baaz, M., Makowsky, J.A. (eds.) CSL 2003. LNCS, vol. 2803, pp. 1–14. Springer, Heidelberg (2003)
Abdulla, P.A., Čerāns, K., Jonsson, B., Tsay, Y.: General decidability theorems for infinite-state systems. In: LICS 1996, pp. 313–321. IEEE (1996)
Abdulla, P.A., Mayr, R., Sangnier, A., Sproston, J.: Solving parity games on integer vectors. Technical Report EDI-INF-RR-1417, Univ. of Edinburgh (2013)
Brázdil, T., Jančar, P., Kučera, A.: Reachability games on extended vector addition systems with states. In: Abramsky, S., Gavoille, C., Kirchner, C., Meyer auf der Heide, F., Spirakis, P.G. (eds.) ICALP 2010. LNCS, vol. 6199, pp. 478–489. Springer, Heidelberg (2010)
Chatterjee, K., Doyen, L.: Energy parity games. TCS 458, 49–60 (2012)
Chatterjee, K., Doyen, L., Henzinger, T., Raskin, J.-F.: Generalized mean-payoff and energy games. In: FSTTCS 2010. LIPIcs, LZI, vol. 8, pp. 505–516 (2010)
Chatterjee, K., Randour, M., Raskin, J.-F.: Strategy synthesis for multi-dimensional quantitative objectives. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol. 7454, pp. 115–131. Springer, Heidelberg (2012)
Esparza, J., Nielsen, M.: Decibility issues for Petri nets - a survey. Journal of Informatik Processing and Cybernetics 30(3), 143–160 (1994)
van Glabbeek, R.J.: The linear time – branching time spectrum I; the semantics of concrete, sequential processes. In: Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.) Handbook of Process Algebra, ch. 1, pp. 3–99. Elsevier (2001)
Habermehl, P.: On the complexity of the linear-time mu-calculus for Petri-nets. In: Azéma, P., Balbo, G. (eds.) ICATPN 1997. LNCS, vol. 1248, pp. 102–116. Springer, Heidelberg (1997)
Jančar, P., Esparza, J., Moller, F.: Petri nets and regular processes. J. Comput. Syst. Sci. 59(3), 476–503 (1999)
Kirsten, D.: Alternating tree automata and parity games. In: Grädel, E., Thomas, W., Wilke, T. (eds.) Automata, Logics, and Infinite Games. LNCS, vol. 2500, pp. 153–167. Springer, Heidelberg (2002)
McNaughton, R.: Infinite games played on finite graphs. Annals of Pure and Applied Logic 65, 149–184 (1993)
Raskin, J.-F., Samuelides, M., Van Begin, L.: Games for counting abstractions. Electr. Notes Theor. Comput. Sci. 128(6), 69–85 (2005)
Valk, R., Jantzen, M.: The residue of vector sets with applications to decidability problems in Petri nets. Acta Inf. 21, 643–674 (1985)
Zielonka, W.: Infinite games on finitely coloured graphs with applications to automata on infinite trees. TCS 200, 135–183 (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Abdulla, P.A., Mayr, R., Sangnier, A., Sproston, J. (2013). Solving Parity Games on Integer Vectors. In: D’Argenio, P.R., Melgratti, H. (eds) CONCUR 2013 – Concurrency Theory. CONCUR 2013. Lecture Notes in Computer Science, vol 8052. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-40184-8_9
Download citation
DOI: https://doi.org/10.1007/978-3-642-40184-8_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-40183-1
Online ISBN: 978-3-642-40184-8
eBook Packages: Computer ScienceComputer Science (R0)