## Jan Martens: Lowerbounds for partition refinement algorithms that decide bisimilarity

Most of the algorithms that decide strong bisimilarity for LTSs can be classified as partition refinement algorithms. This includes the most efficient and well-known Paige-Tarjan algorithm. In recent work we establish an Omega((m+n) log n) lowerbound for the time complexity of these partition refinement algorithms, matching the time complexity of the Paige-Tarjan algorithm. However there *…continue reading*

## Tim Willemse: On quotients for equivalences on transition systems

There is a wealth of equivalence relations on labelled transition systems; see, e.g., Van Glabbeek’s linear-time branching-time spectrum. Some of these equivalences have found their way in tool sets such as mCRL2, where they are used either to compare two transition systems, or to reduce the size of a transition system. The latter is often *…continue reading*

## Herman Geuvers: Programming with Higher Inductive Types

A relatively recent extension to type theory is “homotopy type theory”. This provides a new view on types, where a type A is interpreted as a topological space, a term t of type A is interpreted as a point in the space and a proof of an equality, p : q=t is interpreted as a *…continue reading*

## Olav Bunte: Dynamic systems of communicating OIL components

In the previous presentation, I showed how we can model asynchronously communicating OIL components in mCRL2. Since then, we have added a “new” operator in OIL which enables users to create new instances of components dynamically. I show how we model the addition of this operator in mCRL2, which required significant changes. Also, I show *…continue reading*

## Yousra Hafidi: Verifying Cordis models using mCRL2: some challenges

Cordis models are industrial, UML like models. There are some semantical differences compared to standard UML. We verify Cordis models using a translation to mCRL2. In order to verify such models, we have to over several obstacles. In this talk, I will discuss three main challenges that we face so far: (1) the accurate translation *…continue reading*

## Anton Wijs: Memory Efficient State Space Exploration on GPUs for Concurrent State Machines with Data

GPUexplore is a tool that exploits the computational power of graphics processors to efficiently construct state spaces, and on-the-fly check safety and liveness properties. Its current main practical limitation, though, is related to its input language. The tool accepts networks of Labelled Transition Systems, which were initially useful to test whether state space could be *…continue reading*

## Jan Friso Groote: On the random structure of behavioural transition systems.

What is the structure of a transition system that represent the behaviour of processes? We assumed that it was just an ordinary random graph, but got odd results when predicting the sizes of state spaces generated by lps2lts. Viewing state spaces as parallel non-communicating random state spaces gave far better results. This also helps in *…continue reading*

## Anna Stramaglia: Semantics of UML State Machine Diagrams – overview and ambiguities

The Unified Modeling Language (UML), proposed by the Object Management Group (OMG), is a general purpose modeling language which became the standard for modeling system’ structure and behaviour. A UML model offers different views of the system in the form of various diagrams. The talk’s focus are UML State Machine Diagrams, widely used to specify *…continue reading*

## Thomas Neele: Compositional Learning of Synchronous Automata

The classical L* algorithm for learning DFAs runs in polynomial time with the size of the DFA being learnt. However, the DFA that represents a system consisting of multiple parallel components can grow exponentially in the number of components; known as the state space explosion problem. In this talk I will demonstrate how, given the *…continue reading*

## Erik de Vink: In search of for stability: cancelativity for probabilistic bisimulation

In an ongoing project on the complete axiomatization of branching probabilistic bisimulation, we are currently focusing on a cancellation property. We see a route of proving the property by means of topological arguments which seems a bit far-fetched. As a possible alternative approach we propose the notion of a stable process. A process is stable *…continue reading*