Thomas Neele: Operations on Fixpoint Equation Systems, a formalisation in Coq.
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
Kevin Jilissen: Restricting SysML Activity Diagrams to facilitate formal analysis
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
Rick Erkens: Optimizing Term Rewriting with Creeper Trace Transducers
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
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
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