## David N. Jansen: Revisiting Weak Simulation for Substochastic Markov Chains

The spectrum of branching-time relations for probabilistic systems has been investigated thoroughly by Baier, Hermanns, Katoen and Wolf (2003, 2005), including weak simulation for systems involving substochastic distributions. Weak simulation was proven to be sound *…continue reading*

## Mark Bouwman: Formal Modelling and Verification of an Interlocking using mCRL2

This paper presents an application of the formal modelling and model checking toolkit mCRL2 and the model-based testing tool JTorX in the signalling domain. The mCRL2 toolkit is used to formally model the behaviour of a *…continue reading*

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