Automated verification of state sequence invariants in general game playing

摘要

A general game player is a system that can play previously unknown games given nothing but their rules. Many of the existing successful approaches to general game playing require to generate some form of game-specific knowledge, but when current systems establish knowledge they rely on the approximate method of playing random sample matches rather than formally proving knowledge. In this paper, we present a theoretically founded and practically viable method for automatically verifying properties of games whose rules are given in the general Game Description Language (GDL). We introduce a simple formal language to describe game-specific knowledge as state sequence invariants, and we provide a proof theory for verifying these invariants with the help of Answer Set Programming. We prove the correctness of this method against the formal semantics for GDL, and we report on extensive experiments with a practical implementation of this proof system, which show that our method of formally proving knowledge is viable for the practice of general game playing.