On decidability and complexity of low-dimensional robot games

作者:

Highlights:

摘要

A robot game, also known as a Z-VAS game, is a two-player vector addition game played on the integer lattice Zn, 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 EXPSPACE-complete and study a subclass of robot games where deciding the winner is in EXPTIME.

论文关键词:Reachability games,Vector addition game,Decidability,Winning strategy,Integer vector addition system

论文评审过程:Received 13 December 2016, Revised 24 July 2019, Accepted 9 August 2019, Available online 20 August 2019, Version of Record 6 October 2019.

论文官网地址:https://doi.org/10.1016/j.jcss.2019.08.003