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

To establish that some set X is a subset of greatest fixpoint nu f, we routinely show that X is a post-fixpoint, ie., X is a subset of f(X). This is a straightforward, constructive way of proving greatest fixpoints. However, for least fixpoints, constructive approaches such as fixpoint iteration break down when we consider subset …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

In this presentation, I shall introduce Autonomous Data Language, highlight its most important attributes and explain the main concepts of the language using some examples.

The principal objective of our ongoing IRF project “Programs in the wild: Uncertainties, adaptability, and verification” is to provide a formal framework and tools for modelling and verifying the behaviour of systems characterised by a close interaction of a program with an unpredictable environment, like Cyber-Physical Systems (CPSs). In this talk we will discuss the …continue reading

Almost all practical software systems today are configurable. Huge configuration spaces, usually of size exponential in the number of configuration options or features, render their design, analysis, and explanation challenging tasks. In this talk, I will introduce the notion of “feature causality” to support explainability of configurable systems. Inspired by the seminal definition of actual …continue reading