PhD Defence by Steen Vester, Friday 28 October 2016 at 13:00, Technical University of Denmark, Building 101, Meeting Center room S09.
Read more about this thesis in DTU Orbit - the official research database of the Technical University of Denmark, DTU.
Abstract:
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 entity 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-byconstruction
programs from high-level 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 in this domain are obtained. We also show how the technique of symmetry
reduction can be extended from the traditional non-deterministic setting to a game-based setting. Further, the
novel concept of wining cores in parity games is introduced. We use this to develop a new polynomial-time underapproximation
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
equilbria and for deciding existence of strategies that ensure reaching a target with a high probaility.
Supervisor: Associate Professor Michael Reichhardt Hansen, DTU Compute.
Co-supervisor: Professor Valentin F Goranko, Stockholm University, Sweden.
Examiners:
Associate Professor Carsten Witt, DTU Compute (Chair).
Prof. Dr. Ernst-Rüdiger Olderog, Universität Oldenburg, Germany.
Professor Kim Guldstrand Larsen, Aalborg University, Denmark.
Chairman of the proceedings:
Professor Jan Madsen, DTU Compute.
Everyone is welcome