## Maximilian Köhl: Most-Specific Verdictors for Imperfectly Observable Systems

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*

## Bas Luttik: On the translation of pi-calculus into mCRL2

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*

## Michel Reniers: Supervisory Control Synthesis of Timed Automata Using Forcible Events

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*

## Jan Martens: Smaller proofs(?) for the language inequivalence of two DFAs

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*

## Cancelled – Michel Reniers: Supervisory Control Synthesis of Timed Automata Using Forcible Events

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*

## Thomas Neele: Characterising the Winning Strategies in Binary Parity Games with Propositional Logic

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*

## Pieter van Gelder: Probabilistic risk assessment of civil infrastructural systems

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*

## Valentina Castiglioni: A formal framework for Cyber-Physical Systems

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*

## Matthias Volk: Continuous-Time Markov Chains with Imprecisely Timed Observations

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*

## Flip van Spaendonck: (Semi-)Automate Extraction of Behavioral Models from C++ Code

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*