Model checking for stochastic games

by Alessandro Bruni for PRISM Model Checker

This project will focus on implementing model checking techniques for stochastic games. The main goal of the project is to gain support for LTL model checking on the stochastic games engine, and to further improve the games engine itself by solving the equilibriums through strategy iteration techniques. This will improve the analysis of stochastic games both in expressive power and in efficiency.