Browse ORBi by ORBi project

- Background
- Content
- Benefits and challenges
- Legal aspects
- Functions and services
- Team
- Help and tutorials

On the Sets of Real Numbers Recognized by Finite Automata in Multiple Bases Boigelot, Bernard ; Brusten, Julien ; in Lecture Notes in Computer Science (2008, July), 5126 This paper studies the expressive power of finite automata recognizing sets of real numbers encoded in positional notation. We consider Muller automata as well as the restricted class of weak ... [more ▼] This paper studies the expressive power of finite automata recognizing sets of real numbers encoded in positional notation. We consider Muller automata as well as the restricted class of weak deterministic automata, used as symbolic set representations in actual applications. In previous work, it has been established that the sets of numbers that are recognizable by weak deterministic automata in two bases that do not share the same set of prime factors are exactly those that are definable in the first order additive theory of real and integer numbers (R, Z, +, <). This result extends Cobham's theorem, which characterizes the sets of integer numbers that are recognizable by finite automata in multiple bases. In this paper, we first generalize this result to multiplicatively independent bases, which brings it closer to the original statement of Cobham's theorem. Then, we study the sets of reals recognizable by Muller automata in two bases. We show with a counterexample that, in this setting, Cobham's theorem does not generalize to multiplicatively independent bases. Finally, we prove that the sets of reals that are recognizable by Muller automata in two bases that do not share the same set of prime factors are exactly those definable in (R, Z, +, <). These sets are thus also recognizable by weak deterministic automata. This result leads to a precise characterization of the sets of real numbers that are recognizable in multiple bases, and provides a theoretical justification to the use of weak automata as symbolic representations of sets. [less ▲] Detailed reference viewed: 102 (33 ULg)A Generalization of Cobham's Theorem to Automata over Real Numbers Boigelot, Bernard ; Brusten, Julien in Lecture Notes in Computer Science (2007, July), 4596 This paper studies the expressive power of finite-state automata recognizing sets of real numbers encoded positionally. It is known that the sets that are definable in the first-order additive theory of ... [more ▼] This paper studies the expressive power of finite-state automata recognizing sets of real numbers encoded positionally. It is known that the sets that are definable in the first-order additive theory of real and integer variables (R, Z, +, <) can all be recognized by weak deterministic Büchi automata, regardless of the encoding base r > 1. In this paper, we prove the reciprocal property, i.e., that a subset of R that is recognizable by weak deterministic automata in every base r > 1 is necessarily definable in (R, Z, +, <). This result generalizes to real numbers the well-known Cobham's theorem on the finite-state recognizability of sets of integers. Our proof gives interesting insight into the internal structure of automata recognizing sets of real numbers, which may lead to efficient data structures for handling these sets. [less ▲] Detailed reference viewed: 140 (33 ULg)The power of hybrid acceleration Boigelot, Bernard ; in Lecture Notes in Computer Science (2006), 4144 This paper addresses the problem of computing symbolically the set of reachable configurations of a linear hybrid automaton. A solution proposed in earlier work consists in exploring the reachable ... [more ▼] This paper addresses the problem of computing symbolically the set of reachable configurations of a linear hybrid automaton. A solution proposed in earlier work consists in exploring the reachable configurations using an acceleration operator for computing the iterated effect of selected control cycles. Unfortunately, this method imposes a periodicity requirement on the data transformations labeling these cycles, that is not always satisfied in practice. This happens in particular with the important subclass of timed automata, even though it is known that the paths of such automata have a periodic behavior. The goal of this paper is to broaden substantially the applicability of hybrid acceleration. This is done by introducing powerful reduction rules, aimed at translating hybrid data transformations into equivalent ones that satisfy the periodicity criterion. In particular, we show that these rules always succeed in the case of timed automata. This makes it possible to compute an exact symbolic representation of the set of reachable configurations of a linear hybrid automaton, with a guarantee of termination over the subclass of timed automata. Compared to other known solutions to this problem, our method is simpler, and applicable to a much larger class of systems. [less ▲] Detailed reference viewed: 40 (8 ULg)Number-Set Representations for Infinite-State Verification Boigelot, Bernard in Proceedings of VISSAS 2005 (2006) In order to compute the reachability set of infinite-state models, one needs a technique for exploring infinite sequences of transitions in finite time, as well as a symbolic representation for the finite ... [more ▼] In order to compute the reachability set of infinite-state models, one needs a technique for exploring infinite sequences of transitions in finite time, as well as a symbolic representation for the finite and infinite sets of configurations that are to be handled. The representation problem can be solved by automata-based methods, which consist in representing a set by a finite-state machine recognizing its elements, suitably encoded as words over a finite alphabet. Automata-based set representations have many advantages: They are expressive, easy to manipulate, and admit a canonical form. In this survey, we describe two automata-based structures that have been developed for representing sets of numbers (or, more generally, of vectors): The Number Decision Diagram (NDD) for integer values, and the Real Vector Automaton (RVA) for real numbers. We discuss the expressiveness of these structures, present some construction algorithms, and give a brief introduction to some related acceleration techniques. [less ▲] Detailed reference viewed: 12 (2 ULg)An effective decision procedure for linear arithmetic over the integers and reals Boigelot, Bernard ; Jodogne, Sébastien ; Wolper, Pierre in ACM transactions on Computational Logic (2005), 6(3), 614--633 This article 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 article 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 infinite words, but this involves some difficult and delicate to implement algorithms. The contribution of this article is to show, using topological arguments, that only a restricted class of automata on infinite words are necessary for handling real and integer linear arithmetic. This allows the use of substantially simpler algorithms, which have been successfully implemented. [less ▲] Detailed reference viewed: 54 (15 ULg)Omega-regular model checking Boigelot, Bernard ; ; Wolper, Pierre in Lecture Notes in Computer Science (2004), 2988 "Regular model checking" is the name of a family of techniques for analyzing infinite-state systems in which states are represented by words or trees, sets of states by finite automata on these objects ... [more ▼] "Regular model checking" is the name of a family of techniques for analyzing infinite-state systems in which states are represented by words or trees, sets of states by finite automata on these objects, and transitions by finite automata operating on pairs of state encodings, i.e. finite-state transducers. In this context, the central problem is then to compute the iterative closure of a finite-state transducer. This paper addresses the use of regular model-checking like techniques for systems whose states are represented by infinite (omega) words. Its main motivation is to show the feasibility and usefulness of this approach through a combination of the necessary theoretical developments, implementation, and experimentation. The iteration technique that is used is adapted from recent work of the authors on the iteration of finite-word transducers. It proceeds by comparing successive elements of a sequence of approximations of the iteration, detecting an "increment" that is added to move from one approximation to the next, and extrapolating the sequence by allowing arbitrary repetitions of this increment. By restricting oneself to weak deterministic Buchi automata, and using a number of implementation optimizations, examples of significant size can be handled. The proposed transducer iteration technique can just as well be exploited to compute the closure of a given set of states by the transducer iteration, which has proven to be a very effective way of using the technique. Examples such as a leaking gas burner in which time is modeled by real variables have been handled completely within the automata-theoretic setting. [less ▲] Detailed reference viewed: 59 (10 ULg)Counting the solutions of Presburger equations without enumerating them Boigelot, Bernard ; 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: 17 (4 ULg)Hybrid Acceleration using Real Vector Automata Boigelot, Bernard ; ; Jodogne, Sébastien 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: 24 (4 ULg)Iterating transducers in the large Boigelot, Bernard ; ; Wolper, Pierre 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: 39 (7 ULg)On Iterating Linear Transformations over Recognizable Sets of Integers Boigelot, Bernard 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: 29 (5 ULg)Representing arithmetic constraints with finite automata: An overview Boigelot, Bernard ; Wolper, Pierre 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: 35 (7 ULg)On the Use of Weak Automata for Deciding Linear Arithmetic with Integer and Real Variables Boigelot, Bernard ; Jodogne, Sébastien ; Wolper, Pierre 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: 35 (6 ULg)Counting the Solutions of Presburger Equations without Enumerating Them Boigelot, Bernard ; 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: 10 (1 ULg)On the construction of automata from linear arithmetic constraints Wolper, Pierre ; Boigelot, Bernard 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: 37 (6 ULg)Symbolic Verification of Communication Protocols with Infinite State Spaces using QDDs Boigelot, Bernard ; 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: 20 (1 ULg)Symbolic Methods for Exploring Infinite State Spaces Boigelot, Bernard 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: 52 (12 ULg)Verifying Systems with Infinite but Regular State Spaces Wolper, Pierre ; Boigelot, Bernard 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: 9 (1 ULg)On the Expressiveness of Real and Integer Arithmetic Automata Boigelot, Bernard ; ; Wolper, Pierre 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: 30 (0 ULg)The Power of QDDs Boigelot, 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: 22 (1 ULg)An Improved Reachability Analysis Method for Strongly Linear Hybrid Systems Boigelot, Bernard ; ; 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: 9 (0 ULg) |
||