An algorithm for searching states of game of Go based on symbolic model checking

The existing artificial intelligence techniques for games of Go have made remarkable achievements. However, the strongest AI for Go does not have a deterministic search capability. To address this issue, we introduce the model checking technique to the field of Go algorithms. First, we use an Alternating Finite Automaton (AFA) to establish a formal model for Go, and we employee a formula of Alternating-time Temporal Logic (ATL) to formalize win conditions. On the basis of it, the Go problem is mapped to the model checking problem between the ATL formula and the AFA. By employing the Ordered Binary Decision Diagram (OBDD) technique, we obtain a method for computing the least fixed point to implicitly perform model checking, in order to avoid the huge state space of Go that cause insufficient memory. As shown in the simulation results, the symbolic model checking can efficiently conduct some deterministic searches in the state space of Go.