Master thesis defense in Algolog on Epistemic Planning (another one)

[Thomas Bolander]

Master thesis defense in Algolog. All are welcome.

Time: Monday 29 April, 13.00

Place: build. 322, room 030.

Speaker: Mads Pico Jensen.

Title of thesis: Conditional Epistemic Planning.

Best,

   Thomas

[Valentin Goranko]

Master thesis defense in AlgoLoG. All are welcome.

-----------------

Day and time: Thursday, 25 April, 11.00am

Venue: build. 305, room 053.

Student: Steen Vester

Title: Game-Theoretic and Computational Aspects of Concurrent Game Models

Supervisor: Valentin Goranko

External examiner: Peter Bro Miltersen, Aarhus University 

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 model-checking 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.

[Valentin Goranko]