-
Guaranteed approximations of arbitrarily quantified reachability problems
Authors:
Eric Goubault,
Sylvie Putot
Abstract:
We propose an approach to compute inner and outer-approximations of the sets of values satisfying constraints expressed as arbitrarily quantified formulas. Such formulas arise for instance when specifying important problems in control such as robustness, motion planning or controllers comparison. We propose an interval-based method which allows for tractable but tight approximations. We demonstrat…
▽ More
We propose an approach to compute inner and outer-approximations of the sets of values satisfying constraints expressed as arbitrarily quantified formulas. Such formulas arise for instance when specifying important problems in control such as robustness, motion planning or controllers comparison. We propose an interval-based method which allows for tractable but tight approximations. We demonstrate its applicability through a series of examples and benchmarks using a prototype implementation.
△ Less
Submitted 14 September, 2023;
originally announced September 2023.
-
Estimating the Coverage Measure and the Area Explored by a Line-Sweep Sensor on the Plane
Authors:
Maria Costa Vianna,
Eric Goubault,
Luc Jaulin,
Sylvie Putot
Abstract:
This paper presents a method for determining the area explored by a line-sweep sensor during an area-covering mission in a two-dimensional plane. Accurate knowledge of the explored area is crucial for various applications in robotics, such as mapping, surveillance, and coverage optimization. The proposed method leverages the concept of coverage measure of the environment and its relation to the to…
▽ More
This paper presents a method for determining the area explored by a line-sweep sensor during an area-covering mission in a two-dimensional plane. Accurate knowledge of the explored area is crucial for various applications in robotics, such as mapping, surveillance, and coverage optimization. The proposed method leverages the concept of coverage measure of the environment and its relation to the topological degree in the plane, to estimate the extent of the explored region. In addition, we extend the approach to uncertain coverage measure values using interval analysis. This last contribution allows for a guaranteed characterization of the explored area, essential considering the often critical character of area-covering missions. Finally, this paper also proposes a novel algorithm for computing the topological degree in the 2-dimensional plane, for all the points inside an area of interest, which differs from existing solutions that compute the topological degree for single points. The applicability of the method is evaluated through a real-world experiment.
△ Less
Submitted 7 September, 2023;
originally announced September 2023.
-
Tractable higher-order under-approximating AE extensions for non-linear systems
Authors:
Eric Goubault,
Sylvie Putot
Abstract:
We consider the problem of under and over-approximating the image of general vector-valued functions over bounded sets, and apply the proposed solution to the estimation of reachable sets of uncertain non-linear discrete-time dynamical systems. Such a combination of under and over-approximations is very valuable for the verification of properties of embedded and cyber-physical controlled systems.…
▽ More
We consider the problem of under and over-approximating the image of general vector-valued functions over bounded sets, and apply the proposed solution to the estimation of reachable sets of uncertain non-linear discrete-time dynamical systems. Such a combination of under and over-approximations is very valuable for the verification of properties of embedded and cyber-physical controlled systems. Over-approximations prove properties correct, while under-approximations can be used for falsification. Coupled, they provide a measure of the conservatism of the analysis. This work introduces a general framework relying on computations of robust ranges of vector-valued functions. This framework allows us to extend for under-approximation many precision refinements that are classically used for over-approximations, such as affine approximations, Taylor models, quadrature formulae and preconditioning methods. We end by evaluating the efficiency and precision of our approach, focusing on the application to the analysis of discrete-time dynamical systems with inputs and disturbances, on different examples from the literature.
△ Less
Submitted 27 January, 2021;
originally announced January 2021.
-
On-The-Fly Control of Unknown Systems: From Side Information to Performance Guarantees through Reachability
Authors:
Franck Djeumou,
Abraham P. Vinod,
Eric Goubault,
Sylvie Putot,
Ufuk Topcu
Abstract:
We develop data-driven algorithms for reachability analysis and control of systems with a priori unknown nonlinear dynamics. The resulting algorithms not only are suitable for settings with real-time requirements but also provide provable performance guarantees. To this end, they merge noisy data from only a single finite-horizon trajectory and, if available, various forms of side information. Suc…
▽ More
We develop data-driven algorithms for reachability analysis and control of systems with a priori unknown nonlinear dynamics. The resulting algorithms not only are suitable for settings with real-time requirements but also provide provable performance guarantees. To this end, they merge noisy data from only a single finite-horizon trajectory and, if available, various forms of side information. Such side information may include knowledge of the regularity of the dynamics, algebraic constraints on the states, monotonicity, or decoupling in the dynamics between the states. Specifically, we develop two algorithms, $\texttt{DaTaReach}$ and $\texttt{DaTaControl}$, to over-approximate the reachable set and design control signals for the system on the fly. $\texttt{DaTaReach}$ constructs a differential inclusion that contains the unknown dynamics. Then, in a discrete-time setting, it over-approximates the reachable set through interval Taylor-based methods applied to systems with dynamics described as differential inclusions. We provide a bound on the time step size that ensures the correctness and termination of $\texttt{DaTaReach}$. $\texttt{DaTaControl}$ enables convex-optimization-based control using the computed over-approximation and the receding-horizon control framework. Besides, $\texttt{DaTaControl}$ achieves near-optimal control and is suitable for real-time control of such systems. We establish a bound on its suboptimality and the number of primitive operations it requires to compute control values. Then, we theoretically show that $\texttt{DaTaControl}$ achieves tighter suboptimality bounds with an increasing amount of data and richer side information. Finally, experiments on a unicycle, quadrotor, and aircraft systems demonstrate the efficacy of both algorithms over existing approaches.
△ Less
Submitted 16 December, 2021; v1 submitted 10 November, 2020;
originally announced November 2020.
-
On-The-Fly Control of Unknown Smooth Systems from Limited Data
Authors:
Franck Djeumou,
Abraham P. Vinod,
Eric Goubault,
Sylvie Putot,
Ufuk Topcu
Abstract:
We investigate the problem of data-driven, on-the-fly control of systems with unknown nonlinear dynamics where data from only a single finite-horizon trajectory and possibly side information on the dynamics are available. Such side information may include knowledge of the regularity of the dynamics, monotonicity of the states, or decoupling in the dynamics between the states. Specifically, we deve…
▽ More
We investigate the problem of data-driven, on-the-fly control of systems with unknown nonlinear dynamics where data from only a single finite-horizon trajectory and possibly side information on the dynamics are available. Such side information may include knowledge of the regularity of the dynamics, monotonicity of the states, or decoupling in the dynamics between the states. Specifically, we develop two algorithms, $\texttt{DaTaReach}$ and $\texttt{DaTaControl}$, to over-approximate the reachable set and design control signals for the system on the fly. $\texttt{DaTaReach}$ constructs a differential inclusion that contains the unknown vector field. Then, it computes an over-approximation of the reachable set based on interval Taylor-based methods applied to systems with dynamics described as differential inclusions. $\texttt{DaTaControl}$ enables convex-optimization-based, near-optimal control using the computed over-approximation and the receding-horizon control framework. We provide a bound on its suboptimality and show that more data and side information enable $\texttt{DaTaControl}$ to achieve tighter suboptimality bounds. Finally, we demonstrate the efficacy of $\texttt{DaTaControl}$ over existing approaches on the problems of controlling a unicycle and quadrotor systems.
△ Less
Submitted 22 March, 2021; v1 submitted 26 September, 2020;
originally announced September 2020.
-
Formal Verification of Station Keeping Maneuvers for a Planar Autonomous Hybrid System
Authors:
Benjamin Martin,
Khalil Ghorbal,
Eric Goubault,
Sylvie Putot
Abstract:
We formally verify a hybrid control law designed to perform a station keeping maneuver for a planar vehicle. Such maneuver requires that the vehicle reaches a neighborhood of its station in finite time and remains in it while waiting for further instructions. We model the dynamics as well as the control law as a hybrid program and formally verify both the reachability and safety properties i…
▽ More
We formally verify a hybrid control law designed to perform a station keeping maneuver for a planar vehicle. Such maneuver requires that the vehicle reaches a neighborhood of its station in finite time and remains in it while waiting for further instructions. We model the dynamics as well as the control law as a hybrid program and formally verify both the reachability and safety properties involved. We highlight in particular the automated generation of invariant regions which turns out to be crucial in performing such verification. We use the theorem prover Keymaera X to discharge some of the generated proof obligations.
△ Less
Submitted 8 September, 2017;
originally announced September 2017.
-
Robustness analysis of finite precision implementations
Authors:
Eric Goubault,
Sylvie Putot
Abstract:
A desirable property of control systems is to be robust to inputs, that is small perturbations of the inputs of a system will cause only small perturbations on its outputs. But it is not clear whether this property is maintained at the implementation level, when two close inputs can lead to very different execution paths. The problem becomes particularly crucial when considering finite precision i…
▽ More
A desirable property of control systems is to be robust to inputs, that is small perturbations of the inputs of a system will cause only small perturbations on its outputs. But it is not clear whether this property is maintained at the implementation level, when two close inputs can lead to very different execution paths. The problem becomes particularly crucial when considering finite precision implementations, where any elementary computation can be affected by a small error. In this context, almost every test is potentially unstable, that is, for a given input, the computed (finite precision) path may differ from the ideal (same computation in real numbers) path. Still, state-of-the-art error analyses do not consider this possibility and rely on the stable test hypothesis, that control flows are identical. If there is a discontinuity between the treatments in the two branches, that is the conditional block is not robust to uncertainties, the error bounds can be unsound.
We propose here a new abstract-interpretation based error analysis of finite precision implementations, which is sound in presence of unstable tests. It automatically bounds the discontinuity error coming from the difference between the float and real values when there is a path divergence, and introduces a new error term labeled by the test that introduced this potential discontinuity. This gives a tractable error analysis, implemented in our static analyzer FLUCTUAT: we present results on representative extracts of control programs.
△ Less
Submitted 16 September, 2013;
originally announced September 2013.
