Events at MF 6.132

The observable behavior of a system usually carries crucial information about its internal state, properties, and potential future behaviors. In this talk, I present a generic automata-theoretic synthesis approach to obtain most-specific verdicts from imperfect observations of an ongoing run of a system. Verdicts can be elements of any join-semilattice ordered by specificity. I show …continue reading

In [1], Rob van Glabbeek proved that there does not exist a compositional translation of pi-calculus into CCS that is valid up to strong barbed bisimilarity, but that there does exist a similarly valid compositional transition if the communication facility is of CCS is upgraded to ACP-style communication. In my talk, I will explore whether …continue reading

This paper presents an algorithm for synthesizing a supervisor for timed automata (TA) using the conventional supervisory control theory. The algorithm is directly applicable to TA without explicit transformation into finite automata, and iteratively strengthens the guards of edges labeled by controllable events and invariants of locations where the progression of time can be preempted …continue reading

This paper presents an algorithm for synthesizing a supervisor for timed automata (TA) using the conventional supervisory control theory. The algorithm is directly applicable to TA without explicit transformation into finite automata, and iteratively strengthens the guards of edges labeled by controllable events and invariants of locations where the progression of time can be preempted …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