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