Event Category: Colloquium

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

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

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

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

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