@MASTERSTHESIS\{IMM2013-06538,
    author       = "S. Vester",
    title        = "Game-Theoretic and Computational Aspects of Concurrent Game Models",
    year         = "2013",
    school       = "Technical University of Denmark, {DTU} Compute, {E-}mail: compute@compute.dtu.dk",
    address      = "Matematiktorvet, Building 303{-B,} {DK-}2800 Kgs. Lyngby, Denmark",
    type         = "",
    note         = "{DTU} supervisor: Valentin Goranko, vfgo@dtu.dk, {DTU} Compute",
    url          = "http://www.compute.dtu.dk/English.aspx",
    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 verification of concurrent programs, distributed systems and communication protocols. In alternating-time temporal logic the semantics is typically defined 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 infinite 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 finite-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."
}