PhD defence: Quantitative Systems: Efficient Reasoning under Uncertainty

On Friday, November 6, 13:00, Anders Mariegaard will defend his PhD thesis. Due to the current circumstance, the defence will be held online via Microsoft Teams.

If you wish to attend the defence online, please send an email to Peter Dolog, who will send you an invitation prior to the event.

Online rules

• Please stick to the following rules to make the best of an unfortunate situation. 
• Be aware that you must be muted during the entire session
• Please leave your camera off
• For questions, please use the chat function
• The defence will start at precisely 13:00. The session is open from 12:30. You are not allowed to join after the defence starts, neither during the break or examination

Abstract:

As the number of embedded software systems encountered in our daily life is ever increasing, it is imperative that these systems function as expected. The problem is exacerbated by the fact that modern systems, such as Cyber-physical systems (CPS), must not only function on its own, but must also interact with an uncontrollable and uncertain environment.

An approach to verifying such systems is model-checking, relying on abstract mathematical models of the system and its requirements specification, to automatically prove whether or not the model satisfies the requirements. If the model faithfully represents the real system, the computed verdict holds also for the real system.

As most systems naturally incorporate quantitative aspects, there is thus a need for formalisms that naturally support non-functional aspects, such as consumption/production of resources, timing information and aspects of uncertainty, such as
probabilistic behavior.

In this thesis, we therefore propose formalisms and algorithms to support efficient verification of quantitative systems under uncertainty. We first consider uncertainty in specifications and behavioral relations. For weighted systems, we consider how to quantify the behavioral differences between two systems. Concretely, we show how to compute a distance that captures the difference in branching behavior, also for systems where some of the concrete weights are unknown at design-time.

For probabilistic systems where the probabilities are uncertain and drawn from an interval of probabilities, we present three different semantic interpretations, together with associated model-checking algorithms.

The second part of the thesis develops efficient symbolic local algorithms for model-checking quantitative probabilistic systems. For a given model and formula, we reduce the model-checking problem to fixed-point computations on a structure that encodes inter-dependencies that naturally arise from the inductive definition of satisfaction of the formula by the model.

For probabilistic multiplayer games, an implementation is provided, together with an experimental evaluation showing performance comparable to the state-of-the-art tool PRISM-GAMES, on several scalable models.

Finally, we consider a case-study involving energy consumption forecasting of comfort cooling for an office building equipped with solar cells to generate energy and means to store energy. We model the case study in the tool UPPAAL-STRATEGO and using its statistical methods and machine learning techniques, we show how to synthesize near-optimal control strategies.

Members of the assessment committee are:

• Associate Professor Peter Dolog, Aalborg University,
• Senior Researcher Radu Mateescu, INRIA Grenoble - Rhone-Alpes, and
• Maitre de Conferences, HDR Didier Lime, École Centrale de Nantes.
   
• Professor Kim Guldstrand Larsen is Anders Mariegaard’s supervisor.
• The moderator is Associate Professor Brian Nielsen.

All interested parties are welcome.