Herman Geuvers: Apartness and Hennessy-Milner logic
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
Maurice Laveaux: Modern (Thread-Safe) Decision Diagram Library
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
Jeroen Keiren: An alternative characterization of fixed points
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
Jan Martens: Computing minimal distinguishing HML-formulas is NP-hard
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
Tim Willemse: On a relation between Failures Refinement and Model-Based Testing
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
Erik de Vink: Zielonka’s algorithm for variability parity games
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
Tom Franken: Autonomous Data Language for Parallel Programming
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.
Valentina Castiglioni: Uncertainties, adaptability, and verification
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
Clemens Dubslaff: “Feature Causality”
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