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
Anna Stramaglia: lpsparunfold: features and application
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
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
Bas Luttik: About divergence-preserving branching bisimilarity
Jan Friso Groote: Another attempt to make BDDs more compact.
Quite some time ago I presented an approach to represent BDDs more compactly. The approach could be used to represent some formulas exponentially more compact than in ordinary BDDs. However, it was not possible to prove that this representation was never more than polynomially larger than BDDs. This approach turned out to be a particular …continue reading