Automated verification of state sequence invariants in general game playing

Sebastian Haufe; Michael Thielscher

doi:10.1016/j.artint.2012.04.003

Automated verification of state sequence invariants in general game playing

Sebastian Haufe
, Michael Thielscher

Department of Computer Science

Reykjavik University

Research output: Contribution to journal › Article › peer-review

Abstract

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.

Original language	English
Pages (from-to)	1-30
Number of pages	30
Journal	Artificial Intelligence
Volume	187-188
DOIs	https://doi.org/10.1016/j.artint.2012.04.003
Publication status	Published - Aug 2012

Bibliographical note

Funding Information: We thank the anonymous reviewers for their very valuable, extensive feedback and constructive suggestions for improving the paper. This research was supported under Australian Research Council’s (ARC) Discovery Projects funding scheme (project number DP 120102023) and by the Icelandic Centre for Research (RANNIS, grant number 210019). Michael Thielscher is the recipient of an ARC Future Fellowship (project number FT 0991348). He is also affiliated with the University of Western Sydney.

Other keywords

Answer set programming
General game playing
Knowledge representation

Access to Document

10.1016/j.artint.2012.04.003

Cite this

@article{57a54a49626945bc83dca7e051532f6d,

title = "Automated verification of state sequence invariants in general game playing",

abstract = "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.",

keywords = "Answer set programming, General game playing, Knowledge representation",

author = "Sebastian Haufe and Michael Thielscher",

note = "Funding Information: We thank the anonymous reviewers for their very valuable, extensive feedback and constructive suggestions for improving the paper. This research was supported under Australian Research Council{\textquoteright}s (ARC) Discovery Projects funding scheme (project number DP 120102023) and by the Icelandic Centre for Research (RANNIS, grant number 210019). Michael Thielscher is the recipient of an ARC Future Fellowship (project number FT 0991348). He is also affiliated with the University of Western Sydney.",

year = "2012",

month = aug,

doi = "10.1016/j.artint.2012.04.003",

language = "English",

volume = "187-188",

pages = "1--30",

journal = "Artificial Intelligence",

issn = "0004-3702",

publisher = "Elsevier B.V.",

}

TY - JOUR

T1 - Automated verification of state sequence invariants in general game playing

AU - Haufe, Sebastian

AU - Thielscher, Michael

N1 - Funding Information: We thank the anonymous reviewers for their very valuable, extensive feedback and constructive suggestions for improving the paper. This research was supported under Australian Research Council’s (ARC) Discovery Projects funding scheme (project number DP 120102023) and by the Icelandic Centre for Research (RANNIS, grant number 210019). Michael Thielscher is the recipient of an ARC Future Fellowship (project number FT 0991348). He is also affiliated with the University of Western Sydney.

PY - 2012/8

Y1 - 2012/8

N2 - 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.

AB - 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.

KW - Answer set programming

KW - General game playing

KW - Knowledge representation

UR - https://www.scopus.com/pages/publications/84860160773

U2 - 10.1016/j.artint.2012.04.003

DO - 10.1016/j.artint.2012.04.003

M3 - Article

SN - 0004-3702

VL - 187-188

SP - 1

EP - 30

JO - Artificial Intelligence

JF - Artificial Intelligence

ER -

Automated verification of state sequence invariants in general game playing

Abstract

Bibliographical note

Other keywords

Access to Document

Fingerprint

Cite this