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.

翻译：本文提出了一种框架，用于在不确定性条件下验证连续时间非线性系统对信号时序逻辑（STL）规范的满足性。该方法基于可达性分析，解决了因过度逼近的可达集或不完整仿真所导致的满足性不确定问题。通过布尔区间运算扩展了STL语义，使得满足性信号可分解为带有可追踪不确定性标记的单元分量。这些分量在满足性树中传播，支持对嵌套公式的精确识别。为提高效率，仅对导致不确定性的可达集进行细化，这些集合通过相关标记进行识别。该框架支持在线或离线监测，以适应系统的增量演化，同时避免不必要的重复计算。通过对非线性振荡器的案例研究，展示了该方法显著降低了满足性模糊度，凸显了其有效性。