10月21日阮吉讲座：Model Checking Incomplete Information Games in General Game Playing
来源：会议讲座
作者：
时间：2014-10-20
Title: Model Checking Incomplete Information Games in General Game Playing
Speaker: Ji Ruan,Auckland University of Technology, New Zealand
Place: Room108, Teaching Bldg3,Peking University (北京大学第三教学楼108室)
Time: 15:10-18:00
Abstract: The AAAI General Game Playing Competition tests the ability of computer programs to play games in general, rather than just the ability to play a specific game. Participants in the competition are provided with previously unknown games, and are required to dynamically and autonomously determine how best to play these games. The Game Description Language (GDL) is a logic-based formalism for representing the rules of games with complete information, and is extended to GDL-II which allows to describe games with incomplete information. We use model checking to automatically verify that games specified in GDL-II satisfy desirable temporal and knowledge conditions. We present some complexity results for such decision problems. Also we give a systematic translation of GDL-II to a model checking language, prove the translation to be correct, and demonstrate the feasibility of applying model checking tools for GDL-II games by case studies.
Speaker: Ji Ruan,Auckland University of Technology, New Zealand
Place: Room108, Teaching Bldg3,Peking University (北京大学第三教学楼108室)
Time: 15:10-18:00
Abstract: The AAAI General Game Playing Competition tests the ability of computer programs to play games in general, rather than just the ability to play a specific game. Participants in the competition are provided with previously unknown games, and are required to dynamically and autonomously determine how best to play these games. The Game Description Language (GDL) is a logic-based formalism for representing the rules of games with complete information, and is extended to GDL-II which allows to describe games with incomplete information. We use model checking to automatically verify that games specified in GDL-II satisfy desirable temporal and knowledge conditions. We present some complexity results for such decision problems. Also we give a systematic translation of GDL-II to a model checking language, prove the translation to be correct, and demonstrate the feasibility of applying model checking tools for GDL-II games by case studies.