In earlier work (with Komi Golov) we defined a notion of directed branching bisimulation and its associated positive Hennessy-Milner logic with until (PHMLU). It has the nice property that s is directed bisimular with t if and only if the PHMLU theory of s is a subset of the theory of t. This has various …continue reading

In many previous Colloquium talks, I have presented work on using mCRL2 to verify mutual exclusion algorithms under various models of shared register behaviour. In particular, we have looked at whether read and write operations on a register, which have duration, can overlap in time. If they can, we must consider how the overlapping operations …continue reading

Analysis of Markov models is of high importance for formal verification. Until now, analysis of Markov Automata required them to be fully specified, which is a considerable restriction as rates may be unknown or influenced by uncertainty of the environment. We introduce parametric Markov Automata (pMA) to capture this uncertainty with parametric transition functions. In …continue reading

Monitoring, or runtime verification, is a lightweight formal verification technique that analyzes individual executions rather than exploring the entire state space. In this talk, I will present one approach to monitoring in the context of STARK. Specifically, we consider DisTL, a logic for expressing properties about expected behavior of systems under uncertainty. Since the evaluation …continue reading

Quotients have only been studied for a handful of equivalences in the linear time-branching time spectrum, for which there are results pertaining to canonicity and minimality. We extend these results to weak simulation equivalence and coupled similarity, two closely related equivalences induced by simulation preorders. We describe abstract procedures for transforming an LTS into a …continue reading

We previously introduced initial work on Quasi Decision Diagrams (QDDs) which act as a replacement of Binary Decision Diagrams (BDDs). In this talk, we highlight the challenges faced when applying BDDs for model checking, and we discuss how QDDs may overcome them. Furthermore, we report results evaluating QDDs as potential replacement for BDDs on various …continue reading

Within the theory of model checking, one of the techniques to combat the state space explosion is symmetry reduction. The general idea of symmetry reduction is quite straightforward: to obtain a reduced model, we combine symmetric states. A key ingredient here is that we need to be able to identify which states are indeed symmetric. …continue reading

The Maeslant Barrier is a storm surge barrier that protects Rotterdam and its harbour from storm surges in the North Sea. Its software control consists of three major components, one of which is BesW. BesW is responsible for all the movements of the barrier except for pushing and pulling it. The software control of the …continue reading

The Open Interaction Language (OIL) is a state-machine language developed at Canon Production Printing that provides a formal yet accessible way to describe how components interact through sequences of actions. OIL emphasizes separation of concerns, enabling engineers to model different aspects of a system separately. This talk introduces OIL protocol specifications, which are used to …continue reading