In the untimed setting, it is well-known that the modal mu-calculus is more expressive than other modal logics such as LTL, CTL and CTL*. It can thus be considered a foundational logic for model-checking. In the timed setting, the status of similarly foundational logics is less satisfactory. There are timed extensions of modal logics, such …continue reading

Decision trees (DTs) are widely used to represent control strategies, e.g., for machine learning classifiers or formal verification results. Decisions in DTs are based on expressive predicates, but they seem to not fully exploit their potential towards concise representations. One reason is in their tree structure, leading to isomorphic subtrees not being merged. Reduced ordered …continue reading

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

Deterministic finite automata (DFAs) are perhaps one of the simplest models of computation. A classic result is that if two automata with n states are language inequivalent, then there is a word of length at most n that is accepted by only one of the automata, i.e. the word is distinguishing. In a sense this …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

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