Track papers across labs, topics, and trends.
Search papers, labs, and topics across Lattice.
The authors establish a logical dependency tracking framework that propagates reachability uncertainty through Signal Temporal Logic (STL) syntax trees using three-valued semantics to isolate which uncertain components causally dictate formula satisfaction. Resolving indeterminate temporal logic states has traditionally required intractable combinatorial searches over nested subformulas, prohibiting real-time corrective intervention. By extracting sufficient constraints into a compact Disjunctive Normal Form, this approach enables millisecond-level, minimum-effort control correction with certified deterministic or probabilistic guarantees via zonotopic reachability and linear programming.
Instead of combinatorially enumerating nested temporal logic formulas to fix control violations, tracking logical dependencies via three-valued semantics extracts certified corrective constraints in milliseconds.
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/.