PaperlayerView exact revision on arXiv

Source-linked AI summary

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

Antoine Besset, Joris Tillet, Chuchu Fan, Julien Alexandre dit Sandretto

arXiv:2609.09439v1cs.LOcs.ROeess.SY

TL;DR

Under uncertainty, STL monitoring can certify satisfaction or expose indeterminacy without identifying corrective actions. The paper tracks logical dependencies through three-valued STL semantics to extract compact sufficient correction clauses, then uses reachable-tube constraints for guaranteed control correction. Experiments on nonlinear systems demonstrate formally guaranteed corrections under bounded uncertainty and certified probabilistic bounds in the stochastic case.

  • Problem

    Existing STL monitoring methods provide guaranteed or probabilistic assessment under uncertainty but do not determine corrective actions when satisfaction is indeterminate.

  • Method

    The method propagates markers and logical dependencies through the STL structure to produce a compact DNF of sufficient constraints, which is enforced using zonotopic reachable-tube control correction.

  • Results

    The approach yields millisecond dependency extraction without combinatorial enumeration and produces corrections guaranteeing STL satisfaction under bounded uncertainty with certified probabilistic bounds in stochastic settings.

  • Takeaways & Limitations

    Logical dependency tracking provides a tractable, formally guaranteed alternative to globally optimal correction by selecting logically minimal sufficient clause subsets at the cost of suboptimality.

  • Takeaways & Limitations

    Online deployment remains bottlenecked by reachability analysis, which takes 5–10 s, while the correction layer runs in milliseconds.

Abstract

from arXiv · show

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

I. INTRODUCTION

The paper addresses how to restore STL satisfaction when uncertainty makes specifications indeterminate, by tracking which reachable-set ambiguities affect global satisfaction and converting them into correction constraints.

  • Motivation: Uncertainty can make STL specifications indeterminate, while existing guaranteed monitoring methods do not compute corrective actions to restore satisfaction.Indeterminacy typically occurs when reachable sets intersect predicate boundaries, but local ambiguities do not all affect global satisfaction.
  • Assumptions: The paper assumes a nominal trajectory already satisfying the specification and having sufficient control margin for correction.Nominal trajectories may be obtained using planning, learning-based, optimization, robust-control, or multi-agent synthesis methods.
  • Approach: The framework tracks logical dependencies during signal propagation to identify reachable sets responsible for formula-level indeterminacy.It uses three-valued satisfaction propagation through the STL structure rather than direct All-SAT enumeration.
  • Contributions: Dependency tracking extracts a compact DNF of sufficient correction clauses in milliseconds without combinatorial enumeration and scales to hundreds of markers.The method is evaluated against All-SAT and single-enumeration strategies.
  • Control correction: The control application uses zonotopic reachable tubes and one linear program per clause to compute corrections guaranteeing formula satisfaction.The constraint-identification method is independent of the control-synthesis approach, although zonotopic parameterization is used for the demonstrated application.

B. Signal temporal logic

STL specifies temporal and state-dependent requirements for continuous-time systems, and the paper evaluates predicates and formulas over reachable tubes using three-valued semantics.

  • STL syntax: STL extends Linear Temporal Logic with atomic predicates, negation, disjunction, and temporal-until operators over continuous-time signals.The considered fragment permits arbitrarily nested eventually and always operators used in reach-avoid, recurrence, and sequencing specifications.
  • Predicate evaluation: Atomic predicates receive values 1, 0, or [0, 1] according to whether a reachable set is contained in, disjoint from, or intersects the predicate set.Predicate sets are represented as hyperboxes to facilitate linear optimization.
  • Three-valued semantics: Satisfaction signals are propagated bottom-up through the formula tree as certain and uncertain unitary signals.For bounded parameters, the resulting formula value is 1 when all trajectories satisfy it, 0 when all violate it, and [0, 1] when satisfaction is indeterminate.

D. Guaranteed probabilistic bound

The paper derives probabilistic satisfaction guarantees by validating parameter subsets and formulates minimum-effort corrections that enforce STL satisfaction through reachable-tube constraints.

  • Probabilistic guarantee: A validated parameter subset with probability c provides a lower bound of c on the probability that the STL formula is satisfied.The result follows from the inclusion of the validated subset in the formula-satisfaction set and monotonicity of probability measure.
  • Assumptions: The stochastic formulation assumes independent, stationary uncertain parameters with known initial probability distributions, without assuming a state distribution at later times.The control input is piecewise constant over the correction intervals.
  • Problem formulation: The correction problem seeks a minimum-effort control modification that guarantees Pr((ŷ, t) |= ϕ) ≥ c for a target confidence level c.For bounded uncertainty, the corresponding requirement is satisfaction for every parameter in the bounded set.
  • Constraint reduction: The chance constraint is reduced to inclusion conditions on reachable tubes at critical time intervals and then enforced as linear constraints.This reduction avoids handling the probabilistic constraint directly.

III. CRITICAL CONSTRAINTS IDENTIFICATION

The method identifies critical predicate constraints by tracking uncertainty and logical dependencies through STL formulas. It represents sufficient corrections as a logically minimal DNF rather than requiring all uncertain markers.

  • Critical constraints specify where a corrected reachable tube must satisfy strict predicate inclusion or exclusion in continuous time.The method addresses both temporal quantifier choices and indeterminacy caused by predicate crossings.
  • Three-valued signals carry markers that identify reachable sets and predicates responsible for indeterminate satisfaction.Markers are defined recursively as predicate clauses or logical combinations with expected satisfaction values from the nominal trajectory.
  • The framework tracks dependencies during propagation and discards insufficient clauses to produce a compact DNF of sufficient correction clauses.This avoids the pessimism of treating every reachable set causing indeterminacy as jointly necessary.
  • The master formula encodes whether the STL formula is guaranteed, and each DNF conjunction contains logically minimal predicate clauses.Removing any clause from a conjunction makes the master formula false.
  • Continuous-time Picard-box abstractions and discrete-time DNF rewritings limit the approach through varying interval lengths and possible combinatorial complexity.The stated limitations concern continuous-time monitoring abstractions and online discrete-time reformulations.

B. Propagation Rules to Track Logical Dependencies

Marker propagation exploits three-valued STL semantics and dominance relations to retain only dependencies that can affect satisfaction. The resulting logical structure remains tractable for hundreds of markers.

  • Markers propagate through STL syntax using expected values, with certain and uncertain unitary signals distinguished during computation.Tables I–III summarize propagation for disjunction, conjunction, and negation.
  • For disjunction, an expected value of 1 dominates; for conjunction, an expected value of 0 dominates; ties preserve joint dependencies.Negation inherits the marker while flipping its expected value.
  • The resulting logical structure stays mostly flat and supports millisecond-range DNF computation for 50 to 700 markers.This tractability is attributed to the propagation rules and their pruning of dominated dependencies.
  • Temporal operators propagate marker-associated unitary signals by shifting their time intervals back over the operator horizon.Fig. 1 illustrates this shift-back operation for F[a,b]ϕ.
  • The extracted DNF exposes alternative sufficient corrections, such as mitigating either Q1 ∧Q2 ∧Q3 or Q4 ∧Q5.Each conjunction is logically minimal because dominated markers are discarded.

C. Inherited Constraints

Inherited constraints account for conditions that remain necessary after selecting a DNF clause. The procedure projects uncertain signals, tracks their dependencies, and selects a tractable correction candidate.

  • The DNF decomposes the required reach-avoid conditions into alternative candidate constraint sets, from which the least costly correction can be selected.The exact corrected-tube position relative to the nominal trajectory is not required; set inclusion or exclusion is sufficient.
  • A corrected tube must satisfy inherited constraints from the nominal trajectory in addition to resolving the selected uncertain clauses.Examples include obstacle avoidance and timing constraints from temporal operators.
  • For each candidate clause, other atomic predicates are relaxed to [0, 1] while their expected values remain fixed, then irrelevant indeterminacy is discarded.The identification remains tractable in the reported 20–50 ms range.
  • Fig. 2 projects the full signal to [0, 1] and tracks timed and logical dependencies to derive additional constraints MA ∧MB.Blue, green, and red regions distinguish the critical time, projection, and projection result.
  • Computing the globally minimum correction would require retaining all combinations of inherited disjunctions, potentially producing Ktot ≈ K · K′ clauses.The implementation filters to one clause to keep correction computation tractable.

D. Probabilistic Extension and Scaling Vector

The probabilistic extension represents a desired probability level through a scaled parameter subset and converts chance constraints into reachable-tube conditions. Zonotopic corrections encode decision variables through symbolic generators.

  • A scaling vector A selects a subset Sc of the initial parameter set with prescribed probability P(Sc) = c.The construction begins with a mean-centered parameter set whose probability exceeds c.
  • Different scaling vectors distribute uncertainty differently across parameters, producing distinct reachable-tube widths and correction constraints.A discrete grid of A values can be sampled and propagated with contractor-based methods.
  • The chance constraint Pr((ŷ, t) |= ϕ) ≥ c is reduced to deterministic inclusion of the reachable tube associated with Sc.This avoids solving the constraint directly as a stochastic program.
  • Control corrections are encoded as zonotopic generators whose amplitudes are decision variables associated with unique noise symbols.With m control dimensions and Nc intervals, the corrected control zonotope has at most m·Nc generators.
  • Validated reachability separates parameter uncertainty, correction effects, and nonlinear or numerical remainder terms in the resulting reachable sets.The solver tracks symbolic correction dependencies through propagation, allowing fixed correction values to shift reachable-set centers.

B. Problem Formulation

The correction problem reduces critical reachable-set inclusions and exclusions to linear constraints for each selected sufficient clause. Under stated box and control-bound conditions, these constraints can be incorporated into a minimum-effort linear program.

  • 1) Geometric Constraints:: Each critical reachable set associated with a selected clause is constrained by inclusion in a reduced predicate, with exclusions handled analogously.The selected clause and inherited constraints determine the relevant critical-set index collection.
  • 1) Geometric Constraints:: The geometric reduction uses interval hulls of uncertainty and control zonotopes after translating the predicate box by the nominal reachable set.The resulting set is a box and may be empty when uncertainty exceeds the predicate margin.
  • 1) Geometric Constraints:: The geometric equivalence relies on the combined uncertainty and control zonotope being a box after the necessary order reduction for predicate evaluation.The interval hull operation is denoted by □(·).
  • 1) Geometric Constraints:: The reduced predicate is formed by subtracting the nominal reachable set and uncertainty hull from the original predicate box.Successive Pontryagin differences preserve the axis-aligned box structure used for the reduction.
  • 1) Geometric Constraints:: Inclusion of the correction zonotope in the reduced predicate is equivalent to linear constraints suitable for direct incorporation into the optimization problem.For a fixed scaling vector, these constraints support minimum-effort correction through a linear program.
  • 1) Geometric Constraints:: The theoretical guarantee holds only when every correction coordinate remains within its admissible interval v_j ∈ [-1, 1].The uncertainty zonotope is computed under these same bounds.

C. Feasibility and Iterative Refinement

The correction layer is evaluated on a nonlinear vehicle with piecewise commands, uncertain dynamics, and nested STL requirements. The setup uses validated reachable-tube computation and linear programming to test correction feasibility.

  • C. Feasibility and Iterative Refinement: The experiment selects a nominal trajectory that presents ambiguous cases intended to exercise the approach's key features.The dynamics and control structure are evaluated under uncertain gains and perturbations.
  • C. Feasibility and Iterative Refinement: The experiment uses a Dubins-like nonlinear vehicle with 15 command steps and 30 decision variables under uncertainty in gains and additive perturbations.The piecewise command has N_c = 15 steps, yielding 2N_c = 30 decision variables.
  • C. Feasibility and Iterative Refinement: The vehicle model uses throttle and steering feedback around a feedforward command, with uncertainty affecting both gains and additive disturbances.The control input is applied over the 15-step piecewise command.
  • C. Feasibility and Iterative Refinement: The STL specification requires waypoint visits, obstacle avoidance, goal reaching after the second waypoint, and stabilization in the goal region.The formula combines a flat waypoint-and-obstacle component with a nested goal-reaching component.
  • C. Feasibility and Iterative Refinement: Reachable tubes are computed with validated Runge-Kutta integration through DynIbex1, the LP is solved with GLPK, and the confidence grid contains 84 points.These tools support the bounded and probabilistic experiment configurations.

B. Bounded disturbances

The experiments evaluate correction under bounded, Gaussian, and multi-target uncertainty scenarios. The reported corrections satisfy the STL requirements while exposing conservatism and a practical effort–computation trade-off.

  • B. Bounded disturbances: The bounded-uncertainty scenario uses interval uncertainties in throttle gain, steering gain, and additive perturbations treated as constant within each integration step.The specified intervals are [K_v] = [2, 2.2], [K_c] = [1.8, 2], and [P_v] = [-0.025, 0.025].
  • B. Bounded disturbances: The bounded-uncertainty correction guarantees satisfaction after the nominal tube intersects obstacle 2, decelerating before waypoint 2 and accelerating toward the goal.The correction remains zero until deviation begins, and finer piecewise steps can reduce the resulting overshoot.
  • B. Bounded disturbances: Under Gaussian uncertainty, shifting the reach sequence from G[10,11] to G[8,9] enforces exclusion during the earlier period and prevents premature triggering.The correction is conservatively decelerated before waypoint 2, then accelerates and stabilizes in the goal region.
  • B. Bounded disturbances: In the multi-target scenario, one correction step steers and accelerates the system before feedback rejoins the nominal trajectory and stabilization succeeds for 1 s.Uncertainty affects both waypoint satisfaction and goal-region stabilization.
  • B. Bounded disturbances: For 84 parameter sets at probability threshold 0.95, the minimum correction effort is 1.5 and the maximum is 2.The variation in effort reflects a practical trade-off when computation time is not critical.

D. Computation Time

The correction layer runs in milliseconds, while reachability remains the main computational bottleneck; clause pruning and dependency-aware identification keep correction practical but can trade optimality for computation time.

  • Computation time: Total correction time scales linearly with the number of clauses, while dominated clauses are pruned to reduce computation to a single Ck.Each clause guarantees satisfaction, and pruning scores clauses by aggregating predicate membership degrees with a minimum operator.
  • Computation time: The average minimum correction increases from 1.7 to 2.2 when dominated clauses are pruned, highlighting a trade-off between optimality and computation time.The comparison is reported across all samples on the confidence-grid evaluation.
  • Constraint identification: Dependency-aware constraint identification avoids the combinatorial enumeration that makes the implemented SAT Evaluation intractable as markers grow.The alternative identifies constraints by backward testing ordered by robustness, while SAT enumeration can time out beyond one minute.
  • Method implications: The method provides a tractable, scalable alternative that selects a logically minimal sufficient clause subset with formal guarantees, at the cost of suboptimality.The correction formulation uses zonotopic reachable sets and linear programming to enforce the extracted clauses.
  • Computation time: The correction layer runs in milliseconds, whereas reachability analysis remains the main bottleneck at 5–10 s.The framework is independent of the reachability method, so faster reachability procedures could directly improve deployment time.
Loading 2609.09439v1…