Myrthe Spronck: Completeness Criteria in Modal mu-Calculus Formulae
When verifying liveness properties on transition systems, it is often necessary to discard spurious counterexamples. This can be done through the application of completeness criteria: assumptions on which paths represent realistic executions of the modelled system. To support verification of properties under completeness criteria, we have developed template modal mu-calculus formulae that can be instantiated …continue reading
Jeroen Keiren: An Expressive Timed Modal Mu-Calculus for Timed Automata
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
Clemens Dubslaff: Explaining Control Strategies: Trees or Diagrams?
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
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