In many games the outcome of the players’ actions is given stochastically rather than deterministically, e.g., in card games, board games with dice (Risk!), etc.
However, the literature of logic-based languages for strategic reasoning has so far fallen short of expressing probabilities in the specification language itself.
The aim of this project is to extend the Alternating-time Temporal Logic ATL, one of the most widely-studied logic for strategic reasoning , to account for probabilities, as well as to model in general stochastic aspects of games of imperfect information.
Your contribution: You will define an extension of the logic ATL to account for probabilities. This language will be interpreted on games of imperfect information. You will study the model checking problem in this setting and devise model checking algorithms for the verification of properties of interest in games. If time allows, you will implement these algorithms in a model checking tool, possibly built on top of the MCMAS model checker for multi-agent systems .