Cumulative-Time Signal Temporal Logic
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866915241542025216 |
|---|---|
| author | Chen, Hongkai Zhang, Zeyu Roy, Shouvik Bartocci, Ezio Smolka, Scott A. Stoller, Scott D. Lin, Shan |
| author_facet | Chen, Hongkai Zhang, Zeyu Roy, Shouvik Bartocci, Ezio Smolka, Scott A. Stoller, Scott D. Lin, Shan |
| contents | Signal Temporal Logic (STL) is a widely adopted specification language in cyber-physical systems for expressing critical temporal requirements, such as safety conditions and response time. However, STL's expressivity is not sufficient to capture the cumulative duration during which a property holds within an interval of time. To overcome this limitation, we introduce Cumulative-Time Signal Temporal Logic (CT-STL) that operates over discrete-time signals and extends STL with a new cumulative-time operator. This operator compares the sum of all time steps for which its nested formula is true with a threshold. We present both a qualitative and a quantitative (robustness) semantics for CT-STL and prove both their soundness and completeness properties. We provide an efficient online monitoring algorithm for both semantics. Finally, we show the applicability of CT-STL in two case studies: specifying and monitoring cumulative temporal requirements for a microgrid and an artificial pancreas. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2504_10325 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Cumulative-Time Signal Temporal Logic Chen, Hongkai Zhang, Zeyu Roy, Shouvik Bartocci, Ezio Smolka, Scott A. Stoller, Scott D. Lin, Shan Logic in Computer Science Signal Temporal Logic (STL) is a widely adopted specification language in cyber-physical systems for expressing critical temporal requirements, such as safety conditions and response time. However, STL's expressivity is not sufficient to capture the cumulative duration during which a property holds within an interval of time. To overcome this limitation, we introduce Cumulative-Time Signal Temporal Logic (CT-STL) that operates over discrete-time signals and extends STL with a new cumulative-time operator. This operator compares the sum of all time steps for which its nested formula is true with a threshold. We present both a qualitative and a quantitative (robustness) semantics for CT-STL and prove both their soundness and completeness properties. We provide an efficient online monitoring algorithm for both semantics. Finally, we show the applicability of CT-STL in two case studies: specifying and monitoring cumulative temporal requirements for a microgrid and an artificial pancreas. |
| title | Cumulative-Time Signal Temporal Logic |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2504.10325 |