Pierre-Jean Meyer

Pierre-Jean Meyer, Alex Devonport, Murat Arcak

This paper presents TIRA, a Matlab library gathering several methods for the computation of interval over-approximations of the reachable sets for both continuous- and discrete-time nonlinear systems. Unlike other existing tools, the main strength of interval-based reachability analysis is its simplicity and scalability, rather than the accuracy of the over-approximations. The current implementation of TIRA contains four reachability methods covering wide classes of nonlinear systems, handled with recent results relying on contraction/growth bounds and monotonicity concepts. TIRA's architecture features a central function working as a hub between the user-defined reachability problem and the library of available reachability methods. This design choice offers increased extensibility of the library, where users can define their own method in a separate function and add the function call in the hub function.

Pierre-Jean Meyer, Dimos V. Dimarogonas

This paper presents a compositional approach to specification-guided abstraction refinement for control synthesis of a nonlinear system associated with a method to over-approximate its reachable sets. Given an initial coarse partition of the state space, the control specification is given as a sequence of the cells of this partition to visit at each sampling time. The dynamics are decomposed into subsystems where some states and inputs are not observed, some states are observed but not controlled and where assume-guarantee obligations are used on the uncontrolled states of each subsystem. A finite abstraction is created for each subsystem through a refinement procedure starting from a coarse partition of the state space, then proceeding backwards on the specification sequence to iteratively split the elements of the partition whose coarseness prevents the satisfaction of the specification. Each refined abstraction is associated with a controller and it is proved that combining these local controllers can enforce the specification on the original system. The efficiency of the proposed approach compared to other abstraction methods is illustrated in a numerical example.

Pierre-Jean Meyer, Samuel Coogan, Murat Arcak

This paper over-approximates the reachable sets of a continuous-time uncertain system using the sensitivity of its trajectories with respect to initial conditions and uncertain parameters. We first prove the equivalence between an existing over-approximation result based on the sign-stability of the sensitivity matrices and a discrete-time approach relying on a mixed-monotonicity property. We then present a new over-approximation result which scales at worst linearly with the state dimension and is applicable to any continuous-time system with bounded sensitivity. Finally, we provide a simulation-based approach to estimate these bounds through sampling and falsification. The results are illustrated with numerical examples on traffic networks and satellite orbits.

Octavio Narvaez-Aroche, Pierre-Jean Meyer, Stephen Tu et al.

The sit-to-stand movement is a key feature for wide adoption of powered lower limb orthoses for patients with complete paraplegia. In this paper we study the control of the ascending phase of the sit-to-stand movement for a minimally actuated powered lower limb orthosis at the hips. First, we generate a pool of finite horizon Linear Quadratic Regulator feedback gains, designed under the assumption that we can control not only the torque at the hips but also the loads at the shoulders that in reality are applied by the user. Next we conduct reachability analysis to define a performance metric measuring the robustness of each controller against parameter uncertainty, and choose the best controller from the pool with respect to this metric. Then, we replace the presumed shoulder control with an Iterative Learning Control algorithm as a substitute for human experiments. Indeed this algorithm obtains torque and forces at the shoulders that result in successful simulations of the sit-to-stand movement, regardless of parameter uncertainty and factors deliberately introduced to hinder learning. Thus it is reasonable to expect that the superior cognitive skills of real users will enable them to cooperate with the hip torque controller through training.

Octavio Narvaez-Aroche, Pierre-Jean Meyer, Murat Arcak et al.

A sensitivity-based approach for computing over-approximations of reachable sets, in the presence of constant parameter uncertainties and a single initial state, is used to analyze a three-link planar robot modeling a Powered Lower Limb Orthosis and its user. Given the nature of the mappings relating the state and parameters of the system with the inputs, and outputs describing the trajectories of its Center of Mass, reachable sets for their respective spaces can be obtained relying on the sensitivities of the nonlinear closed-loop dynamics in the state space. These over-approximations are used to evaluate the worst-case performances of a finite time horizon linear-quadratic regulator (LQR) for controlling the ascending phase of the Sit-To-Stand movement.

Pierre-Jean Meyer, Dimos V. Dimarogonas

This paper deals with the control synthesis problem for a continuous nonlinear dynamical system under a Linear Temporal Logic (LTL) formula. The proposed solution is a top-down hierarchical decomposition of the control problem involving three abstraction layers of the problem, iteratively solved from the coarsest to the finest. The LTL planning is first solved on a small transition system only describing the regions of interest involved in the LTL formula. For each pair of consecutive regions of interest in the resulting accepting path satisfying the LTL formula, a discrete plan is then constructed in the partitioned workspace to connect these two regions while avoiding unsafe regions. Finally, an abstraction refinement approach is applied to synthesize a controller for the dynamical system to follow each discrete plan. The second main contribution, used in the third abstraction layer, is a new monotonicity-based method to over-approximate the finite-time reachable set of any continuously differentiable system. The proposed framework is demonstrated in simulation for a motion planning problem of a mobile robot modeled as a disturbed unicycle.

Pierre-Jean Meyer

The literature on reachability analysis methods for neural networks currently only focuses on uncertainties on the network's inputs. In this paper, we introduce two new approaches for the reachability analysis of neural networks with additional uncertainties on their internal parameters (weight matrices and bias vectors of each layer), which may open the field of formal methods on neural networks to new topics, such as safe training or network repair. The first and main method that we propose relies on existing reachability analysis approach based on mixed monotonicity (initially introduced for dynamical systems). The second proposed approach extends the ESIP (Error-based Symbolic Interval Propagation) approach which was first implemented in the verification tool Neurify, and first mentioned in the publication of the tool VeriNet. Although the ESIP approach has been shown to often outperform the mixed-monotonicity reachability analysis in the classical case with uncertainties only on the network's inputs, we show in this paper through numerical simulations that the situation is greatly reversed (in terms of precision, computation time, memory usage, and broader applicability) when dealing with uncertainties on the weights and biases.

Abdelrahman Sayed Sayed, Pierre-Jean Meyer, Mohamed Ghazel

A neural ordinary differential equation (neural ODE) is a machine learning model that is commonly described as a continuous-depth generalization of a residual network (ResNet) with a single residual block, or conversely, the ResNet can be seen as the Euler discretization of the neural ODE. These two models are therefore strongly related in a way that the behaviors of either model are considered to be an approximation of the behaviors of the other. In this work, we establish a more formal relationship between these two models by bounding the approximation error between two such related models. The obtained error bound then allows us to use one of the models as a verification proxy for the other, without running the verification tools twice: if the reachable output set expanded by the error bound satisfies a safety property on one of the models, this safety property is then guaranteed to be also satisfied on the other model. This feature is fully reversible, and the initial safety verification can be run indifferently on either of the two models. This novel approach is illustrated on a numerical example of a fixed-point attractor system modeled as a neural ODE.

Abdelrahman Sayed Sayed, Pierre-Jean Meyer, Mohamed Ghazel

Neural ordinary differential equations (neural ODE) are powerful continuous-time machine learning models for depicting the behavior of complex dynamical systems, but their verification remains challenging due to limited reachability analysis tools adapted to them. We propose a novel interval-based reachability method that leverages continuous-time mixed monotonicity techniques for dynamical systems to compute an over-approximation for the neural ODE reachable sets. By exploiting the geometric structure of full initial sets and their boundaries via the homeomorphism property, our approach ensures efficient bound propagation. By embedding neural ODE dynamics into a mixed monotone system, our interval-based reachability approach, implemented in TIRA with single-step, incremental, and boundary-based approaches, provides sound and computationally efficient over-approximations compared with CORA's zonotopes and NNV2.0 star set representations, while trading tightness for efficiency. This trade-off makes our method particularly suited for high-dimensional, real-time, and safety-critical applications. Applying mixed monotonicity to neural ODE reachability analysis paves the way for lightweight formal analysis by leveraging the symmetric structure of monotone embeddings and the geometric simplicity of interval boxes, opening new avenues for scalable verification aligned with the symmetry and geometry of neural representations. This novel approach is illustrated on two numerical examples of a spiral system and a fixed-point attractor system modeled as a neural ODE.

Pierre-Jean Meyer

This paper presents a new reachability analysis approach to compute interval over-approximations of the output set of feedforward neural networks with input uncertainty. We adapt to neural networks an existing mixed-monotonicity method for the reachability analysis of dynamical systems and apply it to each partial network within the main network. This ensures that the intersection of the obtained results is the tightest interval over-approximation of the output of each layer that can be obtained using mixed-monotonicity on any partial network decomposition. Unlike other tools in the literature focusing on small classes of piecewise-affine or monotone activation functions, the main strength of our approach is its generality: it can handle neural networks with any Lipschitz-continuous activation function. In addition, the simplicity of our framework allows users to very easily add unimplemented activation functions, by simply providing the function, its derivative and the global argmin and argmax of the derivative. Our algorithm is compared to five other interval-based tools (Interval Bound Propagation, ReluVal, Neurify, VeriNet, CROWN) on both existing benchmarks and two sets of small and large randomly generated networks for four activation functions (ReLU, TanH, ELU, SiLU).

Pierre-Jean Meyer, Antoine Girard, Emmanuel Witrant

In this paper, we develop a compositional approach to abstraction and safety synthesis for a general class of discrete time nonlinear systems. Our approach makes it possible to define a symbolic abstraction by composing a set of symbolic subsystems that are overlapping in the sense that they can share some common state variables. We develop compositional safety synthesis techniques using such overlapping symbolic subsystems. Comparisons, in terms of conservativeness and of computational complexity, between abstractions and controllers obtained from different system decompositions are provided. Numerical experiments show that the proposed approach for symbolic control synthesis enables a significant complexity reduction with respect to the centralized approach, while reducing the conservatism with respect to compositional approaches using non-overlapping subsystems.