Simon Borgbjerg Laursen will defend his thesis:
Synchronization and Control of Quantitative Systems
The defence takes place on Monday 28th of November 2016, 13:00, in room 0.2.13 at Selma Lagerlöfs Vej 300
Formal methods, such as model checking, theorem proving and static analysis, are used to provide confidence in system models and designs, as it can assist in all phases of system development and testing. However, formal modelling of software is not trivial, and the ever increasing demand for software functionality and the complexity of such software systems makes modelling even harder. This challenge creates the need for expressive and computationally feasible modelling and
specification formalisms. In this thesis, we explore modelling formalisms for quantitative systems and systems with partial observability to determine their computational limitations and feasibility.
In the first part of the thesis, we study the synchronization problem, where the objective is to find a sequence of inputs that reset a system without knowing what state the system started in. This objective was first studied for systems where no information is available about its current system state. We extend this to systems with partial observability, where the controller has some information about the current state. The objective is to find a synchronizing strategy that, based on the observations, gives the next input. For deterministic systems, we show that the computational complexity of finding synchronizing strategies remains the same as for the classical problem with no observability. We then extend the concept of synchronizing strategies to quantitative systems. In particular, we analyse when the controller has partial information about the current accumulated weight in a deterministic system. We prove the surprising result, that the existence of synchronizing strategy for such a system is decidable in polynomial time.
In the second part, we study quantitative games, i.e. games where part of the objective is to minimise or contain some quantitative value. In particular, average-energy games where objective aims to optimise the long-run average of the accumulated energy. We show that this objective arises naturally in several applications, and previous case studies. We prove that determining the winner in such games is in NP ∩ coNP and is at least as hard as solving mean-payoff games.
Then, we analyse in details the complexity of determining the winner average-energy games while maintaining the accumulated energy within given bounds. Finally, we study average-energy games where the bounds are existentially quantified.
Members of the assessment committee:
Professor Jean-Francois Raskin, Université Libre de Bruxelles
Associate Professor Thomas Troels Hildebrandt, ITU University of Copenhagen and
Associate Professor Manfred Jaeger, Aalborg University.
Professor Kim Guldstrand Larsen and Associate Professor Jiří Srba are the supervisors.
Moderator Associate Professor Brian Nielsen.
All interested parties are welcome. After the defense the department will be hosting a small reception in cluster 1.