GDL-Ⅱ is a logic-based knowledge representation formalism used in general game playing to describe the rules of arbitrary games, in particular those with incomplete information. In this paper, we use model checking to automatically verify that games specified in GDL-Ⅱ satisfy desirable temporal and knowledge conditions. We present a systematic translation of GDL-Ⅱ to a model checking language, prove the translation to be correct, and demonstrate the feasibility of applying model checking tools for GDL-Ⅱ games by four case studies.
展开▼
