Boigelot, B., & Mainz, I. (2018). Efficient Symbolic Representation of Convex Polyhedra in High-Dimensional Spaces.

*Lecture Notes in Computer Science*.Peer reviewed

This work is aimed at developing an efficient data structure for representing symbolically convex polyhedra. We introduce an original data structure, the Decomposed Convex Polyhedron (DCP), that is closed ...

Boigelot, B., Mainz, I., Marsault, V., & Rigo, M. (2017). An efficient algorithm to decide periodicity of b-recognisable sets using MSDF convention.

*Leibniz International Proceedings in Informatics, 80*.Peer reviewed

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 ...

Lens, S. (2015).

*Efficient and Precise Trajectory Planning for Nonholonomic Mobile Robots*. Unpublished doctoral thesis, Université de Liège, Liège, Belgique.Trajectory planning is one of the fundamental problems in mobile robotics. A wide variety of approaches have been proposed over the years to deal with the various issues of this problem. This thesis presents ...

Krishna Moorthy Parvathi, S. M., Boigelot, B., & Mercatoris, B. (2015, July 15).

*Effective segmentation of green vegetation for resource-constrained real-time applications*. Paper presented at 10th European Conference on Precision Agriculture, Beit-Dagan, Israel.This paper describes an improved algorithm for segmentation of green vegetation under uncontrolled illumination conditions and also suitable for resource-constrained real-time applications. The proposed ...

Lens, S., & Boigelot, B. (2015).

*From Constrained Delaunay Triangulations to Roadmap Graphs with Arbitrary Clearance*. Eprint/Working paper retrieved from http://arxiv.org/abs/1606.02055.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 ...

Lens, S., & Boigelot, B. (2015).

*Efficient Path Interpolation and Speed Profile Computation for Nonholonomic Mobile Robots*. Eprint/Working paper retrieved from http://arxiv.org/abs/1508.02608.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 ...

Lens, S., & Boigelot, B. (2014).

*Efficient Path Planning for Nonholonomic Mobile Robots*. Liège, Belgium: Montefiore Institute.This work addresses path planning for nonholonomic robots moving in two-dimensional space. The problem consists in computing a sequence of line segments that leads from the current configuration of the robot ...

Krishna Moorthy Parvathi, S. M., Detry, R., Boigelot, B., & Mercatoris, B. (2014, March 05).

*A vision-based autonomous inter-row weeder*. Paper presented at ENVITAM PhD Student Day, Université catholique de Louvain, Louvain-la-Neuve, Belgium.Autonomous robotic weed destruction plays a significant role in crop production as it automates one of the few unmechanized and drudging tasks of agriculture i.e. manual weed destruction. Robotic technology ...

Krishna Moorthy Parvathi, S. M., Mercatoris, B., & Boigelot, B. (2014, February 07).

*Robot weed killers - no pain more gain*. Poster session presented at 19th National Symposium on Applied Biological Sciences, Gembloux Agro-Bio Tech (Liège University), Faculty of Bioscience Engineering, Belgium.Weed destruction plays a significant role in crop production, and its automation has both economic and environmental benefits by minimizing the usage of chemicals in the fields. Our aim is to design a small ...

Boigelot, B., Herbreteau, F., & Mainz, I. (2014). Acceleration of Affine Hybrid Transformations.

*Lecture Notes in Computer Science, 8837*, 31-46.Peer reviewed

This work addresses the computation of the set of reachable configurations of linear hybrid automata. The approach relies on symbolic state-space exploration, using acceleration in order to speed up the ...

Fonteneau, R., Ernst, D., Boigelot, B., & Louveaux, Q. (2014). Lipschitz robust control from off-policy trajectories.

*Proceedings of the 53rd IEEE Conference on Decision and Control (IEEE CDC 2014)*.Peer reviewed

We study the minmax optimization problem introduced in [Fonteneau et al. (2011), ``Towards min max reinforcement learning'', Springer CCIS, vol. 129, pp. 61-77] for computing control policies for batch mode ...

Degbomont, J.-F. (2013).

*Implicit Real Vector Automata*. Unpublished doctoral thesis, Université de Liège, Liège, Belgique.This thesis introduces a new data structure, the Implicit Real Vector Automaton (IRVA), suited for representing symbolically polyhedra, i.e., regions of n-dimensional space defined by finite Boolean ...

Fonteneau, R., Ernst, D., Boigelot, B., & Louveaux, Q. (2013). Généralisation Min Max pour l'Apprentissage par Renforcement Batch et Déterministe : Relaxations pour le Cas Général T Etapes.

*8èmes Journées Francophones de Planification, Décision et Apprentissage pour la conduite de systèmes (JFPDA'13)*.Peer reviewed

Cet article aborde le problème de généralisation minmax dans le cadre de l'apprentissage par renforcement batch et déterministe. Le problème a été originellement introduit par [Fonteneau, 2011], et il a déjà ...

Fonteneau, R., Ernst, D., Boigelot, B., & Louveaux, Q. (2013). Min max generalization for deterministic batch mode reinforcement learning: relaxation schemes.

*SIAM Journal on Control and Optimization, 51*(5), 3355–3385.Peer reviewed (verified by ORBi)

We study the min max optimization problem introduced in Fonteneau et al. [Towards min max reinforcement learning, ICAART 2010, Springer, Heidelberg, 2011, pp. 61–77] for computing policies for batch mode ...

Fonteneau, R., Ernst, D., Boigelot, B., & Louveaux, Q. (2012). Généralisation min max pour l'apprentissage par renforcement batch et déterministe : schémas de relaxation.

*Septièmes Journées Francophones de Planification, Décision et Apprentissage pour la conduite de systèmes (JFPDA 2012)*.Peer reviewed

On s’intéresse au problème de généralisation min max dans le cadre de l’apprentissage par renforcement batch et déterministe. Le problème a été originellement introduit par Fonteneau et al. (2011). Dans un ...

Boigelot, B. (2012). Domain-specific regular acceleration.

*International Journal on Software Tools for Technology Transfer, 14*(2), 193-206.Peer reviewed (verified by ORBi)

The regular model-checking approach is a set of techniques aimed at exploring symbolically infinite state spaces. These techniques proceed by representing sets of configurations of the system under analysis by ...

Fonteneau, R., Ernst, D., Boigelot, B., & Louveaux, Q. (2011). Relaxation schemes for min max generalization in deterministic batch mode reinforcement learning.

*4th International NIPS Workshop on Optimization for Machine Learning (OPT 2011)*.Peer reviewed

We study the min max optimization problem introduced in [Fonteneau, 2011] for computing policies for batch mode reinforcement learning in a deterministic setting. This problem is NP-hard. We focus on the two ...

Dethier, G. (2011).

*Design and Implementation of a Distributed Lattice Boltzmann-based Fluid Flow Simulation Tool*. Unpublished doctoral thesis, Université de Liège, Liège, Belgique.Lattice Boltzmann-based (LB) simulations are well suited to the simulation of fluid flows in complex structures encountered in chemical engineering like porous media or structured packing used in distillation ...

Boigelot, B., Brusten, J., & Bruyère, V. (2010). On the Sets of Real Numbers Recognized by Finite Automata in Multiple Bases.

*Logical Methods in Computer Science, 6*(1), 1-17.Peer reviewed

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 ...

Boigelot, B., Brusten, J., & Degbomont, J.-F. (2010). Implicit Real Vector Automata.

*Electronic Proceedings in Theoretical Computer Science, 39*, 63-76.Peer reviewed (verified by ORBi)

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 ...

Boigelot, B., Brusten, J., & Bruyère, V. (2008). On the Sets of Real Numbers Recognized by Finite Automata in Multiple Bases.

*Lecture Notes in Computer Science, 5126*, 112-123.Peer reviewed

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 ...

Lens, S. (2008).

*Locomotion d'un robot mobile*. Unpublished master thesis, Université de Liège, Liège, Belgique.Dans le domaine de la robotique mobile, l’étude de la locomotion possède
une place prépondérante. De nombreuses approches et solutions peuvent être
envisagées et il convient d’apporter un soin particulier ...

Boigelot, B., & Brusten, J. (2007). A Generalization of Cobham's Theorem to Automata over Real Numbers.

*Lecture Notes in Computer Science, 4596*, 813-824.Peer reviewed

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 ...

Boigelot, B. (2006). Number-Set Representations for Infinite-State Verification.

*Proceedings of VISSAS 2005*(pp. 1-16). IOS Press.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 ...

Boigelot, B., & Herbreteau, F. (2006). The power of hybrid acceleration.

*Lecture Notes in Computer Science, 4144*, 438-451.Peer reviewed

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 ...

Van Lishout, F. (2006).

*Single-player games: introduction to a new solving method*. Unpublished DEA/DES thesis, University of Liège, Liège, Belgium.In many games, the machine has become stronger than the best human players. Machines have already beaten the human World Champion in famous games like Checkers, Chess, Scrabble and Othello. However, mankind ...

Boigelot, B., Jodogne, S., & Wolper, P. (2005). An effective decision procedure for linear arithmetic over the integers and reals.

*ACM Transactions on Computational Logic, 6*(3), 614--633.Peer reviewed (verified by ORBi)

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 ...

Boigelot, B., & Latour, L. (2004). Counting the solutions of Presburger equations without enumerating them.

*Theoretical Computer Science, 313*(1), 17-29.Peer reviewed (verified by ORBi)

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 ...

Boigelot, B., Legay, A., & Wolper, P. (2004). Omega-regular model checking.

*Lecture Notes in Computer Science, 2988*, 561-575.Peer reviewed

"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 ...

Boigelot, B., Herbreteau, F., & Jodogne, S. (2003). Hybrid Acceleration using Real Vector Automata.

*Lecture Notes in Computer Science, 2725*, 193-205.Peer reviewed

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 ...

Boigelot, B. (2003). On Iterating Linear Transformations over Recognizable Sets of Integers.

*Theoretical Computer Science, 309*(1-3), 413-468.Peer reviewed (verified by ORBi)

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 ...

Boigelot, B., Legay, A., & Wolper, P. (2003). Iterating transducers in the large.

*Lecture Notes in Computer Science, 2725*, 223-235.Peer reviewed

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 ...

Boigelot, B., & Wolper, P. (2002). Representing arithmetic constraints with finite automata: An overview.

*Lecture Notes in Computer Science, 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 ...

Boigelot, B., Jodogne, S., & Wolper, P. (2001). On the Use of Weak Automata for Deciding Linear Arithmetic with Integer and Real Variables.

*Lecture Notes in Computer Science, 2083*, 611--625.Peer reviewed

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 ...

Boigelot, B., & Latour, L. (2001). Counting the Solutions of Presburger Equations without Enumerating Them.

*Lecture Notes in Computer Science, 2494*, 40-51.Peer reviewed

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 ...

Wolper, P., & Boigelot, B. (2000). On the construction of automata from linear arithmetic constraints.

*Lecture Notes in Computer Science, 1785*, 1-19.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 ...

Boigelot, B., & Godefroid, P. (1999). Symbolic Verification of Communication Protocols with Infinite State Spaces using QDDs.

*Formal Methods in System Design, 14*(3), 237-255.Peer reviewed (verified by ORBi)

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 ...

Boigelot, B. (1998).

*Symbolic Methods for Exploring Infinite State Spaces*. Unpublished doctoral thesis, Université de Liège, Liège, Belgium.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 ...

Boigelot, B., Rassart, S., & Wolper, P. (1998). On the Expressiveness of Real and Integer Arithmetic Automata.

*Lecture Notes in Computer Science, 1443*, 152-163.Peer reviewed

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 ...

Wolper, P., & Boigelot, B. (1998). Verifying Systems with Infinite but Regular State Spaces.

*Lecture Notes in Computer Science, 1427*, 88-97.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 ...

Boigelot, B., Bronne, L., & Rassart, S. (1997). An Improved Reachability Analysis Method for Strongly Linear Hybrid Systems.

*Lecture Notes in Computer Science, 1254*, 167-178.Peer reviewed

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 ...

Boigelot, B., & Godefroid, P. (1997). Automatic Synthesis of Specifications from the Dynamic Observation of Reactive Programs.

*Lecture Notes in Computer Science, 1217*, 321-333.Peer reviewed

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 ...

Boigelot, B., Godefroid, P., Willems, B., & Wolper, P. (1997). The Power of QDDs.

*Lecture Notes in Computer Science, 1302*, 172-186.Peer reviewed

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 ... ...

Boigelot, B., & Godefroid, P. (1996). Model Checking in Practice: An Analysis of the ACCESS.bus Protocol using SPIN.

*Lecture Notes in Computer Science, 1051*, 465-478.Peer reviewed

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 ...

Boigelot, B., & Godefroid, P. (1996). Symbolic Verification of Communication Protocols with Infinite State Spaces Using QDDs.

*Lecture Notes in Computer Science, 1102*, 1-12.Peer reviewed

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 ...

Wolper, P., & Boigelot, B. (1995). An Automata-Theoretic Approach to Presburger Arithmetic Constraints.

*Lecture Notes in Computer Science, 983*, 21-32.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 ...

Boigelot, B., & Wolper, P. (1994). Symbolic Verification with Periodic Sets.

*Lecture Notes in Computer Science, 818*, 55-67.Peer reviewed

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 ... ...