Modular and Online Monitoring of Temporal Logic Specification with Integral and Filter

In a recent work, Bakhirkin and Basset [3] proposed a new specification language that extends STL. Their logic overcomes the syntactic restrictions of STL, enabling the production and manipulation of real-valued output signals and the expression of properties that have typically been described using other logics, such as STL*. In this contribution, we extend this specification language in three directions. First, we introduce a novel integral operator over sliding windows, allowing the specification of cumulative properties, for example, asserting that the integral of a signal over a time interval remains within a given threshold. Second, we introduce a filtering operator for the sliding window operator, enabling us to restrict the scope of aggregation to signal segments that satisfy the filtering condition. Third, we develop an efficient online monitoring algorithm for the extended logic. Finally, we test the logic on two case studies: an artificial pancreas controller and a monitoring of outdoor weather events.