Abstract
Ensuring the correctness of cyber-physical systems under uncertainty remains a critical challenge, particularly when verifying temporal properties. While stochastic methods provide probabilistic assessments, they often lack formal guarantees of completeness. In this work, we introduce a framework that combines reachability analysis with probabilistic reasoning through the Potential Cloud formalism, delivering a guaranteed enclosure for the probability of property satisfaction. We extend Signal Temporal Logic (STL) semantics to Potential Clouds, enabling the evaluation of property satisfaction with respect to confidence levels. A novel robustness metric is introduced to quantify the sensitivity of a tube to uncertainty. Additionally, we define and compute a safe set of confidence intervals that ensures STL satisfaction and associate this set with its probability of occurrence. The approach is compared against Probabilistic STL and ProbStarTL on representative benchmarks, showing that our method provides numerically stable lower bounds while remaining computationally tractable. The effectiveness of the approach is demonstrated on a multi-parameter nonlinear system and a neural network-controlled system, showing its potential for system design under rigorous probabilistic safety requirements.
| Original language | English |
|---|---|
| Article number | 109724 |
| Journal | International Journal of Approximate Reasoning |
| Volume | 197 |
| DOIs | |
| Publication status | Published - 1 Oct 2026 |
Keywords
- Hybrid system
- Nonlinear system
- Probabilistic STL
- Reachability analysis
- Signal temporal logic
Fingerprint
Dive into the research topics of 'Set-based monitoring for signal temporal logic with uncertainty mitigation and confidence guarantees'. Together they form a unique fingerprint.Cite this
- APA
- Author
- BIBTEX
- Harvard
- Standard
- RIS
- Vancouver