Proving two processes equivalent modulo branching bisimulation can be quite difficult and laborious. The cones and foci method seeks to simplify proving equivalence by assuming that, in most implementations, internal actions progress towards a state in which only externally visible actions are possible. In this talk, we will discuss the original technique, its incompleteness, and …continue reading

Logics expressing spatial properties go back to Tarksi. Often their semantics is based on topological spaces. Cianza et al. propose to use instead so-called closure spaces as underlying mathematical structure, because closure spaces comprise topological spaces as well as standard Kripke frames. In this talk we exploit the fact that finite Kripke frames induce quasi-discrete …continue reading

I will discuss a process algebra with constants for the deadlocked and accepting processes, action prefixing, non-deterministic choice, sequencing, signals and conditions. As Jos Baeten already mentioned in his FSA colloquium talk of October 7, 2021, a process can be specified with a guarded recursive specification over this process algebra if, and only if, it …continue reading

In the FormaSig project we translate communicating SysML state machines to mCRL2. Selecting and executing a transition consists of several transitions in the mCRL2 model. These internal state machines can be considered unobservable and are renamed to tau. Since many of these internal transitions can be combined, the bisimulation quotient is orders of magnitude smaller …continue reading

Data types such as lists and structured sorts enable the creation of concise process models in mCRL2. However, static analysis tools such as constant elimination, parameter elimination and sum elimination only consider process parameters as a single unit in their analysis. Therefore, the added structure in process parameters negatively affects these static analysis techniques. Groote …continue reading

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