Game-Theoretic and Computational Aspects of Concurrent Game Models |
Steen Vester
|
| Abstract | Concurrent games provide a very expressive way of modelling the interaction between agents in reactive systems with infinite behavior. We analyze the model-checking problem of the alternating-time temporal logics ATL and ATL interpreted over concurrent game models. This problem has applications in program synthesis and formal veri fication of concurrent programs, distributed systems and communication protocols. In alternating-time temporal logic the semantics is typically de fined such that players can either remember the whole history of a game (perfect recall semantics) or remember nothing about the history of a game (memoryless semantics). Perfect recall strategies have the advantage that many games can be solved when players have access to infi nite memory, but this also leads to high complexity (and undecidability in some cases) of the modelchecking problem. With memoryless strategies many fewer games can be solved, but on the other hand the complexity of model-checking is much lower, due to the vast restriction of the strategy space. We propose to consider fi nite-memory semantics as an intermediate case. This is introduced both with a bounded memory size and with an unbounded memory size. This notion is introduced to be able to solve more games than with memoryless semantics, but without getting as high complexity as for perfect recall semantics. Therefore we study the expressiveness of the new types of semantics as well as the complexity of the model-checking problem. This is done for ATL and ATL in both complete and incomplete information concurrent games. |
| Type | Master's thesis [Academic thesis] |
| Year | 2013 |
| Publisher | Technical University of Denmark, DTU Compute, E-mail: compute@compute.dtu.dk |
| Address | Matematiktorvet, Building 303-B, DK-2800 Kgs. Lyngby, Denmark |
| Series | IMM-M.Sc.-2013-11 |
| Note | DTU supervisor: Valentin Goranko, vfgo@dtu.dk, DTU Compute |
| Electronic version(s) | [pdf] |
| Publication link | http://www.compute.dtu.dk/English.aspx |
| BibTeX data | [bibtex] |
| IMM Group(s) | Computer Science & Engineering |