Abstract
A new research result in this paper shows the decidability, and the TOWER upper bound on complexity, of solving parity multi-energy games (with given initial credit) in the framework of extended vector addition systems with states (where some components in the change vectors are not fixed but can be made arbitrarily large). The result is not deep w.r.t. the state-of-the-art, since it can be shown by a simple reduction to the version without the parity condition that was solved by Brázdil, Jančar, and Kučera (ICALP 2010). Besides giving the reduction, the main aim of the paper is to highlight the crucial ideas of a direct (self-contained) proof of the result; a particular novelty here is a natural attractor construction that seems to have not been used in this context so far.
Supported by the Grant Agency of the Czech Rep., project GAČR:15-13784S
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abdulla, P., Bouajjani, A., d’Orso, J.: Monotonic and downward closed games. Journal of Logic and Computation 18(1), 153–169 (2008). (a preliminary version appeared at CSL/KGC 2003)
Abdulla, P.A., Atig, M.F., Hofman, P., Mayr, R., Kumar, K.N., Totzke, P.: Infinite-state energy games. In: Proc. of CSL-LICS 2014, pp. 7:1–7:10. ACM Press (2014)
Abdulla, P.A., Mayr, R., Sangnier, A., Sproston, J.: Solving parity games on integer vectors. In: D’Argenio, P.R., Melgratti, H. (eds.) CONCUR 2013 – Concurrency Theory. LNCS, vol. 8052, pp. 106–120. Springer, Heidelberg (2013)
Blondin, M., Finkel, A., Göller, S., Haase, C., McKenzie, P.: Reachability in two-dimensional vector addition systems with states is PSPACE-complete. In: Proc. of LICS 2015. ACM Press (2015)
Borosh, I., Flahive, M., Treybig, B.: Small solutions of linear Diophantine equations. Discrete Mathematics 58, 215–220 (1986)
Brázdil, T., Chatterjee, K., Kučera, A., Novotný, P.: Efficient controller synthesis for consumption games with multiple resource types. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 23–38. Springer, Heidelberg (2012)
Brázdil, T., Kiefer, S., Kučera, A., Novotný, P., Katoen, J.P.: Zero-reachability in probabilistic multi-counter automata. In: Proc. of CSL-LICS 2014, pp. 22:1–22:10. ACM Press (2014)
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)
Chaloupka, J.: Z-reachability problem for games on 2-dimensional vector addition systems with states is in P. Fundam. Inform. 123(1), 15–42 (2013). (a preliminary version appeared at the Workshop on Reachability Problems 2010)
Chatterjee, K., Doyen, L.: Energy parity games. Theor. Comput. Sci. 458, 49–60 (2012). (a preliminary version appeared at ICALP 2010)
Chatterjee, K., Randour, M., Raskin, J.: Strategy synthesis for multi-dimensional quantitative objectives. Acta Inf. 51(3–4), 129–163 (2014). (a preliminary version appeared at CONCUR 2012)
Courtois, J.-B., Schmitz, S.: Alternating vector addition systems with states. In: Csuhaj-Varjú, E., Dietzfelbinger, M., Ésik, Z. (eds.) MFCS 2014, Part I. LNCS, vol. 8634, pp. 220–231. Springer, Heidelberg (2014)
Esparza, J.: Decidability and complexity of Petri net problems - an introduction. In: Reisig, W., Rozenberg, G. (eds.) APN 1998. LNCS, vol. 1491, pp. 374–428. Springer, Heidelberg (1998)
Fahrenberg, U., Juhl, L., Larsen, K.G., Srba, J.: Energy games in multiweighted automata. In: Cerone, A., Pihlajasaari, P. (eds.) ICTAC 2011. LNCS, vol. 6916, pp. 95–115. Springer, Heidelberg (2011)
Finkel, A., Goubault-Larrecq, J.: The theory of WSTS: the case of complete WSTS. In: Haddad, S., Pomello, L. (eds.) PETRI NETS 2012. LNCS, vol. 7347, pp. 3–31. Springer, Heidelberg (2012)
Juhl, L., Guldstrand Larsen, K., Raskin, J.-F.: Optimal bounds for multiweighted and parametrised energy games. In: Liu, Z., Woodcock, J., Zhu, H. (eds.) Theories of Programming and Formal Methods. LNCS, vol. 8051, pp. 244–255. Springer, Heidelberg (2013)
Jurdziński, M., Lazić, R., Schmitz, S.: Fixed-dimensional energy games are in pseudo-polynomial time. In: Halldórsson, M.M., Iwama, K., Kobayashi, N., Speckmann, B. (eds.) ICALP 2015. LNCS, vol. 9135, pp. 260–272. Springer, Heidelberg (2015)
Kosaraju, S., Sullivan, G.: Detecting cycles in dynamic graphs in polynomial time. In: Proceedings of STOC 1988, pp. 398–406. ACM Press (1988)
Leroux, J., Schmitz, S.: Reachability in vector addition systems demystified. In: Proc. of LICS 2015. ACM Press (2015)
Rackoff, C.: The covering and boundedness problems for vector addition systems. Theoretical Computer Science 6, 223–231 (1978)
Raskin, J., Samuelides, M., van Begin, L.: Games for counting abstractions. Electr. Notes Theor. Comput. Sci. 128(6), 69–85 (2005)
Velner, Y., Chatterjee, K., Doyen, L., Henzinger, T.A., Rabinovich, A.M., Raskin, J.: The complexity of multi-mean-payoff and multi-energy games. Inf. Comput. 241, 177–196 (2015). (based on versions appearing at FSTTCS 2010 and FoSSaCS 2011)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Jančar, P. (2015). On Reachability-Related Games on Vector Addition Systems with States. In: Bojanczyk, M., Lasota, S., Potapov, I. (eds) Reachability Problems. RP 2015. Lecture Notes in Computer Science(), vol 9328. Springer, Cham. https://doi.org/10.1007/978-3-319-24537-9_6
Download citation
DOI: https://doi.org/10.1007/978-3-319-24537-9_6
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-24536-2
Online ISBN: 978-3-319-24537-9
eBook Packages: Computer ScienceComputer Science (R0)