A parity game is an infinite-duration game between two players who pass a token around in a directed graph. The problem of “solving” a parity game (deciding which player wins a given node) is an interesting problem since it is in UP and co-UP, but not known to be in P. In a binary parity …continue reading

In this lecture I will discuss a number of methods and techniques for the probabilistic risk assessment of civil infrastructural systems, which includes extreme value statistics, system decompositioning techniques, and cost benefit analyses for risk-based optimisation. The flood defence system of the Netherlands will be used as a case study to illustrate the applicability of …continue reading

Cyber-Physical Systems (CPS) are characterised by the interaction of various agents operating under highly changing and, sometimes, unpredictable environmental conditions. It is therefore fundamental to verify whether these systems are robust, i.e., whether they are able to function correctly even in perturbed circumstances. In this talk I will recap the achievements of my project on …continue reading

Labeled continuous-time Markov chains (CTMCs) describe processes subject to random timing and partial observability. In applications such as runtime monitoring or calculation of remaining useful life, we must incorporate past observations. The timing of these observations matters but they may be uncertain. We consider a setting in which we are given a sequence of imprecisely …continue reading

Accurate behavioral models of software systems can be incredibly useful thanks to the vast array of model based techniques that exist, e.g. automated testing through model based testing, verification of requirements using modal formulas, or providing visual insight using state space visualization techniques. However, acquiring such models can be quite difficult. We propose a set …continue reading

The quantitative modal mu-calculus is equal to the modal mu-calculus except that formulas yield real values including (-)infinity instead of true or false. Quantitative modal formulas can be translated to parameterised real equation systems (PRESs), and subsequently to real equation systems (RESs), which is quite similar as translating to PBESs and BESs in case of …continue reading

In this talk, I will focus on a work-in-progress behavioral abstraction enabling the comparison of two modelling methods. The first method is an adaption of the current modelling methodology at Rijkswaterstaat for tunnel control systems based on SysML Activity Diagrams, as introduced in my previous talk. The second method relies on the Dezyne specification language …continue reading