Offre de stage Master 2, équipe COSMO IBISC : « The Verification of General Game Playing »

/, Offre Doctorat/Post-Doctorat/Stage, Recherche, Recrutement/Offre de stage Master 2, équipe COSMO IBISC : « The Verification of General Game Playing »

Offre de stage Master 2, équipe COSMO IBISC : « The Verification of General Game Playing »

Sujet : « The Verification of General Game Playing »

Background

General Game Player (GGP) [1] is a paradigm in Artificial Intelligence focused on developing algorithms and techniques to play more than one game successfully, possibly with limited prior knowledge of the game in hand. By contrast, for several games (such as chess, checkers, go) computers are programmed to play them using specially designed algorithm, which cannot be easily transferred from one game to another. In this context, the Game Description Language (GDL) [2,3] has been developed to represent games in GGP. This logic-based language allows to describe games from a game-theoretic perspective, specifying initial states, winning positions, and available moves.

Objectives

 The main goal of this project is to endowed GDL with model checking techniques, thus allowing for the automated verification of game-theoretical notions and solution concepts.

GDL supports compact representation by using a conceptualization of game states as databases and by relying on logic to define the notions of legal move, state update, etc. You will define a translation of GDL into ISLP, the specification language of the MCMAS model checker, one of the most widely-used model checkers for multi-agent systems [4]. Then, you will test extensively the verification of properties of games expressed in GDL.

More precisely, the proposed project is structured as follows:

  1. Preliminary study of the state of art on GGP and GDL.
  2. Definition of a translation from GDL into ISLP.
  3. Formalisation of various properties of games in ISPL, including winning conditions, existence of (dominant, winning) strategies.
  4. Experimental evaluation in MCMAS of the formalisations in point (2) and (3).

This internship is part of the ongoing ANR PRC project AGAPE (https://anr.fr/Projet-ANR-18-CE23-0013), coordinated by the Université de Toulouse – IRIT.

Start/End date: January-June 2021 (6 months)

Level: Master 2

 Location: Laboratoire IBISC, Bâtiment IBGBI,  Évry

How to apply

Please send an up-to-date CV to the project supervisor, Dr Francesco Belardinelli, at francescoDOTbelardinelliATuniv-evryDOTfr .

References

[1] M. Genesereth, M. Thielscher; General Game Playing. Synthesis Lectures on Artificial Intelligence and Machine Learning, Morgan & Claypool Publishers 2014

[2] M. Thielscher; A General Game Description Language for Incomplete Information Games. AAAI 2010

[3] M. Genesereth, N. Love, B. Pell; General game playing: Overview of the AAAI competition. AI Magazine 2005

[4] https://vas.doc.ic.ac.uk/software/mcmas/ Keywords: Formal Methods, General Game Playing, Game Description Language, Logics for Strategies.