Game-based verification and synthesis

Infinite-duration games provide a convenient way to model distributed, reactive and open systems in which several entities and an uncontrollable environment interact. Here, each entitity as well as the uncontrollable environment are modelled as players.

A strategy for an entity player in the model corresponds directly to a program for the corresponding entity of the system. A strategy for a player which ensures that the player wins no matter how the other players behave then corresponds to a program ensuring that the specification of the entity is satisfied no matter how the other entities and the environment behaves. Synthesis of strategies in games can thus be used for automatic generation of correct-by-construction programs from specifications.

We consider verification and synthesis problems for several well-known game-based models. This includes both model-checking problems and satisfiability problems for logics capable of expressing strategic abilities of players in games with both qualitative and quantitative objectives.

A number of computational complexity results for model-checking and satisfiability problems in this domain are obtained. We also show how the technique of symmetry reduction can be extended to solve finitely-branching turn-based games more efficiently. Further, the novel concept of winning cores in parity games is introduced. We use this to develop a new polynomial-time under-approximation algorithm for solving parity games. Experimental results show that this algorithm performs better than the state-of-the-art algorithms in most benchmark games.

Two new game-based modelling formalisms for distributed systems are presented. The first makes it possible to reason about systems where several identical entities interact. The second provides a game-based modelling formalism for distributed systems with continuous time and probability distributions over the duration of delays. For these new models we provide decidability and undecidability results for problems concerning computation of symmetric Nash equilibria and for deciding existence of strategies that ensure reaching a target with a high probability.