×

On decidability and complexity of low-dimensional robot games. (English) Zbl 1436.91002

Summary: A robot game, also known as a \(\mathbb{Z}\)-VAS game, is a two-player vector addition game played on the integer lattice \(\mathbb{Z}^n\), where one of the players, Adam, aims to avoid the origin while the other player, Eve, aims to reach the origin. The problem is to decide whether or not Eve has a winning strategy. In this paper we prove undecidability of the two-dimensional robot game closing the gap between undecidable and decidable cases. We also prove that deciding the winner in a robot game with states in dimension one is \(\mathsf{EXPSPACE}\)-complete and study a subclass of robot games where deciding the winner is in \(\mathsf{EXPTIME}\).

MSC:

91A05 2-person games
68Q17 Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.)
68Q25 Analysis of algorithms and problem complexity
PDFBibTeX XMLCite
Full Text: DOI Link

References:

[1] Niskanen, R.; Potapov, I.; Reichert, J., Undecidability of two-dimensional robot games, (Proceedings of MFCS 2016. Proceedings of MFCS 2016, LIPIcs, vol. 58 (2016)), 73:1-73:13 · Zbl 1398.91012
[2] Niskanen, R., Robot games with states in dimension one, (Proceedings of RP 2016. Proceedings of RP 2016, LNCS, vol. 9899 (2016)), 163-176 · Zbl 1478.68194
[3] Alur, R.; Henzinger, T. A.; Kupferman, O., Alternating-time temporal logic, J. ACM, 49, 5, 672-713 (2002) · Zbl 1326.68181
[4] Kupferman, O.; Vardi, M. Y.; Wolper, P., An automata-theoretic approach to branching-time model checking, J. ACM, 47, 2, 312-360 (2000) · Zbl 1133.68376
[5] Walukiewicz, I., Pushdown processes: games and model-checking, Inf. Comput., 164, 2, 234-263 (2001) · Zbl 1003.68072
[6] Abdulla, P. A.; Mayr, R.; Sangnier, A.; Sproston, J., Solving parity games on integer vectors, (Proceedings of CONCUR 2013. Proceedings of CONCUR 2013, LNCS, vol. 8052 (2013)), 106-120 · Zbl 1390.68452
[7] Fahrenberg, U.; Juhl, L.; Larsen, K. G.; Srba, J., Energy games in multiweighted automata, (Proceedings of ICTAC 2011. Proceedings of ICTAC 2011, LNCS, vol. 6916 (2011)), 95-115 · Zbl 1350.68168
[8] Chatterjee, K.; Doyen, L., Energy parity games, Theor. Comput. Sci., 458, 49-60 (2012) · Zbl 1260.91039
[9] Abdulla, P. A.; Bouajjani, A.; d’Orso, J., Monotonic and downward closed games, J. Log. Comput., 18, 1, 153-169 (2008) · Zbl 1133.68042
[10] Brázdil, T.; Brozek, V.; Etessami, K., One-counter stochastic games, (Proceedings of FSTTCS 2010. Proceedings of FSTTCS 2010, LIPIcs, vol. 8 (2010)), 108-119 · Zbl 1245.68099
[11] Brázdil, T.; Jančar, P.; Kučera, A., Reachability games on extended vector addition systems with states, (Proceedings of ICALP 2010. Proceedings of ICALP 2010, LNCS, vol. 6199 (2010)), 478-489 · Zbl 1288.68179
[12] Reichert, J., On the complexity of counter reachability games, Fundam. Inform., 143, 3-4, 415-436 (2016) · Zbl 1357.68142
[13] Abdulla, P. A.; Bouajjani, A.; d’Orso, J., Deciding monotonic games, (Proceedings of CSL 2003. Proceedings of CSL 2003, LNCS, vol. 2803 (2003)), 1-14 · Zbl 1116.68491
[14] Doyen, L.; Rabinovich, A., Robot Games (2013), LSV, ENS Cachan, Personal website, 2011, Tech. Rep. LSV-13-02
[15] Haase, C.; Halfon, S., Integer vector addition systems with states, (Proceedings of RP 2014. Proceedings of RP 2014, LNCS, vol. 8762 (2014)), 112-124 · Zbl 1393.68115
[16] Blondin, M.; Finkel, A.; Göller, S.; Haase, C.; McKenzie, P., Reachability in two-dimensional vector addition systems with states is PSPACE-complete, (Proceedings of LICS 2015 (2015)), 32-43 · Zbl 1401.68095
[17] Blondin, M.; Finkel, A.; McKenzie, P., Well behaved transition systems, Log. Methods Comput. Sci., 13, 3, 1860-5974 (2017) · Zbl 1459.68138
[18] Blondin, M.; Haase, C.; Mazowiecki, F., Affine extensions of integer vector addition systems with states, (Proceedings of CONCUR 2018. Proceedings of CONCUR 2018, LIPIcs, vol. 118 (2018), Schloss Dagstuhl), 14:1-14:17 · Zbl 1520.68088
[19] Martin, D. A., Borel determinacy, Ann. Math., 102, 2, 363-371 (1975) · Zbl 0336.02049
[20] Arul, A.; Reichert, J., The complexity of robot games on the integer line, (Proceedings of QAPL 2013. Proceedings of QAPL 2013, EPTCS, vol. 117 (2013)), 132-148 · Zbl 1464.91027
[21] Reichert, J., Reachability Games With Counters: Decidability and Algorithms (2015), Laboratoire Spécification et Vérification, ENS Cachan: Laboratoire Spécification et Vérification, ENS Cachan France, Doctoral thesis
[22] Comon, H.; Cortier, V., Flatness is not a weakness, (Proceedings of CSL 2000. Proceedings of CSL 2000, LNCS, vol. 1862 (2000)), 262-276 · Zbl 0973.68142
[23] Comon, H.; Jurski, Y., Multiple counters automata, safety analysis and Presburger arithmetic, (Proceedings of CAV. Proceedings of CAV, LNCS, vol. 1427 (1998)), 268-279
[24] Comon, H.; Jurski, Y., Timed automata and the theory of real numbers, (Proceedings of CONCUR 1999. Proceedings of CONCUR 1999, LNCS, vol. 1664 (1999)), 242-257 · Zbl 0940.68092
[25] Leroux, J.; Penelle, V.; Sutre, G., The context-freeness problem is coNP-complete for flat counter systems, (Proceedings of ATVA 2014. Proceedings of ATVA 2014, LNCS, vol. 8837 (2014)), 248-263 · Zbl 1448.68270
[26] Leroux, J.; Sutre, G., Flat counter automata almost everywhere!, (Proceedings of ATVA 2005. Proceedings of ATVA 2005, LNCS, vol. 3707 (2005)), 489-503 · Zbl 1170.68519
[27] Minsky, M. L., Computation: Finite and Infinite Machines (1967), Prentice-Hall, Inc. · Zbl 0195.02402
[28] Hunter, P., Reachability in succinct one-counter games, (Proceedings of RP 2015. Proceedings of RP 2015, LNCS, vol. 9328 (2015)), 37-49 · Zbl 1471.68165
[29] (Grädel, E.; Thomas, W.; Wilke, T., Automata, Logics, and Infinite Games: A Guide to Current Research. Automata, Logics, and Infinite Games: A Guide to Current Research, LNCS, vol. 2500 (2002), Springer) · Zbl 1011.00037
[30] 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) · Zbl 1281.68160
[31] Jurdzinski, M.; Lazic, R.; Schmitz, S., Fixed-dimensional energy games are in pseudo-polynomial time, (Proceedings of ICALP 2015. Proceedings of ICALP 2015, LNCS, vol. 9135 (2015), Springer), 260-272 · Zbl 1440.68122
[32] Colcombet, T.; Jurdzinski, M.; Lazic, R.; Schmitz, S., Perfect half space games, (Proceedings of LICS 2017 (2017), IEEE Computer Society), 1-11 · Zbl 1452.91052
[33] Roux, S. L.; Pauly, A.; Raskin, J., Minkowski games, (STACS 2017. STACS 2017, LIPIcs, vol. 66 (2017)), 50:1-50:13 · Zbl 1402.91089
[34] Roux, S. L.; Pauly, A.; Raskin, J.-F., Minkowski games, ACM Trans. Comput. Log., 19, 3, 1-29 (2018) · Zbl 1407.91066
[35] Bouyer, P.; Hofman, P.; Markey, N.; Randour, M.; Zimmermann, M., Bounding average-energy games, (Foundations of Software Science and Computation Structures. Foundations of Software Science and Computation Structures, LNCS (2017), Springer), 179-195 · Zbl 1392.68115
[36] Chatterjee, K.; Velner, Y., Hyperplane separation technique for multidimensional mean-payoff games, J. Comput. Syst. Sci., 88, 236-259 (2017) · Zbl 1371.68107
[37] Korec, I., Small universal register machines, Theor. Comput. Sci., 168, 2, 267-301 (1996) · Zbl 0874.68105
[38] Halava, V.; Niskanen, R.; Potapov, I., On robot games of degree two, (Proceedings of LATA 2015. Proceedings of LATA 2015, LNCS, vol. 8977 (2015)), 224-236 · Zbl 1451.68150
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.