Fast extraction of control constraints for uncertain system logic rules
Fast Constraint Extraction for Corrective Control under STL Specifications via Logical Dependency Tracking
Logic in Computer ScienceRobotics
Summary
Controlling systems to reliably meet complex timing and logical rules is hard when there’s uncertainty. The authors developed a fast way to figure out which parts of the system’s uncertain inputs actually cause problems in following these rules. They use a technique that tracks how uncertainty flows through the logic, enabling quick identification of conditions that must be met. This lets them efficiently adjust controls to correct the system behavior with strong guarantees that the rules will be satisfied.
What this means in practice
- •For control engineers: Adjust control inputs in real time to maintain complex time-dependent rules despite uncertain system behavior.
- •For robotics developers: Improve robotic system reliability by quickly finding and correcting control actions to satisfy nested logical safety and performance rules under uncertainty.
Authors
Antoine Besset, Joris Tillet, Chuchu Fan, Julien Alexandre dit Sandretto
Abstract
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/.