Cumulative-Time Signal Temporal Logic

Signal Temporal Logic (STL) is a widely adopted specification language for Cyber-Physical Systems that can be used to express critical temporal requirements, such as system safety and response time. STL’s expressivity, however, 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) which operates over discrete-time signals and extends STL with a new cumulative-time operator. This operator compares the sum of all timesteps 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 the soundness and completeness of the robustness semantics. We also provide an efficient online monitoring algorithm for both semantics. We demonstrate the utility of CT-STL via two case studies: specifying and monitoring cumulative temporal requirements for a microgrid and an artificial pancreas.