A relatively recent extension to type theory is “homotopy type theory”. This provides a new view on types, where a type A is interpreted as a topological space, a term t of type A is interpreted as a point in the space and a proof of an equality, p : q=t is interpreted as a …continue reading

In the previous presentation, I showed how we can model asynchronously communicating OIL components in mCRL2. Since then, we have added a “new” operator in OIL which enables users to create new instances of components dynamically. I show how we model the addition of this operator in mCRL2, which required significant changes. Also, I show …continue reading

Cordis models are industrial, UML like models. There are some semantical differences compared to standard UML. We verify Cordis models using a translation to mCRL2. In order to verify such models, we have to over several obstacles. In this talk, I will discuss three main challenges that we face so far: (1) the accurate translation …continue reading

GPUexplore is a tool that exploits the computational power of graphics processors to efficiently construct state spaces, and on-the-fly check safety and liveness properties. Its current main practical limitation, though, is related to its input language. The tool accepts networks of Labelled Transition Systems, which were initially useful to test whether state space could be …continue reading

What is the structure of a transition system that represent the behaviour of processes? We assumed that it was just an ordinary random graph, but got odd results when predicting the sizes of state spaces generated by lps2lts. Viewing state spaces as parallel non-communicating random state spaces gave far better results. This also helps in …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

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

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

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