## Ferry Timmers: ASD to mCRL2, translating and raking, a retrospective

The past year I’ve been working on finalizing a translation from ASD (a specification language for control systems used by the industry) to mCRL2. This was not a trivial task since I was left without a formal specification of ASD. What ensued was reverse-engineering and lots of testing with purposefully built models. In the end, *…continue reading*

## Tom Franken: Parallel Sorting Under Assumptions.

The talk will explore parallel sorting with the following assumptions on the parallel processors: The processors can only save a constant amount of parameters. The processors need references to access other processors. Notably, I’ll take a look at sorting networks and the AKS network and at Richard Cole’s Parallel Merge Sort algorithm, to see whether *…continue reading*

## 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*