Origin semantics introduced by Bojańczyk is a fine grained semantics for transducers, that not only expresses the relation between input and output words, but also includes a function that given an output position returns the input position where it was produced: the origin. In this talk we’ll discuss resynchronizations, a tool to relax the notion …continue reading

Assume we have a directed graph. We can find the strongly connected components in this graph using for instance Tarjan’s algorithm. Let’s say we remove an edge from the graph. Can we recalculate the SCCs? A (recent) paper by Bernstein, Probst et.al. presents a way tot do this efficiently. I’ll roughly discuss my experiences with …continue reading

The EULYNX initiative is a collaborative effort of more than ten European railway infrastructure managers to standardise signalling interfaces. Within EULYNX, FormaSig aims to use formal methods to analyse the correctness of the standard. We have recently concluded a case study in which we translate the EULYNX Point interface from SysML to mCRL2. The resulting …continue reading

We propose efficient family-based Software Product Lines (SPL) model checking  based on variability parity games. These extend parity games with conditional edges labelled with (feature) configurations. We validate our contribution by experiments on SPL benchmark models, which demonstrate that a novel family-based algorithm to collectively solve variability parity games, using symbolic representations of the configuration …continue reading

In model checking, partial-order reduction (POR) is an effective technique to reduce the size of the state space. Stubborn sets are an established variant of POR and have seen many applications over the past 31 years. One of the early works on stubborn sets shows that a combination of several conditions on the reduction is …continue reading

This work got started while teaching a functional programming course, where I tried to make the abstract concept of F-(co-)algebras more concrete by stating that, in Java terms, these are just classes that implement a specific kind of generic interface. To make this even more concrete, I tried to implement this idea, together with the …continue reading

A mutual exclusion algorithm is called speed independent if its correctness does not depend on the relative speed of the components. Famous mutual exclusion protocols such as Dekker’s, Peterson’s and Lamport’s bakery are meant to be speed independent. In this talk I argue that speed-independent mutual exclusion may not be implementable on standard hardware, depending …continue reading

Abstract: In the field of automata learning, similar to model-based testing, a target machine is sent interrogative queries with the goal of uncovering its behaviour. The most common algorithm for this in the industry is L*_Mealy, a Mealy-machine-learning variant of Dana Angluin’s 1987 L*. In its current implementation, no means of filtering queries is available. …continue reading