FormaSig aims to strengthen railway signalling standardization processes with the use of formal methods. The concrete approach investigated in FormaSig is to derive formal mCRL2 models from existing SysML specifications. These formal models are then used for two distinct purposes: (i) checking whether the original standard satisfies the requirements that are imposed upon them, and …continue reading

The mCRL2 toolset contains several applications in which computing the set of reachable states of a transition relation plays a role. For example in state space generation and in solving a PBES. List decision diagrams (LDDs) can be used to store sets of states and transitions in a compact manner. This has been demonstrated by …continue reading

We have studied the dual of bisimulation: the notion of “apartness”. Intuitively, two elements are apart if there is a positive way to distinguish them. Apartness is the dual of bisimilarity in a precise categorical sense: apartness is an initial algebra and gives rise to an induction principle. In the talk we will focus on the inductive nature of …continue reading

We take a look at k-DFAOs, which are Deterministic Finite Automata with Output with a special property: each k-DFAO represents a k-automatic sequence a, an infinite sequence in which the i-th element is the output the automata produces for the k-ary representation of i. Given any k-automatic sequence a, we define their complexity ||a||k as …continue reading

Whenever two Labelled Transition Systems (LTSs) are behaviourally inequivalent to each other, one may be interested why this is the case. Using a modal logic that characterises such a behavioural equivalence one can create formulae that distinguish these two LTSs, exposing the reason for the inequivalence. In this presentation I will describe the work by …continue reading

When targeting modern parallel hardware architectures, constructing correct and high-performing software is complex and time-consuming. In particular, reorderings of memory accesses that violate intended sequentially consistent behaviour are a major source of bugs. Applying synchronisation mechanisms to repair these should be done sparingly, as they negatively impact performance. In the past, both static analysis approaches and techniques …continue reading

Parity Games are infinite duration, two-player graph games. Such games play an important role in verification, satisfiability and synthesis. In recent years, several quasi-polynomial time algorithms for solving parity games have appeared. One of the more recent ones, by Pawel Parys, is based on the classical divide-and-conquer algorithm by McNaughton/Zielonka. In this talk, I will …continue reading

The field of process algebra provides a way to model (concurrent) processes algebraically. The syntax of a process calculus is described by an algebraic signature and the semantics is described by a set of operational rules. Strong bisimilarity and branching bisimilarity are two well known behavioral equivalences on processes. Informally two processes are strongly bisimilar …continue reading

Compositional minimisation can be an effective technique to reduce the state space explosion problem. This technique considers a parallel composition of several processes. In its simplest form, each sequential process is replaced by an abstraction, simpler than the corresponding process while still preserving the property that is checked. However, this technique cannot be applied in …continue reading