Cumulative-Time Signal Temporal Logic

TL;DR

CT-STL addresses STL's inability to express cumulative durations by introducing a cumulative-time operator that aggregates the duration a property holds within an interval on discrete-time signals. The authors define qualitative and robustness semantics, prove robustness semantics are sound and complete with respect to the qualitative semantics, and provide online monitoring via RoSI and SlidingC. They validate CT-STL on microgrid voltage management and artificial pancreas control, demonstrating practical benefits for specifying and monitoring cumulative temporal requirements in CPS. This work yields a more expressive, tool-friendly formalism for ensuring safety and performance in timing-critical systems.

Abstract

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.

Figures (7)

• Figure 1: The acceptable region specifies upper bounds for the cumulative time of different overvoltage magnitudes over any one-minute time window. This figure is redrawn from the IEEE Standard 1547-2018 IEEE1547-2018.
• Figure 2: A snapshot of worklist[$v$] maintained for four (incremental) partial traces of the signal $\xi (t)$. $(\xi_{inf},\xi_{sup})$ correspond to the greatest lower bound and lowest upper bound on $\xi$. Each row is the worklist[$v$] when the signal point at the time in the first column is available. The colored entry is affected by the availability of a signal point with corresponding color.
• Figure 3: Microgrid model implemented using MATLAB Simulink.
• Figure 4: Simulated traces of voltages. (a) Voltage signal that violates $\varphi_5$. (b) The first 0.1 s of Figure \ref{['fig:voltages']}(a) determines the violation. (c) Voltage signal that satisfies $\varphi_5$. (d) The first 0.1 s of Figure \ref{['fig:voltages']}(c) shows no violation; so does the remaining signal.
• Figure 5: RoSIs for $\varphi_1$ to $\varphi_5$ are analyzed for Figures \ref{['fig:voltages']}(a)-(d). (a) The RoSI of $\varphi_5$ is sufficient to determine the violation of $\varphi_5$ w.r.t. the signal. (b) The upper bound of the RoSI of $\varphi_5$ turns negative shortly after $t=0.07$, allowing for an early termination. (c) The lower bound of the RoSI of $\varphi_5$ becomes positive near the end of the trace. This occurs because the rest short time is sufficient for $\varphi_5$ to be violated. (d) The lower bound of the RoSI for $\varphi_5$ becomes positive near the end of the trace. This occurs because a very short time window is sufficient for $\varphi_5$ to be violated.

Theorems & Definitions (14)

• Example 1: IEEE Standard
• Remark 1: Expressiveness of CT-STL
• Remark 2: Specifying cumulative-time upper bounds
• Example 2
• definition 1: Robustness
• definition 2: Secondary signals donze2010robust
• theorem 1: Property of Robustness
• Example 3
• Remark 3
• theorem 2