## Jan Friso Groote: An O(m log n) algorithm for branching bisimulation

The O(m log n) algorithm for branching bisimulation devised by Groote/Jansen/Keiren/Wijs was primarily directed towards Kripke structures and not to labelled transition systems. To verify branching bisimulation for LTSs an explicit translation is made to Kripke structures. This *…continue reading*

## Hans Zantema: Symbolic model checking and bounded model checking

We discuss how to solve reachability problems either in BDD based symbolic model checking (by NuXMV) or by bounded model checking using SMT solving. We provide several examples, mainly from the practical assignments of the course *…continue reading*

## Ferry Timmers: A complete axiomatisation for probabilistic trace equivalence

Probabilistic labelled transition systems combine the expressiveness of Markov chains and processes. We are interested in finding a suitable trace equivalence for such systems, which becomes non-trival once non-determinism is introduced. For this search I *…continue reading*

## Jeroen Keiren: Tableaux for mu-calculus model checking of infinite state systems: a note on soundness

In 1992, Bradfield and Stirling presented a tableaux-based approach to local model checking of infinite-state systems that is sound and complete. When trying to apply this approach to model-checking timed and hybrid automata against mu-calculus *…continue reading*

## Allan van Hulst: The quest for the mythical 57-regular Moore graph

Since 1966 it is known that only four regular undirected graphs having diameter 2 and girth 5 can exist. The construction of three of these 5,2-Moore graphs is known but it is still an open *…continue reading*

## Rodin Aarssen: Concrete Syntax with Black Box Parsers

Meta programming is the art of writing software that takes source code as input for manipulation, analysis or code generation. Many meta programming systems reason about abstract syntax trees representing this source code, which requires intimate knowledge of *…continue reading*

## Wieger Wesselink: About the Design and Implementation of State Space Exploration in the mCRL2 toolset

An important use case of the mCRL2 tool set is state space exploration. An efficient and feature-rich implementation is available that works quite well in practice. Unfortunately the design of this implementation is quite complicated, *…continue reading*

## Rick Erkens: “Rewriting the Term Rewriter Part 1: Introduction and Matching”

In an mCRL2 specification the user can specify processes with data, that can in turn be manipulated through the computational model of term rewriting. The term rewriter that the toolset uses now is reasonably fast *…continue reading*

## Tim Willemse: Variability Parity Games

Parity games are two-player, infinite duration games that can be used answer whether a property holds true of a system with a yes or no. In several application domains, one is not only interested in *…continue reading*

## Jurriaan Rot: Coalgebra Learning via Duality

Automata learning is a popular technique for inferring minimal automata through membership and equivalence queries. We generalise learning from automata to a large class of state-based systems, using the theory of coalgebras. The approach relies *…continue reading*