Relay Reachability Algorithm for Exploring Huge State Space 1

Since many desirable properties about finite-state model are expressed as a reachability problem, reachability algorithms have been extensively studied in model checking. On the other hand, reachability algorithms play an important role in game solving since reachability games are often described as a finite state model. In this sense, reachability algorithms are located in the intersection of the research areas of Model Checking and Artificial Intelligence.This paper interests in solving the reachability games called Push-Push. However, both exact and approximate reachability algorithms are not sufficient to the games since its state space is huge and requires lots of iterations such as 338 steps in the reachability computation. Thus we devise the new algorithm called relay reachability algorithm. It divides the global state space into several local ones. And exact reachability algorithm is applied on each local state space one by one. With these reachability algorithms, we solve all of the games.