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

## Mark Bouwman: Verifying the EULYNX level crossing

Even though the behaviour of the EULYNX specification of the level crossing is conceptually quite simple, the state space associated to the mCRL2 model is enormous. This Thursday I will present the reasons for the state space explosion and the measures we took to drastically reduce it. Moreover, I will present the verification efforts, which *…continue reading*

## Jos Baeten: Integration of automata theory and process theory

Since 2007, I have been working on a project to integrate automata theory and process theory. The motivation is to present students with a model of a computer in a basic course on the foundations of computer science, that relates more closely to computers as they know them. A recent result in this project is *…continue reading*

## Hans Zantema: The paint pot problem and common multiples in monoids

On a finite sequence of paint pots the following steps are allowed: * Swap two consecutive non-empty pots. * If the two neighbours of a non-empty pot are empty, then divide the paint in the middle pot over the two neighbours, after which these neighbours will be non-empty and the middle one will be empty. *…continue reading*

## Flip van Spaendonck: The Busy-Forbidden Protocol, an efficient shared-exclusive access lock

Mutual exclusion algorithms such as Peterson’s, make sure only a single thread can be present in the exclusive section at a given time. Similarly, a shared-exclusive lock also provides a shared section, in which any number of threads can be present, but only if no thread is present in the exclusive section. In this talk, *…continue reading*

## Rick Erkens: Regular tree languages and (dis)analogies with regular languages

Tree automata are a generalisation of finite automata over words. A tree automaton accepts a set of ranked ordered trees (terms if you will) just like a DFA accepts a set of words over an alphabet. Most interesting properties that regular languages enjoy, carry over to regular tree languages in some sense. I will present *…continue reading*

## Maurice Laveaux: On The Fly Solving for Symbolic Parity Games

In model checking we are interested in determining whether a property is satisfied for a given system. In particular, we want to know whether the property holds for the initial state of the system. We often see, especially while developing the model, that properties are already violated in relatively few steps from the initial state. *…continue reading*

## Yousra Hafidi: On starvation freedom property of Peterson’s mutual exclusion algorithm for more than 2 processes

It is well known that Peterson’s algorithm for two processes is starvation free. In this talk I study the generalization of Peterson’s algorithm to N>2 processes using tournament trees. In particular, I will show how, contrary to the two processes version, this algorithm is not starvation free if we do not make any fairness assumptions. *…continue reading*

## Herman Geuvers: “Computer Assisted Mathematical Proofs: using the computer to verify computers”

A “Proof Assistant” is a computer program that allows users to create complete mathematical proofs, interactively with the computer, where the computer checks each small reasoning step. In this way one obtains the utmost guarantee of correctness. I will outline how Proof Assistants work, how they are used to verify mathematical proofs and computer systems. Verifying a proof with a *…continue reading*

## Olav Bunte: Asynchronously communicating OIL components

In this presentation we focus on how we envision OIL components to communicate with each other. We define the behaviour of communicating OIL components using a formalism found in literature, namely the FIFO system, and we show how this can be modelled in mCRL2. Also, we show some typical unwanted behaviour in asynchronous communication and *…continue reading*