Game Equivalence and Bisimulation for Game Description Language

This paper investigates the equivalence between games represented by state transition models and its applications. We first define a notion of bisimulation equivalence between state transition models and prove that it can be logically characterized by Game Description Language (GDL). Then we introduce a concept of quotient state transition model. As the minimum equivalent of the original model, it allows us to improve the efficiency of model checking for GDL. Finally, we demonstrate with real games that bisimulation equivalence can be generalized to characterize more general game equivalence.