References of "Boigelot, Bernard"
     in
Bookmark and Share    
Full Text
Peer Reviewed
See detailCounting the solutions of Presburger equations without enumerating them
Boigelot, Bernard ULg; Latour, Louis

in Theoretical Computer Science (2004), 313(1), 17-29

The Number Decision Diagram (NDD) has recently been introduced as a powerful representation system for sets of integer vectors. NDDs can notably be used for handling sets defined by arbitrary Presburger ... [more ▼]

The Number Decision Diagram (NDD) has recently been introduced as a powerful representation system for sets of integer vectors. NDDs can notably be used for handling sets defined by arbitrary Presburger formulas, which makes them well suited for representing the set of reachable states of finite-state systems extended with unbounded integer variables. In this paper, we address the problem of counting the number of distinct elements in a set of numbers or, more generally, of vectors, represented by an NDD. We give an algorithm that is able to produce an exact count without enumerating explicitly the vectors, which makes it capable of handling very large sets. As an auxiliary result, we also develop an efficient projection method that allows to construct efficiently NDDs from quantified formulas, and thus makes it possible to apply our counting technique to sets specified by formulas. Our algorithms have been implemented in the verification tool LASH, and applied successfully to various counting problems. [less ▲]

Detailed reference viewed: 12 (4 ULg)
Full Text
Peer Reviewed
See detailHybrid Acceleration using Real Vector Automata
Boigelot, Bernard ULg; Herbreteau, Frédéric; Jodogne, Sébastien ULg

in Lecture Notes in Computer Science (2003, July), 2725

This paper addresses the problem of computing an exact and effective representation of the set of reachable configurations of a linear hybrid automaton. Our solution is based on accelerating the state ... [more ▼]

This paper addresses the problem of computing an exact and effective representation of the set of reachable configurations of a linear hybrid automaton. Our solution is based on accelerating the state-space exploration by computing symbolically the repeated effect of control cycles. The computed sets of configurations are represented by Real Vector Automata (RVA), the expressive power of which is beyond that of the first-order additive theory of reals and integers. This approach makes it possible to compute in finite time sets of configurations that cannot be expressed as finite unions of convex sets. The main technical contributions of the paper consist in a powerful sufficient criterion for checking whether a hybrid transformation (i.e., with both discrete and continuous features) can be accelerated, as well as an algorithm for applying such an accelerated transformation on RVA. Our results have been implemented and successfully applied to several case studies, including the well-known leaking gas burner, and a simple communication protocol with timers. [less ▲]

Detailed reference viewed: 16 (4 ULg)
Full Text
Peer Reviewed
See detailIterating transducers in the large
Boigelot, Bernard ULg; Legay, A.; Wolper, Pierre ULg

in Lecture Notes in Computer Science (2003), 2725

Checking infinite-state systems is frequently done by encoding infinite sets of states as regular languages. Computing such a regular representation of, say, the reachable set of states of a system ... [more ▼]

Checking infinite-state systems is frequently done by encoding infinite sets of states as regular languages. Computing such a regular representation of, say, the reachable set of states of a system requires acceleration techniques that can finitely compute the effect of an unbounded number of transitions. Among the acceleration techniques that have been proposed, one finds both specific and generic techniques. Specific techniques exploit the particular type of system being analyzed, e.g. a system manipulating queues or integers, whereas generic techniques only assume that the transition relation is represented by a finite-state transducer, which has to be iterated. In this paper, we investigate the possibility of using generic techniques in cases where only specific techniques have been exploited so far. Finding that existing generic techniques are often not applicable in cases easily handled by specific techniques, we have developed a new approach to iterating transducers. This new approach builds on earlier work, but exploits a number of new conceptual and algorithmic ideas, often induced with the help of experiments, that give it a broad scope, as well as good performance. [less ▲]

Detailed reference viewed: 28 (7 ULg)
Full Text
Peer Reviewed
See detailOn Iterating Linear Transformations over Recognizable Sets of Integers
Boigelot, Bernard ULg

in Theoretical Computer Science (2003), 309(1-3), 413-468

It has been known for a long time that the sets of integer vectors that are recognizable by finite-state automata are those that can be defined in an extension of Presburger arithmetic. In this paper, we ... [more ▼]

It has been known for a long time that the sets of integer vectors that are recognizable by finite-state automata are those that can be defined in an extension of Presburger arithmetic. In this paper, we address the problem of deciding whether the closure of a linear transformation preserves the recognizable nature of sets of integer vectors. We solve this problem by introducing an original extension of the concept of recognizability to sets of vectors with complex components. This generalization allows to obtain a simple necessary and sufficient condition over linear transformations, in terms of the eigenvalues of the transformation matrix. We then show that these eigenvalues do not need to be computed explicitly in order to evaluate the condition, and we give a full decision procedure based on simple integer arithmetic. The proof of this result is constructive, and can be turned into an algorithm for applying the closure of a linear transformation that satisfies the condition to a finite-state representation of a set. Finally, we show that the necessary and sufficient condition that we have obtained can straightforwardly be turned into a sufficient condition for linear transformations with linear guards. [less ▲]

Detailed reference viewed: 22 (5 ULg)
Full Text
See detailRepresenting arithmetic constraints with finite automata: An overview
Boigelot, Bernard ULg; Wolper, Pierre ULg

in Lecture Notes in Computer Science (2002, July), 2401

Linear numerical constraints and their first-order theory, whether defined over the reals or the. integers, are basic tools that appear in many areas of Computer Science. This paper overviews a set of ... [more ▼]

Linear numerical constraints and their first-order theory, whether defined over the reals or the. integers, are basic tools that appear in many areas of Computer Science. This paper overviews a set of techniques based on finite automata that lead to decision procedures and other useful algorithms, as well as to a normal form, for the first-order linear theory of the integers, of the reals, and of the integers and reals combined. This approach has led to an implemented tool, which has the so far unique capability of handling the linear. first-order theory of the integers and reals combined. [less ▲]

Detailed reference viewed: 28 (7 ULg)
Full Text
Peer Reviewed
See detailOn the Use of Weak Automata for Deciding Linear Arithmetic with Integer and Real Variables
Boigelot, Bernard ULg; Jodogne, Sébastien ULg; Wolper, Pierre ULg

in Lecture Notes in Computer Science (2001), 2083

This paper considers finite-automata based algorithms for handling linear arithmetic with both real and integer variables. Previous work has shown that this theory can be dealt with by using finite ... [more ▼]

This paper considers finite-automata based algorithms for handling linear arithmetic with both real and integer variables. Previous work has shown that this theory can be dealt with by using finite automata on in finite words, but this involves some difficult and delicate to implement algorithms. The contribution of this paper is to show, using topological arguments, that only a restricted class of automata on in finite words are necessary for handling real and integer linear arithmetic. This allows the use of substantially simpler algorithms and opens the path to the implementation of a usable system for handling this combined theory. [less ▲]

Detailed reference viewed: 27 (6 ULg)
Full Text
Peer Reviewed
See detailCounting the Solutions of Presburger Equations without Enumerating Them
Boigelot, Bernard ULg; Latour, Louis

in Lecture Notes in Computer Science (2001), 2494

The Number Decision Diagram (NDD) has recently been proposed as a powerful representation system for sets of integer vectors. In particular, NDDs can be used for representing the sets of solutions of ... [more ▼]

The Number Decision Diagram (NDD) has recently been proposed as a powerful representation system for sets of integer vectors. In particular, NDDs can be used for representing the sets of solutions of arbitrary Presburger formulas, or the set of reachable states of some systems using unbounded integer variables. In this paper, we address the problem of counting the number of distinct elements in a set of vectors represented as an NDD. We give an algorithm that is able to perform an exact count without enumerating explicitly the vectors, which makes it capable of handling very large sets. As an auxiliary result, we also develop an efficient projection method that allows to construct efficiently NDDs from quantified formulas, and thus makes it possible to apply our counting technique to sets specified by formulas. Our algorithms have been implemented in the verification tool LASH, and applied successfully to various counting problems. [less ▲]

Detailed reference viewed: 6 (1 ULg)
Full Text
See detailOn the construction of automata from linear arithmetic constraints
Wolper, Pierre ULg; Boigelot, Bernard ULg

in Lecture Notes in Computer Science (2000, March), 1785

This paper presents an overview of algorithms for constructing automata from linear arithmetic constraints. It identifies one case in which the special structure of the automata that are constructed ... [more ▼]

This paper presents an overview of algorithms for constructing automata from linear arithmetic constraints. It identifies one case in which the special structure of the automata that are constructed allows a linear-time determinization procedure to be used. Furthermore, it shows through theoretical analysis and experiments that the special structure of the constructed automata does, in quite a general way, render the usual upper bounds on automata operations vastly overpessimistic. [less ▲]

Detailed reference viewed: 31 (6 ULg)
Full Text
Peer Reviewed
See detailSymbolic Verification of Communication Protocols with Infinite State Spaces using QDDs
Boigelot, Bernard ULg; Godefroid, Patrice

in Formal Methods in System Design (1999), 14(3), 237-255

We study the verification of properties of communication protocols modeled by a finite set of finite-state machines that communicate by exchanging messages via unbounded FIFO queues. It is well-known that ... [more ▼]

We study the verification of properties of communication protocols modeled by a finite set of finite-state machines that communicate by exchanging messages via unbounded FIFO queues. It is well-known that most interesting verification problems, such as deadlock detection, are undecidable for this class of systems. However, in practice, these verification problems may very well turn out to be decidable for a subclass containing most "real" protocols. Motivated by this optimistic (and, we claim, realistic) observation, we present an algorithm that may construct a finite and exact representation of the state space of a communication protocol, even if this state space is infinite. Our algorithm performs a loop-first search in the state space of the protocol being analyzed. A loop-first search is a search technique that attempts to explore first the results of successive executions of loops in the protocol description (code). A new data structure named Queue-content Decision Diagram (QDD) is introduced for representing (possibly infinite) sets of queue-contents. Operations for manipulating QDDs during a loop-first search are presented. A loop-first search using QDDs has been implemented, and experiments on several communication protocols with infinite state spaces have been performed. For these examples, our tool completed its search, and produced a finite symbolic representation for these infinite state spaces. [less ▲]

Detailed reference viewed: 9 (1 ULg)
Full Text
See detailSymbolic Methods for Exploring Infinite State Spaces
Boigelot, Bernard ULg

Doctoral thesis (1998)

In this thesis, we introduce a general method for computing the set of reachable states of an infinite-state system. The basic idea, inspired by well-known state-space exploration methods for finite-state ... [more ▼]

In this thesis, we introduce a general method for computing the set of reachable states of an infinite-state system. The basic idea, inspired by well-known state-space exploration methods for finite-state systems, is to propagate reachability from the initial state of the system in order to determine exactly which are the reachable states. Of course, the problem being in general undecidable, our goal is not to obtain an algorithm which is guaranteed to produce results, but one that often produces results on practically relevant cases. Our approach is based on the concept of meta-transition, which is a mathematical object that can be associated to the model, and whose purpose is to make it possible to compute in a finite amount of time an infinite set of reachable states. Different methods for creating meta-transitions are studied. We also study the properties that can be verified by state-space exploration, in particular linear-time temporal properties. The state-space exploration technique that we introduce relies on a symbolic representation system for the sets of data values manipulated during exploration. This representation system has to satisfy a number of conditions. We give a generic way of obtaining a suitable representation system, which consists of encoding each data value as a string of symbols over some finite alphabet, and to represent a set of values by a finite-state automaton accepting the language of the encodings of the values in the set. Finally, we particularize the general representation technique to two important domains: unbounded FIFO buffers, and unbounded integer variables. For each of those domains, we give detailed algorithms for performing the required operations on represented sets of values. [less ▲]

Detailed reference viewed: 33 (8 ULg)
Full Text
See detailVerifying Systems with Infinite but Regular State Spaces
Wolper, Pierre ULg; Boigelot, Bernard ULg

in Lecture Notes in Computer Science (1998), 1427

Thanks to the development of a number of efficiency enhancing techniques, state-space exploration based verification, and in particular model checking, has been quite successful for finite-state systems ... [more ▼]

Thanks to the development of a number of efficiency enhancing techniques, state-space exploration based verification, and in particular model checking, has been quite successful for finite-state systems. This has prompted efforts to apply a similar approach to systems with infinite state spaces. Doing so amounts to developing algorithms for computing a symbolic representation of the infinite state space, as opposed to requiring the user to characterize the state space by assertions. Of course, in most cases, this can only be done at the cost of forgoing any general guarantee of success. The goal of this paper is to survey a number of results in this area and to show that a surprisingly common characteristic of the systems that can be analyzed with this approach is that their state space can be represented as a regular language. [less ▲]

Detailed reference viewed: 3 (1 ULg)
Full Text
Peer Reviewed
See detailOn the Expressiveness of Real and Integer Arithmetic Automata
Boigelot, Bernard ULg; Rassart, Stéphane; Wolper, Pierre ULg

in Lecture Notes in Computer Science (1998), 1443

If read digit by digit, a n-dimensional vector of integers represented in base r can be viewed as a word over the alphabet r to the n. It has been known for some time that, under this encoding, the sets ... [more ▼]

If read digit by digit, a n-dimensional vector of integers represented in base r can be viewed as a word over the alphabet r to the n. It has been known for some time that, under this encoding, the sets of integer vectors recognizable by finite automata are exactly those definable in Presburger arithmetic if independence with respect to the base is required, and those definable in a slight extension of Presburger arithmetic if only a specific base is considered. Using the same encoding idea, but moving to infinite words, finite automata on infinite words can recognize sets of real vectors. This leads to the question of which sets of real vectors are recognizable by finite automata, which is the topic of this paper. We show that the recognizable sets of real vectors are those definable in the theory of reals and integers with addition and order, extended with a special base-dependent predicate that tests the value of a specified digit of a number. Furthermore, in the course of proving that sets of vectors defined in this theory are recognizable by finite automata, we show that linear equations and inequations have surprisingly compact representations by automata, which leads us to believe that automata accepting sets of real vectors can be of more than theoretical interest. [less ▲]

Detailed reference viewed: 21 (0 ULg)
Full Text
Peer Reviewed
See detailThe Power of QDDs
Boigelot, Bernard ULg; Godefroid, Patrice; Willems, Bernard et al

in Lecture Notes in Computer Science (1997), 1302

Queue-content Decision Diagrams (QDDs) are finite-automaton based data structures for representing (possibly infinite) sets of contents of a finite collection of unbounded FIFO queues. Their intended use ... [more ▼]

Queue-content Decision Diagrams (QDDs) are finite-automaton based data structures for representing (possibly infinite) sets of contents of a finite collection of unbounded FIFO queues. Their intended use is to serve as a symbolic representation of the possible queue contents that can occur in the state space of a protocol modeled by finite-state machines communicating through unbounded queues. This is done with the help of a loop-first search, a state-space exploration technique that attempts whenever possible to compute symbolically the effect of repeatedly executing a loop any number of times, making it possible to analyze protocols with infinite state spaces though without the guarantee of termination. This paper first solves a key problem concerning the use of QDDs in this context: it precisely characterizes when, and shows how, the operations required by a loop-first search can be applied to QDDs. Then, it addresses the problem of exploiting QDDs and loop-first searches to broaden the range of properties that can be checked from simple state reachability to temporal logic. Finally, a sufficient criterion for the termination of a loop-first search using QDDs is given. [less ▲]

Detailed reference viewed: 20 (1 ULg)
Full Text
Peer Reviewed
See detailAn Improved Reachability Analysis Method for Strongly Linear Hybrid Systems
Boigelot, Bernard ULg; Bronne, Louis; Rassart, Stéphane

in Lecture Notes in Computer Science (1997), 1254

This paper addresses the exact computation of the set of reachable states of a linear hybrid system. It proposes an approach that is an extension of classical state-space exploration. This approach uses a ... [more ▼]

This paper addresses the exact computation of the set of reachable states of a linear hybrid system. It proposes an approach that is an extension of classical state-space exploration. This approach uses a new operation, based on a cycle analysis in the control graph of the system, for generating sets of reachable states, as well as a powerful representation system for sets of values. The method broadens the range of hybrid systems for which a finite and exact representation of the set of reachable states can be computed. In particular, the state-space exploration may be performed even if the set of variable values reachable at a given control location cannot be expressed as a finite union of convex regions. The technique is illustrated on a very simple example. [less ▲]

Detailed reference viewed: 7 (0 ULg)
Full Text
Peer Reviewed
See detailAutomatic Synthesis of Specifications from the Dynamic Observation of Reactive Programs
Boigelot, Bernard ULg; Godefroid, Patrice

in Lecture Notes in Computer Science (1997), 1217

VeriSoft is a tool for systematically exploring the state spaces of systems composed of several concurrent processes executing arbitrary C (or C++) code. VeriSoft can automatically detect coordination ... [more ▼]

VeriSoft is a tool for systematically exploring the state spaces of systems composed of several concurrent processes executing arbitrary C (or C++) code. VeriSoft can automatically detect coordination problems between the concurrent processes of a system. In this paper, we present a method to synthesize a finite-state machine that simulates all the sequences of visible operations of a given process that were observed during a state-space exploration performed by VeriSoft. The examination of this machine makes it possible to discover the dynamic behavior of the process in its environment and to understand how it contributes to the global behavior of the system. [less ▲]

Detailed reference viewed: 1 (1 ULg)
Full Text
Peer Reviewed
See detailSymbolic Verification of Communication Protocols with Infinite State Spaces Using QDDs
Boigelot, Bernard ULg; Godefroid, Patrice

in Lecture Notes in Computer Science (1996), 1102

We study the verification of properties of communication protocols modeled by a finite set of finite-state machines that communicate by exchanging messages via unbounded FIFO queues. It is well-known that ... [more ▼]

We study the verification of properties of communication protocols modeled by a finite set of finite-state machines that communicate by exchanging messages via unbounded FIFO queues. It is well-known that most interesting verification problems, such as deadlock detection, are undecidable for this class of systems. However, in practice, these verification problems may very well turn out to be decidable for a subclass containing most "real" protocols. Motivated by this optimistic (and, we claim, realistic) observation, we present an algorithm that may construct a finite and exact representation of the state space of a communication protocol, even if this state space is infinite. Our algorithm performs a loop-first search in the state space of the protocol being analyzed. A loop-first search is a search technique that attempts to explore first the results of successive executions of loops in the protocol description (code). A new data structure named Queue-content Decision Diagram (QDD) is introduced for representing (possibly infinite) sets of queue-contents. Operations for manipulating QDDs during a loop-first search are presented. A loop-first search using QDDs has been implemented, and experiments on several existing communication protocols with infinite state spaces have been performed. For these examples, our tool completed its search, and produced a finite symbolic representation for these infinite state spaces. [less ▲]

Detailed reference viewed: 10 (1 ULg)
Full Text
Peer Reviewed
See detailModel Checking in Practice: An Analysis of the ACCESS.bus Protocol using SPIN
Boigelot, Bernard ULg; Godefroid, Patrice

in Lecture Notes in Computer Science (1996), 1051

This paper presents a case study of the use of model checking for analyzing an industrial protocol, the ACCESS.bus protocol. Our analysis of this protocol was carried out using SPIN, an automated ... [more ▼]

This paper presents a case study of the use of model checking for analyzing an industrial protocol, the ACCESS.bus protocol. Our analysis of this protocol was carried out using SPIN, an automated verification system which includes an implementation of model-checking algorithms. A model of the protocol was developed, and properties expressed by linear-time temporal-logic formulas were checked on this model. This analysis revealed subtle flaws in the design of the protocol. Developers who worked on implementations of ACCESS.bus were unaware of these flaws at a very late stage of their development process. We also present suggestions for solving the detected problems. [less ▲]

Detailed reference viewed: 5 (1 ULg)
Full Text
See detailAn Automata-Theoretic Approach to Presburger Arithmetic Constraints
Wolper, Pierre ULg; Boigelot, Bernard ULg

in Lecture Notes in Computer Science (1995), 983

This paper introduces a finite-automata based representation of Presburger arithmetic definable sets of integer vectors. The representation consists of concurrent automata operating on the binary ... [more ▼]

This paper introduces a finite-automata based representation of Presburger arithmetic definable sets of integer vectors. The representation consists of concurrent automata operating on the binary encodings of the elements of the represented sets. This representation has several advantages. First, being automata-based it is operational in nature and hence leads directly to algorithms, for instance all usual operations on sets of integer vectors translate naturally to operations on automata. Second, the use of concurrent automata makes it compact. Third, it is insensitive to the representation size of integers. Our representation can be used whenever arithmetic constraints are needed. To illustrate its possibilities we show that it can handle integer programming optimally, and that it leads to a new original algorithm for the satisfiability of arithmetic inequalities. [less ▲]

Detailed reference viewed: 12 (3 ULg)
Full Text
Peer Reviewed
See detailSymbolic Verification with Periodic Sets
Boigelot, Bernard ULg; Wolper, Pierre ULg

in Lecture Notes in Computer Science (1994), 818

Symbolic approaches attack the state explosion problem by introducing implicit representations that allow the simultaneous manipulation of large sets of states. The most commonly used representation in ... [more ▼]

Symbolic approaches attack the state explosion problem by introducing implicit representations that allow the simultaneous manipulation of large sets of states. The most commonly used representation in this context is the Binary Decision Diagram (BDD). This paper takes the point of view that other structures than BDD's can be useful for representing sets of values, and that combining implicit and explicit representations can be fruitful. It introduces a representation of complex periodic sets of integer values, shows how this representation can be manipulated, and describes its application to the state-space exploration of protocols. Preliminary experimental results indicate that the method can dramatically reduce the resources required for state-space exploration. [less ▲]

Detailed reference viewed: 18 (6 ULg)