arXiv subjects

Julien Alexandre dit Sandretto

Publications and source records attributed to Julien Alexandre dit Sandretto.

4 recordsLinked to original sources

arXiv2026

Fast Constraint Extraction for Corrective Control under STL Specifications via Logical Dependency Tracking

Ensuring the satisfaction of Signal Temporal Logic (STL) specifications under uncertainty is challenging, as reachability-based monitoring provides guarantees but does not indicate how to restore satisfaction when it becomes indeterminate. A key difficulty is identifying which uncertain components actually affect global satisfaction, especially for nested formulas. This paper introduces a logical dependency tracking framework that propagates uncertainty through the STL structure and captures the causal contribution of reachable sets to satisfaction. By associating markers to uncertain predicates and propagating them via three-valued semantics, we extract in milliseconds a compact Disjunctive Normal Form (DNF) of sufficient constraints, avoiding combinatorial enumeration. As an application, we formulate control correction as a minimum-effort optimization problem. Using zonotopic reachability, the derived constraints are enforced via linear programming, yielding corrections that guarantee STL satisfaction under bounded uncertainty and provide certified probabilistic bounds in the stochastic case. We demonstrate the approach on a nonlinear system with nested STL specifications, showing that dependency tracking enables efficient and formally guaranteed correction. The tracking implementation is available at https://github.com/Antoine-Bst/STL-Three-Valued-Clause-Filtering/.

cs.LO↗

arXiv2025

Uncertainty Removal in Verification of Nonlinear Systems against Signal Temporal Logic via Incremental Reachability Analysis

A framework is presented for the verification of Signal Temporal Logic (STL) specifications over continuous-time nonlinear systems under uncertainty. Based on reachability analysis, the proposed method addresses indeterminate satisfaction caused by over-approximated reachable sets or incomplete simulations. STL semantics is extended via Boolean interval arithmetic, enabling the decomposition of satisfaction signals into unitary components with traceable uncertainty markers. These are propagated through the satisfaction tree, supporting precise identification even in nested formulas. To improve efficiency, only the reachable sets contributing to uncertainty are refined, identified through the associated markers. The framework allows online or offline monitoring to adapt to incremental system evolution while avoiding unnecessary recomputation. A case study on a nonlinear oscillator demonstrates a significant reduction in satisfaction ambiguity, highlighting the effectiveness of the approach.

cs.LO↗

arXiv2019

Sensitivity-based Heuristic for Guaranteed Global Optimization with Nonlinear Ordinary Differential Equations

We focus on interval algorithms for computing guaranteed enclosures of the solutions of constrained global optimization problems where differential constraints occur. To solve such a problem of global optimization with nonlinear ordinary differential equations, a branch and bound algorithm can be used based on guaranteed numerical integration methods. Nevertheless, this kind of algorithms is expensive in term of computation. Defining new methods to reduce the number of branches is still a challenge. Bisection based on the smear value is known to be often the most efficient heuristic for branching algorithms. This heuristic consists in bisecting in the coordinate direction for which the values of the considered function change the most "rapidly". We propose to define a smear-like function using the sensitivity function obtained from the differentiation of ordinary differential equation with respect to parameters. The sensitivity has been already used in validated simulation for local optimization but not as a bisection heuristic. We implement this heuristic in a branch and bound algorithm to solve a problem of global optimization with nonlinear ordinary differential equations. Experiments show that the gain in term of number of branches could be up to 30%.

math.NA↗

arXiv2018

Runge-Kutta Theory and Constraint Programming

There exist many Runge-Kutta methods (explicit or implicit), more or less adapted to specific problems. Some of them have interesting properties, such as stability for stiff problems or symplectic capability for problems with energy conservation. Defining a new method suitable to a given problem has become a challenge. The size, the complexity and the order do not stop growing. This informal challenge to implement the best method is interesting but an important unsolved problem persists. Indeed, the coefficients of Runge-Kutta methods are harder and harder to compute, and the result is often expressed in floating-point numbers, which may lead to erroneous integration schemes. Here, we propose to use interval analysis tools to compute Runge-Kutta coefficients. In particular, we use a solver based on guaranteed constraint programming. Moreover, with a global optimization process and a well chosen cost function, we propose a way to define some novel optimal Runge-Kutta methods.

math.NA↗