-
First-Order Quantification over Automata
Authors:
Bernard Boigelot,
Pascal Fontaine,
Baptiste Vergain
Abstract:
Deciding formulas mixing arithmetic and uninterpreted predicates is of practical interest, notably for applications in verification. Some decision procedures consist in building by structural induction an automaton that recognizes the set of models of the formula under analysis, and then testing whether this automaton accepts a non-empty language. A drawback is that universal quantification is usu…
▽ More
Deciding formulas mixing arithmetic and uninterpreted predicates is of practical interest, notably for applications in verification. Some decision procedures consist in building by structural induction an automaton that recognizes the set of models of the formula under analysis, and then testing whether this automaton accepts a non-empty language. A drawback is that universal quantification is usually handled by a reduction to existential quantification and complementation. For logical formalisms in which models are encoded as infinite words, this hinders the practical use of this method due to the difficulty of complementing infinite-word automata. The contribution of this paper is to introduce an algorithm for directly computing the effect of universal first-order quantifiers on automata recognizing sets of models, for formulas involving natural numbers encoded in unary notation. This makes it possible to apply the automata-based approach to obtain implementable decision procedures for various arithmetic theories.
△ Less
Submitted 7 June, 2023;
originally announced June 2023.
-
Decidability of Difference Logic over the Reals with Uninterpreted Unary Predicates
Authors:
Bernard Boigelot,
Pascal Fontaine,
Baptiste Vergain
Abstract:
First-order logic fragments mixing quantifiers, arithmetic, and uninterpreted predicates are often undecidable, as is, for instance, Presburger arithmetic extended with a single uninterpreted unary predicate. In the SMT world, difference logic is a quite popular fragment of linear arithmetic which is less expressive than Presburger arithmetic. Difference logic on integers with uninterpreted unary…
▽ More
First-order logic fragments mixing quantifiers, arithmetic, and uninterpreted predicates are often undecidable, as is, for instance, Presburger arithmetic extended with a single uninterpreted unary predicate. In the SMT world, difference logic is a quite popular fragment of linear arithmetic which is less expressive than Presburger arithmetic. Difference logic on integers with uninterpreted unary predicates is known to be decidable, even in the presence of quantifiers. We here show that (quantified) difference logic on real numbers with a single uninterpreted unary predicate is undecidable, quite surprisingly. Moreover, we prove that difference logic on integers, together with order on reals, combined with uninterpreted unary predicates, remains decidable.
△ Less
Submitted 24 May, 2023;
originally announced May 2023.
-
An efficient algorithm to decide periodicity of b-recognisable sets using MSDF convention
Authors:
Bernard Boigelot,
Isabelle Mainz,
Victor Marsault,
Michel Rigo
Abstract:
Given an integer base $b>1$, a set of integers is represented in base $b$ by a language over $\{0,1,...,b-1\}$. The set is said to be $b$-recognisable if its representation is a regular language. It is known that eventually periodic sets are $b$-recognisable in every base $b$, and Cobham's theorem implies the converse: no other set is $b$-recognisable in every base $b$.
We are interested in deci…
▽ More
Given an integer base $b>1$, a set of integers is represented in base $b$ by a language over $\{0,1,...,b-1\}$. The set is said to be $b$-recognisable if its representation is a regular language. It is known that eventually periodic sets are $b$-recognisable in every base $b$, and Cobham's theorem implies the converse: no other set is $b$-recognisable in every base $b$.
We are interested in deciding whether a $b$-recognisable set of integers (given as a finite automaton) is eventually periodic. Honkala showed that this problem decidable in 1986 and recent developments give efficient decision algorithms. However, they only work when the integers are written with the least significant digit first.
In this work, we consider the natural order of digits (Most Significant Digit First) and give a quasi-linear algorithm to solve the problem in this case.
△ Less
Submitted 13 February, 2017;
originally announced February 2017.
-
From Constrained Delaunay Triangulations to Roadmap Graphs with Arbitrary Clearance
Authors:
Stéphane Lens,
Bernard Boigelot
Abstract:
This work studies path planning in two-dimensional space, in the presence of polygonal obstacles. We specifically address the problem of building a roadmap graph, that is, an abstract representation of all the paths that can potentially be followed around a given set of obstacles. Our solution consists in an original refinement algorithm for constrained Delaunay triangulations, aimed at generating…
▽ More
This work studies path planning in two-dimensional space, in the presence of polygonal obstacles. We specifically address the problem of building a roadmap graph, that is, an abstract representation of all the paths that can potentially be followed around a given set of obstacles. Our solution consists in an original refinement algorithm for constrained Delaunay triangulations, aimed at generating a roadmap graph suited for planning paths with arbitrary clearance. In other words, a minimum distance to the obstacles can be specified, and the graph does not have to be recomputed if this distance is modified. Compared to other solutions, our approach has the advantage of being simpler, as well as significantly more efficient.
△ Less
Submitted 7 June, 2016;
originally announced June 2016.
-
Efficient Path Interpolation and Speed Profile Computation for Nonholonomic Mobile Robots
Authors:
Stéphane Lens,
Bernard Boigelot
Abstract:
This paper studies path synthesis for nonholonomic mobile robots moving in two-dimensional space. We first address the problem of interpolating paths expressed as sequences of straight line segments, such as those produced by some planning algorithms, into smooth curves that can be followed without stop**. Our solution has the advantage of being simpler than other existing approaches, and has a…
▽ More
This paper studies path synthesis for nonholonomic mobile robots moving in two-dimensional space. We first address the problem of interpolating paths expressed as sequences of straight line segments, such as those produced by some planning algorithms, into smooth curves that can be followed without stop**. Our solution has the advantage of being simpler than other existing approaches, and has a low computational cost that allows a real-time implementation. It produces discretized paths on which curvature and variation of curvature are bounded at all points, and preserves obstacle clearance. Then, we consider the problem of computing a time-optimal speed profile for such paths. We introduce an algorithm that solves this problem in linear time, and that is able to take into account a broader class of physical constraints than other solutions. Our contributions have been implemented and evaluated in the framework of the Eurobot contest.
△ Less
Submitted 11 August, 2015;
originally announced August 2015.
-
Min Max Generalization for Two-stage Deterministic Batch Mode Reinforcement Learning: Relaxation Schemes
Authors:
Raphael Fonteneau,
Damien Ernst,
Bernard Boigelot,
Quentin Louveaux
Abstract:
We study the minmax optimization problem introduced in [22] for computing policies for batch mode reinforcement learning in a deterministic setting. First, we show that this problem is NP-hard. In the two-stage case, we provide two relaxation schemes. The first relaxation scheme works by drop** some constraints in order to obtain a problem that is solvable in polynomial time. The second relaxati…
▽ More
We study the minmax optimization problem introduced in [22] for computing policies for batch mode reinforcement learning in a deterministic setting. First, we show that this problem is NP-hard. In the two-stage case, we provide two relaxation schemes. The first relaxation scheme works by drop** some constraints in order to obtain a problem that is solvable in polynomial time. The second relaxation scheme, based on a Lagrangian relaxation where all constraints are dualized, leads to a conic quadratic programming problem. We also theoretically prove and empirically illustrate that both relaxation schemes provide better results than those given in [22].
△ Less
Submitted 30 October, 2012; v1 submitted 23 February, 2012;
originally announced February 2012.
-
Implicit Real Vector Automata
Authors:
Bernard Boigelot,
Julien Brusten,
Jean-François Degbomont
Abstract:
This paper addresses the symbolic representation of non-convex real polyhedra, i.e., sets of real vectors satisfying arbitrary Boolean combinations of linear constraints. We develop an original data structure for representing such sets, based on an implicit and concise encoding of a known structure, the Real Vector Automaton. The resulting formalism provides a canonical representation of polyhedr…
▽ More
This paper addresses the symbolic representation of non-convex real polyhedra, i.e., sets of real vectors satisfying arbitrary Boolean combinations of linear constraints. We develop an original data structure for representing such sets, based on an implicit and concise encoding of a known structure, the Real Vector Automaton. The resulting formalism provides a canonical representation of polyhedra, is closed under Boolean operators, and admits an efficient decision procedure for testing the membership of a vector.
△ Less
Submitted 31 October, 2010;
originally announced November 2010.
-
On the Sets of Real Numbers Recognized by Finite Automata in Multiple Bases
Authors:
Bernard Boigelot,
Julien Brusten,
Veronique Bruyere
Abstract:
This article 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…
▽ More
This article 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. This result extends Cobham's theorem, which characterizes the sets of integer numbers that are recognizable by finite automata in multiple bases.
In this article, 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 the first order additive theory of real and integer numbers. 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
Submitted 24 February, 2010; v1 submitted 14 January, 2010;
originally announced January 2010.
-
An Effective Decision Procedure for Linear Arithmetic with Integer and Real Variables
Authors:
Bernard Boigelot,
Sebastien Jodogne,
Pierre Wolper
Abstract:
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 infinite 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…
▽ 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 infinite 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 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
Submitted 20 March, 2003;
originally announced March 2003.
