The Experts below are selected from a list of 2640 Experts worldwide ranked by ideXlab platform
Misa Keinänen - One of the best experts on this subject based on the ideXlab platform.
-
Techniques for solving Boolean Equation systems
2006Co-Authors: Misa KeinänenAbstract:Boolean Equation systems are ordered sequences of Boolean Equations decorated with least and greatest fixpoint operators. Boolean Equation systems provide a useful framework for formal verification because various specification and verification problems, for instance, μ-calculus model checking can be represented as the problem of solving Boolean Equation systems. The general problem of solving a Boolean Equation system is a computationally hard task, and no polynomial time solution technique for the problem has been discovered so far. In this thesis, techniques for finding solutions to Boolean Equation systems are studied and new methods for solving such systems are devised. The thesis presents a general framework that allows for dividing Boolean Equation systems into individual blocks and solving these blocks in isolation with special techniques. Three special techniques are presented, namely: (i) new specialized algorithms for disjunctive and conjunctive form Boolean Equation systems, (ii) a new encoding of a general form Boolean Equation system into answer set programming, and (iii) new encodings of a general form Boolean Equation systems into satisfiability problems. The approaches (ii) and (iii) are motivated by the recent success of answer set programming solvers and satisfiability solvers in formal verification. First, the thesis presents especially fast solution algorithms for disjunctive and conjunctive classes of Boolean Equation systems. These special algorithms are useful because many practically relevant model checking problems can be represented as Boolean Equation systems that are disjunctive or conjunctive. The new algorithms have been implemented and the performance of the algorithms has been compared experimentally on communication protocol verification examples. Second, the thesis gives a translation of the problem of solving a general form Boolean Equation system into the problem of finding a stable model of a logic program. The translation allows to use implementations of answer set programming solvers to solve Boolean Equation systems. Experimental tests have been performed using the presented approach and these experiments indicate the usefulness of answer set programming in this problem domain. Third, the thesis presents reductions from the problem of solving general form Boolean Equation systems to the satisfiability problems of difference logic and propositional logic. The reductions allow to use implementations of satisfiability solvers to solve Boolean Equation systems. The presented reductions have been implemented and it is shown via experiments that the new approach leads to practically efficient methods to solve general Boolean Equation systems.
-
a sub quadratic algorithm for conjunctive and disjunctive Boolean Equation systems
International Colloquium on Theoretical Aspects of Computing, 2005Co-Authors: Jan Friso Groote, Misa KeinänenAbstract:We present a new algorithm for conjunctive and disjunctive Boolean Equation systems which arise frequently in the verification and analysis of finite state concurrent systems. In contrast to the previously known O(e2) time algorithms, our algorithm computes the solution to such a fixpoint Equation system with size e and alternation depth d in O(e log d) time (here d < e). We show the correctness and complexity of the algorithm. We discuss heuristics and describe how the algorithm can be efficiently implemented. The algorithm is compared to a previous solution via experiments on verification examples. Our measurements indicate that the new algorithm makes the verification of a large class of fixpoint expressions more tractable.
-
Obtaining Memory-Efficient Solutions to Boolean Equation Systems
Electronic Notes in Theoretical Computer Science, 2005Co-Authors: Misa KeinänenAbstract:This paper is concerned with memory-efficient solution techniques for Boolean fixed-point Equations. We show how certain structures of fixed-point Equation systems, often encountered in solving verification problems, can be exploited in order to substantially improve the performance of fixed-point computations. Also, we investigate the space complexity of the problem of solving Boolean Equation systems, showing a NL-hardness result. A prototype of the proposed technique has been implemented and experimental results on a series of protocol verification benchmarks are reported.
-
Solving alternating Boolean Equation systems in answer set programming
Lecture Notes in Computer Science, 2005Co-Authors: Misa Keinänen, Ilkka NiemeläAbstract:In this paper we apply answer set programming to solve alternating Boolean Equation systems. We develop a novel characterization of solutions for variables in disjunctive and conjunctive Boolean Equation systems. Based on this we devise a mapping from Boolean Equation systems with alternating fixed points to normal logic programs such that the solution of a given variable of an Equation system can be determined by the existence of a stable model of the corresponding logic program. The technique can be used to model check alternating formulas of modal μ-calculus.
-
INAP/WLP - Solving alternating Boolean Equation systems in answer set programming
Lecture Notes in Computer Science, 2005Co-Authors: Misa Keinänen, Ilkka NiemeläAbstract:In this paper we apply answer set programming to solve alternating Boolean Equation systems. We develop a novel characterization of solutions for variables in disjunctive and conjunctive Boolean Equation systems. Based on this we devise a mapping from Boolean Equation systems with alternating fixed points to normal logic programs such that the solution of a given variable of an Equation system can be determined by the existence of a stable model of the corresponding logic program. The technique can be used to model check alternating formulas of modal μ-calculus.
Tim A. C. Willemse - One of the best experts on this subject based on the ideXlab platform.
-
partial order reduction for parity games with an application on parameterised Boolean Equation systems
Tools and Algorithms for Construction and Analysis of Systems, 2020Co-Authors: Thomas Neele, Tim A. C. Willemse, Wieger WesselinkAbstract:Partial-order reduction (POR) is a well-established technique to combat the problem of state-space explosion. We propose POR techniques that are sound for parity games, a well-established formalism for solving a variety of decision problems. As a consequence, we obtain the first POR method that is sound for model checking for the full modal \(\mu \)-calculus. Our technique is applied to, and implemented for the fixed point logic called parameterised Boolean Equation systems, which provides a high-level representation of parity games. Experiments indicate that substantial reductions can be achieved.
-
finding compact proofs for infinite data parameterised Boolean Equation systems
Science of Computer Programming, 2020Co-Authors: Thomas Neele, Tim A. C. Willemse, Jan Friso GrooteAbstract:Abstract Parameterised Boolean Equation Systems (PBESs) can be used to represent many different kinds of decision problems. Most notably, model checking and equivalence problems can be encoded in a PBES. Traditional techniques to solve PBESs, such as instantiation techniques, cannot deal with PBESs with an infinite data domain. We propose an approach that can solve PBESs with infinite data by computing the bisimulation quotient of the underlying graph structure. Furthermore, we show how this technique can be improved by repeatedly searching for finite proofs. We also apply knowledge of intermediate solutions in an early termination heuristic. Unlike existing approaches, our technique is not restricted to subfragments of PBESs. Compared to similar procedures that operate on behavioural models, our technique is also more general: it is not restricted to model checking with finite action sets. Experimental results show that our ideas work well in practice and support a wider range of models and properties than state-of-the-art techniques.
-
evidence extraction from parameterised Boolean Equation systems
3rd International Workshop on Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2018), 2018Co-Authors: Wieger Wesselink, Tim A. C. WillemseAbstract:Model checking is a technique for automatically assessing the quality of software and hardware systems and designs. Given a formalisation of both the system behaviour and the requirements the system should meet, a model checker returns either a yes or a no. In case the answer is not as expected, it is desirable to provide feedback to the user as to why this is the case. Providing such feedback, however, is not straightforward if the requirement is expressed in a highly expressive logic such as the modal µ-calculus, and when the decision problem is solved using intermediate formalisms. In this paper, we show how to extract witnesses and counterexamples from parameterised Boolean Equation systems encoding the model checking problem for the first-order modal µ-calculus. We have implemented our technique in the modelling and analysis toolset mCRL2 and showcase our approach on a few illustrative examples.
-
solving parameterised Boolean Equation systems with infinite data through quotienting
Computer science reports, 2018Co-Authors: Thomas Neele, Tim A. C. Willemse, Jan Friso GrooteAbstract:Parameterised Boolean Equation Systems (PBESs) can be used to represent many different kinds of decision problems. Most notably, model checking and equivalence problems can be encoded in a PBES. Traditional instantiation techniques cannot deal with PBESs with an infinite data domain. We propose an approach that can solve PBESs with infinite data by computing the bisimulation quotient of the underlying graph structure. Furthermore, we show how this technique can be improved by repeatedly searching for finite proofs. Unlike existing approaches, our technique is not restricted to subfragments of PBESs. Experimental results show that our ideas work well in practice and support a wider range of models and properties than state-of-the-art techniques.
-
ARQNL@IJCAR - Evidence extraction from parameterised Boolean Equation systems
2018Co-Authors: Wieger Wesselink, Tim A. C. WillemseAbstract:Model checking is a technique for automatically assessing the quality of software and hardware systems and designs. Given a formalisation of both the system behaviour and the requirements the system should meet, a model checker returns either a yes or a no. In case the answer is not as expected, it is desirable to provide feedback to the user as to why this is the case. Providing such feedback, however, is not straightforward if the requirement is expressed in a highly expressive logic such as the modal µ-calculus, and when the decision problem is solved using intermediate formalisms. In this paper, we show how to extract witnesses and counterexamples from parameterised Boolean Equation systems encoding the model checking problem for the first-order modal µ-calculus. We have implemented our technique in the modelling and analysis toolset mCRL2 and showcase our approach on a few illustrative examples.
Jan Friso Groote - One of the best experts on this subject based on the ideXlab platform.
-
finding compact proofs for infinite data parameterised Boolean Equation systems
Science of Computer Programming, 2020Co-Authors: Thomas Neele, Tim A. C. Willemse, Jan Friso GrooteAbstract:Abstract Parameterised Boolean Equation Systems (PBESs) can be used to represent many different kinds of decision problems. Most notably, model checking and equivalence problems can be encoded in a PBES. Traditional techniques to solve PBESs, such as instantiation techniques, cannot deal with PBESs with an infinite data domain. We propose an approach that can solve PBESs with infinite data by computing the bisimulation quotient of the underlying graph structure. Furthermore, we show how this technique can be improved by repeatedly searching for finite proofs. We also apply knowledge of intermediate solutions in an early termination heuristic. Unlike existing approaches, our technique is not restricted to subfragments of PBESs. Compared to similar procedures that operate on behavioural models, our technique is also more general: it is not restricted to model checking with finite action sets. Experimental results show that our ideas work well in practice and support a wider range of models and properties than state-of-the-art techniques.
-
solving parameterised Boolean Equation systems with infinite data through quotienting
Computer science reports, 2018Co-Authors: Thomas Neele, Tim A. C. Willemse, Jan Friso GrooteAbstract:Parameterised Boolean Equation Systems (PBESs) can be used to represent many different kinds of decision problems. Most notably, model checking and equivalence problems can be encoded in a PBES. Traditional instantiation techniques cannot deal with PBESs with an infinite data domain. We propose an approach that can solve PBESs with infinite data by computing the bisimulation quotient of the underlying graph structure. Furthermore, we show how this technique can be improved by repeatedly searching for finite proofs. Unlike existing approaches, our technique is not restricted to subfragments of PBESs. Experimental results show that our ideas work well in practice and support a wider range of models and properties than state-of-the-art techniques.
-
Verification of Modal Formulas Using Parameterized Boolean Equation Systems
2014Co-Authors: Jan Friso Groote, Mohammad Reza MousaviAbstract:This chapter contains sections titled: 14.1 Boolean Equation systems, 14.2 Parameterized Boolean Equation systems, 14.3 Translation of modal formulas to parameterized Boolean Equation systems, 14.4 Techniques for solving parameterized Boolean Equation systems, 14.5 Historical notes
-
Parameterised Anonymity
Formal Aspects in Security and Trust, 2009Co-Authors: Jan Friso Groote, Simona OrzanAbstract:We introduce the notion of parameterised anonymity, to formalize the anonymity property of protocols with an arbitrary number of participants. This definition is an extension of the well known CSP anonymity formalization of Schneider and Sidiropoulos [18]. Using recently developed invariant techniques for solving parameterised Boolean Equation systems, we then show that the Dining Cryptographers protocol guarantees parameterised anonymity with respect to outside observers. We also argue that although the question whether a protocol guarantees parameterised anonymity is in general undecidable, there are practical subclasses where anonymity can be decided for any group of processes.
-
a sub quadratic algorithm for conjunctive and disjunctive Boolean Equation systems
International Colloquium on Theoretical Aspects of Computing, 2005Co-Authors: Jan Friso Groote, Misa KeinänenAbstract:We present a new algorithm for conjunctive and disjunctive Boolean Equation systems which arise frequently in the verification and analysis of finite state concurrent systems. In contrast to the previously known O(e2) time algorithms, our algorithm computes the solution to such a fixpoint Equation system with size e and alternation depth d in O(e log d) time (here d < e). We show the correctness and complexity of the algorithm. We discuss heuristics and describe how the algorithm can be efficiently implemented. The algorithm is compared to a previous solution via experiments on verification examples. Our measurements indicate that the new algorithm makes the verification of a large class of fixpoint expressions more tractable.
Ilkka Niemelä - One of the best experts on this subject based on the ideXlab platform.
-
Solving alternating Boolean Equation systems in answer set programming
Lecture Notes in Computer Science, 2005Co-Authors: Misa Keinänen, Ilkka NiemeläAbstract:In this paper we apply answer set programming to solve alternating Boolean Equation systems. We develop a novel characterization of solutions for variables in disjunctive and conjunctive Boolean Equation systems. Based on this we devise a mapping from Boolean Equation systems with alternating fixed points to normal logic programs such that the solution of a given variable of an Equation system can be determined by the existence of a stable model of the corresponding logic program. The technique can be used to model check alternating formulas of modal μ-calculus.
-
INAP/WLP - Solving alternating Boolean Equation systems in answer set programming
Lecture Notes in Computer Science, 2005Co-Authors: Misa Keinänen, Ilkka NiemeläAbstract:In this paper we apply answer set programming to solve alternating Boolean Equation systems. We develop a novel characterization of solutions for variables in disjunctive and conjunctive Boolean Equation systems. Based on this we devise a mapping from Boolean Equation systems with alternating fixed points to normal logic programs such that the solution of a given variable of an Equation system can be determined by the existence of a stable model of the corresponding logic program. The technique can be used to model check alternating formulas of modal μ-calculus.
Radu Mateescu - One of the best experts on this subject based on the ideXlab platform.
-
Partial Model Checking using Networks of Labelled Transition Systems and Boolean Equation Systems
Logical Methods in Computer Science, 2013Co-Authors: Frédéric Lang, Radu MateescuAbstract:Partial model checking was proposed by Andersen in 1995 to verify a temporal logic formula compositionally on a composition of processes. It consists in incrementally incorporating into the formula the behavioural information taken from one process - an operation called quotienting - to obtain a new formula that can be verified on a smaller composition from which the incorporated process has been removed. Simplifications of the formula must be applied at each step, so as to maintain the formula at a tractable size. In this paper, we revisit partial model checking. First, we extend quotienting to the network of labelled transition systems model, which subsumes most parallel composition operators, including $m$-among-$n$ synchronisation and parallel composition using synchronisation interfaces, available in the ELOTOS standard. Second, we reformulate quotienting in terms of a simple synchronous product between a graph representation of the formula (called formula graph) and a process, thus enabling quotienting to be implemented efficiently and easily, by reusing existing tools dedicated to graph compositions. Third, we propose simplifications of the formula as a combination of bisimulations and reductions using Boolean Equation systems applied directly to the formula graph, thus enabling formula simplifications also to be implemented efficiently. Finally, we describe an implementation in the CADP (Construction and Analysis of Distributed Processes) toolbox and present some experimental results in which partial model checking uses hundreds of times less memory than on-the-fly model checking.
-
Partial Model Checking using Networks of Labelled Transition Systems and Boolean Equation Systems
2012Co-Authors: Frédéric Lang, Radu MateescuAbstract:Partial model checking was proposed by Andersen in 1995 to verify a temporal logic formula compositionally on a composition of processes. It consists in incrementally incorporating into the formula the behavioural information taken from one process - an operation called quotienting - to obtain a new formula that can be verified on a smaller composition from which the incorporated process has been removed. Simplifications of the formula must be applied at each step, so as to maintain the formula at a tractable size. In this paper, we revisit partial model checking. First, we extend quotienting to the network of labelled transition systems model, which subsumes most parallel composition operators, including m among n synchronisation and parallel composition using synchronisation interfaces, available in the E-LOTOS standard. Second, we reformulate quotienting in terms of a simple synchronous product between a graph representation of the formula (called formula graph) and a process, thus enabling quotienting to be implemented efficiently and easily, by reusing existing tools dedicated to graph compositions. Third, we propose simplifications of the formula as a combination of bisimulations and reductions using Boolean Equation systems applied directly to the formula graph, thus enabling formula simplifications also to be implemented easily and efficiently. Finally, we describe an implementation in the CADP (Construction and Analysis of Distributed Processes) toolbox and present some experimental results in which partial model checking uses hundreds of times less memory than on-the-fly model checking.
-
TACAS - Partial model checking using networks of labelled transition systems and Boolean Equation systems
Tools and Algorithms for the Construction and Analysis of Systems, 2012Co-Authors: Frédéric Lang, Radu MateescuAbstract:Partial model checking was proposed by Andersen in 1995 to verify a temporal logic formula compositionally on a composition of processes. It consists in incrementally incorporating into the formula the behavioural information taken from one process -- an operation called quotienting -- to obtain a new formula that can be verified on a smaller composition from which the incorporated process has been removed. Simplifications of the formula must be applied at each step, so as to maintain the formula at a tractable size. In this paper, we revisit partial model checking. First, we extend quotienting to the network of labelled transition systems model, which subsumes most parallel composition operators, including m among n synchronisation and parallel composition using synchronisation interfaces, available in the E-Lotos standard. Second, we reformulate quotienting in terms of a simple synchronous product between a graph representation of the formula (called formula graph) and a process, thus enabling quotienting to be implemented efficiently and easily, by reusing existing tools dedicated to graph compositions. Third, we propose simplifications of the formula as a combination of bisimulations and reductions using Boolean Equation systems applied directly to the formula graph, thus enabling formula simplifications also to be implemented easily and efficiently. Finally, we describe an implementation in the CADP (Construction and Analysis of Distributed Processes) toolbox and present some experimental results in which partial model checking uses hundreds of times less memory than on-the-fly model checking.
-
Bisimulator 2.0: An On-the-Fly Equivalence Checker based on Boolean Equation Systems
2008Co-Authors: Radu Mateescu, Emilie OudotAbstract:Equivalence checking is a classical verification method determining if a finite-state concurrent system (protocol) satisfies its desired external behaviour (service) by comparing their underlying labeled transition systems (LTSs) modulo an appropriate equivalence relation. Local (or on-the-fly) equivalence checking explores the synchronous product of the LTSs incrementally, allowing an efficient detection of errors in complex systems. In this paper, we consider the technique based on translating the equivalence checking problem in terms of the local resolution of a Boolean Equation system (BES). We propose two enhancements of this technique in the case of equivalent LTSs: a new, faster BES encoding of weak equivalence relations, and a new local BES resolution algorithm with a good average complexity. These enhancements were incorporated into the BISIMULATOR 2.0 equivalence checker of the CADP toolbox, and led to significant performance improvements.
-
Improved On-the-Fly Equivalence Checking using Boolean Equation Systems
2008Co-Authors: Radu Mateescu, Emilie OudotAbstract:Equivalence checking is a classical verification method for ensuring the compatibility of a finite-state concurrent system (protocol) with its desired external behaviour (service) by comparing their underlying labeled transition systems (LTSs) modulo an appropriate equivalence relation. The local (or on-the-fly) approach for equivalence checking combats state explosion by exploring the synchronous product of the LTSs incrementally, thus allowing an efficient detection of errors in complex systems. However, when the two LTSs being compared are equivalent, the on-the-fly approach is outperformed by the global one, which completely builds the LTSs and computes the equivalence classes between states using partition refinement. In this paper, we consider the approach based on translating the on-the-fly equivalence checking problem in terms of the local resolution of a Boolean Equation system (BES). We propose two enhancements of the approach in the case of equivalent LTSs: a new, faster encoding of equivalence relations in terms of BESs, and a new local BES resolution algorithm with a better average complexity. These enhancements were incorporated into the BISIMULATOR 2.0 equivalence checker of the CADP toolbox, and they led to significant performance improvements w.r.t. existing on-the-fly equivalence checking algorithms.