25 citations · 124 across the 16 of their papers we have counts for
16 papers
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…
Formal verification of an industrial UML-like model using mCRL2 (extended version)
Anna Stramaglia, Jeroen J. A. Keiren
Low-code development platforms are gaining popularity. Essentially, such platforms allow to shift from coding to graphical modeling, helping to improve quality and reduce developme…
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…
Deadlock in packet switching networks
Anna Stramaglia, Jeroen J. A. Keiren, Hans Zantema
A deadlock in a packet switching network is a state in which one or more messages have not yet reached their target, yet cannot progress any further. We formalize three different n…
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…
Corrections to A Menagerie of Timed Automata
Jeroen J. A. Keiren, Peter Fontana, Rance Cleaveland
This note corrects a technical error in the ACM Computing Surveys paper mentioned in the title. The flaw involved constructions for showing that timed automata with urgent location…
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…