Event Category: Colloquium

Fixpoint equation systems over arbitrary complete lattices generalise several established formalisms such as parity games and parameterised Boolean equation systems. We identify a number of elementary operations, such as swapping equations and substituting variables by their definitions and prove their correctness. All proofs are formalised in Coq. In this talk, I will go into the …continue reading

SysML has several modeling techniques for defining the behavior of a system. In this talk, we have a closer look on modeling system behavior using activity diagrams and the underlying semantics of these diagrams.  Next, we take a dive into the usage of SysML Activity Diagrams within the generic tunnel control system models of Rijkswaterstaat. …continue reading

In a previous talk I discussed our work on algorithms for optimized term normalization. We use a so-called set automaton to find pattern matches efficiently, and upon discovering a reducible subterm we apply the reduction while preserving as much matching information as possible. By integrating the structure of the right-hand sides into the automaton, we …continue reading

Apartness is the opposite (dual) of bisimulation. Intuitively, two states in a system are apart if there is a positive way to distinguish them. Apartness is an inductive notion, so we have a deduction system for proving that two states are apart, and if we cannot prove they are apart, they are bisimilar. This works …continue reading

Some time ago we have introduced a thread-safe term library in the mCRL2 toolset and have transformed some of the algorithms to parallelised variants. Similarly, we rely on a thread-safe decision diagram with parallelised algorithms for computing symbolic reachability and bisimulation. These (highly efficient) implementations often sacrifice readability of source code for the purpose of …continue reading

The Hennessy-Milner Logic (HML) is a modal logic that expresses behavioural properties of states in LTSs. We are interested in explaining behavioural inequivalence by constructing a formula that /distinguishes/ a pair of states, i.e. a formula that is true in exactly one of the states. Cleaveland presented a method to generate a HML-formula by back-tracking …continue reading

Modelling the behaviour of a system, and stepwise refining that model until it has become sufficiently detailed to generate executable implementation is an appealing approach to software development, advocated by companies such as, e.g. Verum. The approach is rooted in solid mathematics and supported by tools, such as mCRL2, that help the developer. Under the …continue reading

Model checking approaches to software product lines are doubly cursed. Not only high-dimensionality regarding the number of states may be troublesome, also the exponential number of options for a product raises a computational hindrance. In order to mitigate the latter, family-based verification, as opposed to product-based verification, has been proposed. In this talk we consider …continue reading

Concise process models in mCRL2 can be obtained by the use of data types such as lists and structured sorts. However, the addition of structure in the process parameters negatively affects static analysis tools such as constant elimination, parameter elimination and sum elimination which consider process parameters as single units in their analysis. To address …continue reading