25 citations · 124 across the 16 of their papers we have counts for
13 papers · 1 filter
Efficient Evidence Generation for Modal -Calculus Model Checking (extended version)
Anna Stramaglia, Jeroen J. A. Keiren, Maurice Laveaux +1
Model checking is a technique to automatically assess whether a model of the behaviour of a system meets its requirements. Evidence explaining why the behaviour does (not) meet its…
Extensible Proof Systems for Infinite-State Systems
Jeroen J. A. Keiren, Rance Cleaveland
This paper revisits soundness and completeness of proof systems for proving that sets of states in infinite-state labeled transition systems satisfy formulas in the modal mu-calcul…
Fair Mutual Exclusion for N Processes (extended version)
Yousra Hafidi, Jeroen J. A. Keiren, Jan Friso Groote
Peterson's mutual exclusion algorithm for two processes has been generalized to processes in various ways. As far as we know, no such generalization is starvation free without…
Tutorial: Designing Distributed Software in mCRL2
Jan Friso Groote, Jeroen J. A. Keiren
Distributed software is very tricky to implement correctly as some errors only occur in peculiar situations. For such errors testing is not effective. Mathematically proving correc…
A simpler O(m log n) algorithm for branching bisimilarity on labelled transition systems
David N. Jansen, Jan Friso Groote, Jeroen J. A. Keiren +1
Branching bisimilarity is a behavioural equivalence relation on labelled transition systems that takes internal actions into account. It has the traditional advantage that algorith…
Games for Bisimulations and Abstraction
David De Frutos Escrig, Jeroen J. A. Keiren, Tim A. C. Willemse
Weak bisimulations are typically used in process algebras where silent steps are used to abstract from internal behaviours. They facilitate relating implementations to specificatio…
Parity Game Reductions
S. Cranen, J. J. A. Keiren, T. A. C. Willemse
Parity games play a central role in model checking and satisfiability checking. Solving parity games is computationally expensive, among others due to the size of the games, which,…
Stuttering equivalence is too slow!
David N. Jansen, Jeroen J. A. Keiren
Groote and Wijs recently described an algorithm for deciding stuttering equivalence and branching bisimulation equivalence, acclaimed to run in time. Unfort…
Benchmarks for Parity Games (extended version)
Jeroen J. A. Keiren
We propose a benchmark suite for parity games that includes all benchmarks that have been used in the literature, and make it available online. We give an overview of the parity ga…
Improved Static Analysis of Parameterised Boolean Equation Systems using Control Flow Reconstruction
Jeroen J. A. Keiren, Wieger Wesselink, Tim A. C. Willemse
We present a sound static analysis technique for fighting the combinatorial explosion of parameterised Boolean equation systems (PBESs). These essentially are systems of mutually r…
Stuttering Equivalence for Parity Games
Sjoerd Cranen, Jeroen J. A. Keiren, Tim A. C. Willemse
We study the process theoretic notion of stuttering equivalence in the setting of parity games. We demonstrate that stuttering equivalent vertices have the same winner in the parit…
Analysing the Control Software of the Compact Muon Solenoid Experiment at the Large Hadron Collider
Yi-Ling Hwong, Vincent J. J. Kusters, Tim A. C. Willemse
The control software of the CERN Compact Muon Solenoid experiment contains over 30,000 finite state machines. These state machines are organised hierarchically: commands are sent d…
Structural Analysis of Boolean Equation Systems
Jeroen Keiren, Michel A. Reniers, Tim A. C. Willemse
We analyse the problem of solving Boolean equation systems through the use of structure graphs. The latter are obtained through an elegant set of Plotkin-style deduction rules. Our…