Showing 1–15 of 15 results for author: Keiren, J J A

Efficient Evidence Generation for Modal $μ$-Calculus Model Checking (extended version)

Authors: Anna Stramaglia, Jeroen J. A. Keiren, Maurice Laveaux, Tim A. C. Willemse

Abstract: 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 requirements is essential for the user to understand the model checking result. Willemse and Wesselink showed that parameterised Boolean equation systems (PBESs), an intermediate format for $μ$-calculus model checking,… ▽ More 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 requirements is essential for the user to understand the model checking result. Willemse and Wesselink showed that parameterised Boolean equation systems (PBESs), an intermediate format for $μ$-calculus model checking, can be extended with information to generate such evidence. Solving the resulting PBES is much slower than solving one without additional information, and sometimes even impossible. In this paper we develop a two-step approach to solving a PBES with additional information: we first solve its core and subsequently use the information obtained in this step to solve the PBES with additional information. We prove the correctness of our approach and we have implemented it, demonstrating that it efficiently generates evidence using both explicit and symbolic solving techniques. △ Less

Submitted 27 January, 2025; originally announced January 2025.

Comments: This is the extended version of the paper accepted for TACAS 2025

Expressiveness Results for Timed Modal Mu-Calculi

Authors: Rance Cleaveland, Jeroen J. A. Keiren, Peter Fontana

Abstract: This paper establishes relative expressiveness results for several modal mu-calculi interpreted over timed automata. These mu-calculi combine modalities for expressing passage of (real) time with a general framework for defining formulas recursively; several variants have been proposed in the literature. We show that one logic, which we call $L^{rel}_{ν,μ}$, is strictly more expressive than the ot… ▽ More This paper establishes relative expressiveness results for several modal mu-calculi interpreted over timed automata. These mu-calculi combine modalities for expressing passage of (real) time with a general framework for defining formulas recursively; several variants have been proposed in the literature. We show that one logic, which we call $L^{rel}_{ν,μ}$, is strictly more expressive than the other mu-calculi considered. It is also more expressive than the temporal logic TCTL, while the other mu-calculi are incomparable with TCTL in the setting of general timed automata. △ Less

Submitted 6 October, 2023; originally announced October 2023.

Extensible Proof Systems for Infinite-State Systems

Authors: Jeroen J. A. Keiren, Rance Cleaveland

Abstract: 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-calculus. Our results rely on novel results in lattice theory, which give constructive characterizations of both greatest and least fixpoints of monotonic functions over complete lattices. We show how these results may be used… ▽ More 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-calculus. Our results rely on novel results in lattice theory, which give constructive characterizations of both greatest and least fixpoints of monotonic functions over complete lattices. We show how these results may be used to reconstruct the sound and complete tableau method for this problem due to Bradfield and Stirling. We also show how the flexibility of our lattice-theoretic basis simplifies reasoning about tableau-based proof strategies for alternative classes of systems. In particular, we extend the modal mu-calculus with timed modalities, and prove that the resulting tableaux method is sound and complete for timed transition systems. △ Less

Submitted 26 July, 2022; originally announced July 2022.

Comments: Version with full proofs and technical details

Journal ref: ACM TOCL, 2023

Formal verification of an industrial UML-like model using mCRL2 (extended version)

Authors: Anna Stramaglia, Jeroen J. A. Keiren

Abstract: Low-code development platforms are gaining popularity. Essentially, such platforms allow to shift from coding to graphical modeling, helping to improve quality and reduce development time. The Cordis SUITE is a low-code development platform that adopts the Unified Modeling Language (UML) to design complex machine-control applications. In this paper we introduce Cordis models and their semantics. T… ▽ More Low-code development platforms are gaining popularity. Essentially, such platforms allow to shift from coding to graphical modeling, helping to improve quality and reduce development time. The Cordis SUITE is a low-code development platform that adopts the Unified Modeling Language (UML) to design complex machine-control applications. In this paper we introduce Cordis models and their semantics. To enable formal verification, we define an automatic translation of Cordis models to the process algebraic specification language mCRL2. As a proof of concept, we describe requirements of the control software of an industrial cylinder model developed by Cordis, and show how these can be verified using model checking. We show that our verification approach is effective to uncover subtle issues in the industrial model and its implementation. △ Less

Submitted 17 May, 2022; originally announced May 2022.

Comments: pre-print of a paper that is submitted to FMICS 2022

Fair Mutual Exclusion for N Processes (extended version)

Authors: Yousra Hafidi, Jeroen J. A. Keiren, Jan Friso Groote

Abstract: Peterson's mutual exclusion algorithm for two processes has been generalized to $N$ processes in various ways. As far as we know, no such generalization is starvation free without making any fairness assumptions. In this paper, we study the generalization of Peterson's algorithm to $N$ processes using a tournament tree. Using the mCRL2 language and toolset we prove that it is not starvation free u… ▽ More Peterson's mutual exclusion algorithm for two processes has been generalized to $N$ processes in various ways. As far as we know, no such generalization is starvation free without making any fairness assumptions. In this paper, we study the generalization of Peterson's algorithm to $N$ processes using a tournament tree. Using the mCRL2 language and toolset we prove that it is not starvation free unless weak fairness assumptions are incorporated. Inspired by the counterexample for starvation freedom, we propose a fair $N$-process generalization of Peterson's algorithm. We use model checking to show that our new algorithm is correct for small $N$. For arbitrary $N$, model checking is infeasible due to the state space explosion problem, and instead, we present a general proof that, for $N \geq 4$, when a process requests access to the critical section, other processes can enter first at most $(N-1)(N-2)$ times. △ Less

Submitted 3 November, 2021; originally announced November 2021.

Comments: To appear in TMPA'21

Tutorial: Designing Distributed Software in mCRL2

Authors: Jan Friso Groote, Jeroen J. A. Keiren

Abstract: 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 correctness is hard and time consuming, and therefore, it is rarely done. Fortunately, there is a technique in between, namely model checking, that, if applied with skill, is both efficient and able to find rare errors. In t… ▽ More 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 correctness is hard and time consuming, and therefore, it is rarely done. Fortunately, there is a technique in between, namely model checking, that, if applied with skill, is both efficient and able to find rare errors. In this tutorial we show how to create behavioural models of parallel software, how to specify requirements using modal formulas, and how to verify these. For that we use the mCRL2 language and toolset (https://www.mcrl2.org/). We discuss the design of an evolution of well-known mutual exclusion protocols, and how model checking not only provides insight in their behaviour and correctness, but also guides their design. △ Less

Submitted 21 April, 2021; originally announced April 2021.

Comments: Preprint of the paper that has been accepted as a tutorial for FORTE 2021

Deadlock in packet switching networks

Authors: Anna Stramaglia, Jeroen J. A. Keiren, Hans Zantema

Abstract: 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 notions of deadlock in the context of packet switching networks, to which we refer as global, local and weak deadlock. We establish the precise relations between these notions, and prove they characterize different sets o… ▽ More 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 notions of deadlock in the context of packet switching networks, to which we refer as global, local and weak deadlock. We establish the precise relations between these notions, and prove they characterize different sets of deadlocks. Moreover, we implement checking of deadlock freedom of packet switching networks using the symbolic model checker nuXmv. We show experimentally that the implementation is effective at finding subtle deadlock situations in packet switching networks. △ Less

Submitted 15 January, 2021; originally announced January 2021.

Comments: This is a version with full proofs of the preprint that was submitted to FSEN 2021, and accepted for publication in that conference (to appear in Springer LNCS)

A simpler O(m log n) algorithm for branching bisimilarity on labelled transition systems

Authors: David N. Jansen, Jan Friso Groote, Jeroen J. A. Keiren, Anton Wijs

Abstract: Branching bisimilarity is a behavioural equivalence relation on labelled transition systems that takes internal actions into account. It has the traditional advantage that algorithms for branching bisimilarity are more efficient than all algorithms for other weak behavioural equivalences, especially weak bisimilarity. With $m$ the number of transitions and $n$ the number of states, the classic… ▽ More Branching bisimilarity is a behavioural equivalence relation on labelled transition systems that takes internal actions into account. It has the traditional advantage that algorithms for branching bisimilarity are more efficient than all algorithms for other weak behavioural equivalences, especially weak bisimilarity. With $m$ the number of transitions and $n$ the number of states, the classic $O(m n)$ algorithm was recently replaced by an $O(m (\log \lvert \mathit{Act}\rvert + \log n))$ algorithm, which is unfortunately rather complex. This paper combines its ideas with the ideas from Valmari. This results in a simpler algorithm with complexity $O(m \log n)$. Benchmarks show that this new algorithm is also faster and often far more memory efficient than its predecessors. This makes it the best option for branching bisimulation minimisation and preprocessing for weak bisimulation of LTSs. △ Less

Submitted 6 November, 2019; v1 submitted 24 September, 2019; originally announced September 2019.

Comments: This technical report is also filed as Eindhoven Computer Science report 19-03

Report number: CSR-19-03

Games for Bisimulations and Abstraction

Authors: David De Frutos Escrig, Jeroen J. A. Keiren, Tim A. C. Willemse

Abstract: Weak bisimulations are typically used in process algebras where silent steps are used to abstract from internal behaviours. They facilitate relating implementations to specifications. When an implementation fails to conform to its specification, pinpointing the root cause can be challenging. In this paper we provide a generic characterisation of branching-, delayed-, $η$- and weak-bisimulation as… ▽ More Weak bisimulations are typically used in process algebras where silent steps are used to abstract from internal behaviours. They facilitate relating implementations to specifications. When an implementation fails to conform to its specification, pinpointing the root cause can be challenging. In this paper we provide a generic characterisation of branching-, delayed-, $η$- and weak-bisimulation as a game between Spoiler and Duplicator, offering an operational understanding of the relations. We show how such games can be used to assist in diagnosing non-conformance between implementation and specification. Moreover, we show how these games can be extended to distinguish divergences. △ Less

Submitted 21 November, 2017; v1 submitted 1 November, 2016; originally announced November 2016.

Journal ref: Logical Methods in Computer Science, Volume 13, Issue 4 (November 28, 2017) lmcs:2192

Parity Game Reductions

Authors: S. Cranen, J. J. A. Keiren, T. A. C. Willemse

Abstract: 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, for model checking problems, can easily contain $10^9$ vertices or beyond. Equivalence relations can be used to reduce the size of a parity game, thereby potentially alleviating part of the computational burden. We reco… ▽ More 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, for model checking problems, can easily contain $10^9$ vertices or beyond. Equivalence relations can be used to reduce the size of a parity game, thereby potentially alleviating part of the computational burden. We reconsider (governed) bisimulation and (governed) stuttering bisimulation, and we give detailed proofs that these relations are equivalences, have unique quotients and they approximate the winning regions of parity games. Furthermore, we present game-based characterisations of these relations. Using these characterisations our equivalences are compared to relations for parity games that can be found in the literature, such as direct simulation equivalence and delayed simulation equivalence. To complete the overview we develop coinductive characterisations of direct- and delayed simulation equivalence and we establish a lattice of equivalences for parity games. △ Less

Submitted 21 March, 2016; originally announced March 2016.

Stuttering equivalence is too slow!

Authors: David N. Jansen, Jeroen J. A. Keiren

Abstract: Groote and Wijs recently described an algorithm for deciding stuttering equivalence and branching bisimulation equivalence, acclaimed to run in $\mathcal{O}(m \log n)$ time. Unfortunately, the algorithm does not always meet the acclaimed running time. In this paper, we present two counterexamples where the algorithms uses $Ω(md)$ time. A third example shows that the correction is not trivial. In o… ▽ More Groote and Wijs recently described an algorithm for deciding stuttering equivalence and branching bisimulation equivalence, acclaimed to run in $\mathcal{O}(m \log n)$ time. Unfortunately, the algorithm does not always meet the acclaimed running time. In this paper, we present two counterexamples where the algorithms uses $Ω(md)$ time. A third example shows that the correction is not trivial. In order to analyse the problem we present pseudocode of the algorithm, and indicate the time that can be spent on each part of the algorithm in order to meet the desired bound. We also propose fixes to the algorithm such that it indeed runs in $\mathcal{O}(m \log n)$ time. △ Less

Submitted 22 September, 2016; v1 submitted 18 March, 2016; originally announced March 2016.

Comments: 11 pages

Corrections to A Menagerie of Timed Automata

Authors: Jeroen J. A. Keiren, Peter Fontana, Rance Cleaveland

Abstract: 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 locations have the same expressiveness as timed automata that allow false location invariants. Corrected con- structions are presented in this note, and the affected results are reproved. 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 locations have the same expressiveness as timed automata that allow false location invariants. Corrected con- structions are presented in this note, and the affected results are reproved. △ Less

Submitted 23 February, 2016; originally announced February 2016.

Comments: 9 pages, corrects a technical error in the ACM Computing Surveys paper mentioned in the title, that can be found at http://dx.doi.org/10.1145/2518102

Benchmarks for Parity Games (extended version)

Authors: Jeroen J. A. Keiren

Abstract: 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 games, including a description of how they have been generated. We also describe structural properties of parity games, and using these properties we show that our benchmarks are representative. With this work we provide a… ▽ More 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 games, including a description of how they have been generated. We also describe structural properties of parity games, and using these properties we show that our benchmarks are representative. With this work we provide a starting point for further experimentation with parity games. △ Less

Submitted 16 January, 2015; v1 submitted 11 July, 2014; originally announced July 2014.

Comments: The corresponding tool and benchmarks are available from https://github.com/jkeiren/paritygame-generator. This is an extended version of the paper that has been accepted for FSEN 2015

Improved Static Analysis of Parameterised Boolean Equation Systems using Control Flow Reconstruction

Authors: Jeroen J. A. Keiren, Wieger Wesselink, Tim A. C. Willemse

Abstract: We present a sound static analysis technique for fighting the combinatorial explosion of parameterised Boolean equation systems (PBESs). These essentially are systems of mutually recursive fixed point equations ranging over first-order logic formulae. Our method detects parameters that are not live by analysing a control flow graph of a PBES, and it subsequently eliminates such parameters. We show… ▽ More We present a sound static analysis technique for fighting the combinatorial explosion of parameterised Boolean equation systems (PBESs). These essentially are systems of mutually recursive fixed point equations ranging over first-order logic formulae. Our method detects parameters that are not live by analysing a control flow graph of a PBES, and it subsequently eliminates such parameters. We show that a naive approach to constructing a control flow graph, needed for the analysis, may suffer from an exponential blow-up, and we define an approximate analysis that avoids this problem. The effectiveness of our techniques is evaluated using a number of case studies. △ Less

Submitted 27 April, 2014; v1 submitted 24 April, 2013; originally announced April 2013.

Comments: This is an extended version containing full proofs, and results with both versions of our analysis. Scripts and results corresponding to this submission can be found at https://github.com/jkeiren/pbesstategraph-experiments

Stuttering Equivalence for Parity Games

Authors: Sjoerd Cranen, Jeroen J. A. Keiren, Tim A. C. Willemse

Abstract: 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 parity game. This means that solving a parity game can be accelerated by minimising the game graph with respect to stuttering equivalence. While, at the outset, it might not be clear that this strategy should pay off, our exp… ▽ More 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 parity game. This means that solving a parity game can be accelerated by minimising the game graph with respect to stuttering equivalence. While, at the outset, it might not be clear that this strategy should pay off, our experiments using typical verification problems illustrate that stuttering equivalence speeds up solving parity games in many cases. △ Less

Submitted 11 February, 2011; originally announced February 2011.

Comments: Version to appear in NFM 2011