The past year I’ve been working on finalizing a translation from ASD (a specification language for control systems used by the industry) to mCRL2. This was not a trivial task since I was left without a formal specification of ASD. What ensued was reverse-engineering and lots of testing with purposefully built models. In the end, …continue reading

The talk will explore parallel sorting with the following assumptions on the parallel processors: The processors can only save a constant amount of parameters. The processors need references to access other processors. Notably, I’ll take a look at sorting networks and the AKS network and at Richard Cole’s Parallel Merge Sort algorithm, to see whether …continue reading

Most of the algorithms that decide strong bisimilarity for LTSs can be classified as partition refinement algorithms. This includes the most efficient and well-known Paige-Tarjan algorithm. In recent work we establish an Omega((m+n) log n) lowerbound for the time complexity of these partition refinement algorithms, matching the time complexity of the Paige-Tarjan algorithm. However there …continue reading

There is a wealth of equivalence relations on labelled transition systems; see, e.g., Van Glabbeek’s linear-time branching-time spectrum. Some of these equivalences have found their way in tool sets such as mCRL2, where they are used either to compare two transition systems, or to reduce the size of a transition system. The latter is often …continue reading

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