发表机构
U2IS, ENSTA, Institut Polytechnique de Paris; Univ. Grenoble Alpes; CNRS; Grenoble INP; VERIMAG; REALM, AeroAstro, Massachusetts Institute of Technology（巴黎理工学院ENSTA U2IS; 格勒诺布尔阿尔卑斯大学; 法国国家科学研究中心; 格勒诺布尔国立理工学院; VERIMAG实验室; 麻省理工学院航空航天系REALM）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文提出逻辑依赖追踪框架，通过STL结构传播不确定性并提取紧凑DNF约束，实现毫秒级控制校正，保证非线性系统在不确定性下满足STL规范。
AI 中文摘要
在不确定性下确保信号时序逻辑（STL）规范的满足是具有挑战性的，因为基于可达性的监控提供了保证，但并未指明当满足性变得不确定时如何恢复满足。一个关键难点在于识别哪些不确定组件实际上影响全局满足性，尤其是对于嵌套公式。本文提出了一种逻辑依赖追踪框架，该框架通过STL结构传播不确定性，并捕获可达集对满足性的因果贡献。通过将标记关联到不确定谓词，并借助三值语义进行传播，我们在毫秒级时间内提取出紧凑的析取范式（DNF）形式的充分约束，避免了组合枚举。作为应用，我们将控制校正表述为一个最小努力优化问题。利用zonotopic可达性，所导出的约束通过线性规划强制执行，从而产生在有限不确定性下保证STL满足的校正，并在随机情况下提供认证的概率界。我们在一个具有嵌套STL规范的非线性系统上展示了该方法，表明依赖追踪能够实现高效且形式上保证的校正。追踪实现可在以下网址获取：此https URL。
英文摘要
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/.
CommentsAccepted for publication at 65th IEEE Conference on Decision and Control (CDC 26)
