key: cord-0059626-sevieq06 authors: Mamouras, Konstantinos; Chattopadhyay, Agnishom; Wang, Zhifu title: Algebraic Quantitative Semantics for Efficient Online Temporal Monitoring date: 2021-03-01 journal: Tools and Algorithms for the Construction and Analysis of Systems DOI: 10.1007/978-3-030-72016-2_18 sha: 2e1dca98cea5cb14771743192f74d230c60f5630 doc_id: 59626 cord_uid: sevieq06 We investigate efficient algorithms for the online monitoring of properties written in metric temporal logic (MTL). We employ an abstract algebraic semantics based on semirings. It encompasses the Boolean semantics and a quantitative semantics capturing the robustness of satisfaction, which is based on the max-min semiring over the extended real numbers. We provide a precise equational characterization of the class of semirings for which our semantics can be viewed as an approximation to an alternative semantics that quantifies the distance of a system trace from the set of all traces that satisfy the desired property. Online monitoring is a lightweight verification technique for checking during runtime that a system behaves as desired. It has proved to be effective for evaluating the correctness of the behavior of complex systems, which includes cyber-physical systems (CPSs) that consist of both computational and physical processes. An online monitor is a program that observes the execution trace of the system and emits values that indicate events of interest or other actionable information. It is common to specify monitors using special-purpose formalisms such as variants of temporal logic and domain-specific programming languages. In the context of cyber-physical systems, logics that are interpreted over signals are frequently used. This includes Metric Temporal Logic (MTL) [30] and Signal Temporal Logic (STL) [33] . We focus here on properties specified with MTL and interpreted over discrete-time signals. We do not restrict the outputs of the monitor to Boolean (qualitative) verdicts, but allow for a quantitative interpretation of property satisfaction that admits various degrees of truth or falsity. Such quantitative interpretations of temporal logic have been considered before, including several variants of the so-called robust semantics of MTL [22, 20, 5] . Our starting point is the widely-used spatial robust semantics of MTL [22] . This uses the set R ±∞ = R ∪ {−∞, ∞} of the extended real numbers as truth values, where a positive number indicates truth, a negative number indicates falsity, and zero is ambiguous. Disjunction is interpreted as max, and conjunction is interpreted as min. Two quantitative semantic notions are considered in [22] : (1) the robustness degree degree(ϕ, u) of a trace u w.r.t. a formula ϕ, which is defined in a global way using distances between signals, and (2) the robust semantics ρ(ϕ, u) of a formula ϕ w.r.t. a trace u, which is defined by induction on the structure of ϕ. The former notion is the primary definition that captures the intuitive idea of the degree of satisfaction, whereas the latter is used as an approximate estimate. The usefulness of this estimate is justified by establishing a precise relationship between the two values [22] . The robust semantics of [22] has been used in prior work on online monitoring [16, 15] . We embark on an investigation of how to generalize the robustness framework of [22] to other notions of quantitative truth values. Instead of focusing exclusively on the concrete structure (R ±∞ , sup, inf, −∞, ∞), we take an abstract algebraic approach and look at classes of structures that are defined axiomatically. We start by considering the class of semirings, algebraic structures of the form (V, +, ·, 0, 1) with an addition operation + (which models disjunction) and a multiplication operation · (which models conjunction) satisfying a set of equational laws. is an especially interesting example, as it can be used to model uncertainty in the truth value: an element [a, b] indicates that the truth value lies somewhere within this interval. We use an algebraic generalization of the inductively-defined robust semantics of [22] , as our goal is to obtain online monitors that are time-and spaceefficient. Our main results are the following: -The theorem of [22] that relates degree(ϕ, u) and ρ(ϕ, u) is generalized from R ±∞ to a class of semirings. The class of semirings for which the theorem holds admits a precise axiomatic characterization (Theorem 7) . To obtain this, we develop a notion of symbolic quantitative languages that forms a semantic bridge between quantitative specifications and sets of traces. -We propose a new algorithm for efficient online monitoring (Theorem 11) that goes beyond existing algorithms. Prior monitors [16, 15] compute max or min over sliding-windows and therefore apply only to semirings that are linear orders (e.g., B and R ±∞ ). Our monitoring algorithm applies to values V that are partial orders or more general semirings. In order to obtain this algorithm, we reduce the monitoring of formulas of the form ϕ S [a,b] ψ and ϕ U [a,b] ψ to a sliding-window aggregation (which is neither max nor min). We provide an implementation of our algebraic monitoring framework in Rust. Our experiments show that our monitors scale reasonably well and they compare favorably against the state-of-the-art monitoring tool Reelay [40] . A semiring is an algebraic structure (V, +, ·, 0, 1), where + is called addition and · is called multiplication, that satisfies the following properties: (1) (V, +, 0) is a commutative monoid, (2) (V, ·, 1) is a monoid, (3) multiplication distributes over addition, and (4) 0 is an annihilator for multiplication. The last two properties say that x(y+z) = xy+xz, (x+y)z = xz+yz, and 0x = x0 = 0 for all x, y, z ∈ V . We sometimes write xy to mean x·y. A semiring V is called idempotent if addition is idempotent, that is, x + x = x for every x ∈ V . For an idempotent semiring, we define the partial order induced by + as follows: x ≤ y iff x + y = y. A homomorphism from a semiring U to a semiring V is a function h : U → V that commutes with the semiring operations. An epimorphism is a surjective homomorphism. Let U and V be idempotent semirings and h : U → V be a semiring homomorphism. Then, h is monotone (i.e., order-preserving). Example 1. The set B = {⊥, } of Boolean values with disjunction and conjuction is a semiring. The set T = {⊥, ?, } can be endowed with semiring structure as follows: x + ⊥ = x, x + = , ? + ? = ?, x · ⊥ = ⊥, x · = x, and ? · ? = ?, where · is commutative. The structure T is used to give a three-valued interpretation of formulas (? is inconclusive). The structure (R ±∞ , max, min, −∞, ∞) is the max-min semiring over the extended reals. The structure (R, +, ·, 0, 1) is a semiring and Z (integers) and N (natural numbers) are subsemirings of it. We interpret the max-min semiring R ±∞ as degrees of truth, where positive means true and negative means false. The value 0 is ambiguous. For this reason we also consider a variant of R ±∞ , where the value 0 is refined into a positive +0 (true) and a negative −0 (false). We thus obtain the max-min semiring For a set I of integers and n ∈ Z, define For a semiring V , an interval I = [i, j] (where i, j are natural numbers) and an I-indexed tuplex = (x i ) i∈I whose components are in V , we define x = If the tuplex is empty (i.e., I = ∅) then we define x = 0 and x = 1. We will consider formulas of Metric Temporal Logic (MTL) interpreted over traces that are finite or infinite sequences of data items from a set D. We write D * (resp., D + ) for the set of all finite (resp., non-empty finite) sequences over D, and D ω = ω → D for the set of all infinite sequences over D, where ω is the first infinite ordinal (i.e., the set of natural numbers). We also define D ∞ = D * ∪ D ω . We write ε for the empty sequence and |u| for the length of a trace, where |u| = ω if u is infinite. A finite sequence u ∈ D * can be viewed as a function from {0, . . . , |u| − 1} to D, that is, u = u(0)u(1) . . . u(|u| − 1). We also consider a semiring V whose elements represent quantitative truth values, and unary quantitative predicates p : D → V . We write 1, 0 : D → V for the predicates given by 1(d) = 1 and 0(d) = 0 for every d ∈ D. The set MTL(D, V ) of temporal formulas is built from the atomic predicates p : D → V using the Boolean connectives ∨ and ∧, the unary temporal connectives P I , H I , F I , G I , and the binary temporal connectives S I ,S I , U I ,Ū I , where I is an interval of the form [i, j] connective X ∈ {P, H, S,S, F, G, U,Ū}, we write X i as an abbreviation for X [i,i] and X as an abbreviation for X [0,∞) . Since we focus in this paper on online monitoring, we restrict attention to the future-bounded fragment of MTL, where the future-time temporal connectives are bounded. That is, every U I connective is of the form U [a,b] for a ≤ b < ω (and similarly for F I , G I ,Ū I ). We always assume this restriction on formulas. We interpret the formulas in MTL(D, V ) over traces from D ∞ and at specific time points. The interpretation function ρ : Fig. 1 . We say that the formulas ϕ and ψ are equivalent, and we write ϕ ≡ ψ, if ρ(ϕ, u, i) = ρ(ψ, u, i) for every u ∈ D ∞ and i < |u|. For every formula ϕ and every interval I, it holds that P I ϕ ≡ 1 S I ϕ, H I ϕ ≡ 0S I ϕ, F I ϕ ≡ 1 U I ϕ, and G I ϕ ≡ 0Ū I ϕ. We say that a semiring V refines B if there is a semiring homomorphism h : V → B. Notice that h is necessarily an epimorphism because h(0) = ⊥ and h(1) = . Informally, we think of h −1 (⊥) as the subset of "false" values and h −1 ( ) as the subset of "true" values. In particular, this means that V can be partitioned into true and false values. There are semirings that cannot refine B. For example, the semiring (Z, +, ·, 0, 1) of the integers cannot refine B. Let h : V → B. For a predicate p : D → V , we say that d ∈ D h-satisfies p, and we write d |= h p, if h(p(d)) = . For u ∈ D ∞ and i < |u| we define the satisfaction relation |= h as usual (for atomic formulas: Let D be a set of data items, V be a semiring, and h : V → B. The following are equivalent: (1) The function h is a semiring homomorphism. (2) u, i |= h ϕ iff h(ρ(ϕ, u, i)) = for every ϕ : MTL(D, V ), u ∈ D ∞ and i < |u|. Lemma 2 says that the qualitative semantics |= h agrees with the quantitative semantics ρ exactly when h : V → B is a semiring homomorphism. In this case, ρ is more fine-grained and loses no information regarding Boolean satisfaction. Pϕ ≡ P1(Pϕ) ∨ ϕ and Hϕ ≡ H1(Hϕ) ∧ ϕ The identities of Fig. 2 are all shown using the semiring axioms. The identity below can be used to reduce the monitoring of An early occurrence of this idea is in [19] , where they consider the more general Prior work on efficient monitoring [15] uses an algorithm based on it. Specifically, [15] uses a sliding-max algorithm [32] , which can be applied to the max-min semiring R ±∞ and other similar linear orders, but is not applicable to partial orders or other semirings. For a set D with at least two elements and a semiring V , the following are equivalent: (1) The semiring V is a bounded distributive lattice. (2) Equivalence (1) holds for all formulas ϕ, ψ ∈ MTL(D, V ). Proposition 4 gives a precise characterization of when the identity (1) applies. This characterization is axiomatic and identifies the class of bounded distributive lattices as the most general class for which the identity is valid. One important implication is that monitors that are based on this identity cannot be used for other semirings such as (R, +, ·, 0, 1) and (N, +, ·, 0, 1). We want to identify a notion of quantitative truth values in situations where we interpret formulas over a signal x[n] that is not known with perfect accuracy, but we can put an upper and lower bound on each sample, i.e., a ≤ x[n] ≤ b. For example, suppose that we know that 99.9 ≤ x[0] ≤ 100.1 and we want to evaluate the atomic predicate p = "x ≥ 99" at time 0. The truth value can be taken to be the interval [0.9, 1.1] in this case, since there is uncertainty in the distance of signal value from the threshold. More concretely, this situation of uncertain input signal can arise in the monitoring of systems where the raw signal is captured at one site, then compressed and transmitted to another site for monitoring. In many resource-constrained settings (e.g., certain IoT systems), the signal has to be compressed with a lossy compression scheme in order to meet network bandwidth constraints. So, at the monitoring site, the exact signal values are not known but can possibly be placed within intervals (depending on the used compression scheme). In order to model this kind of uncertainty, we consider the set I(R ±∞ ) of intervals of the form [a, b] with a ≤ b and a, b ∈ R ±∞ . An interval [a, b] ⊆ R ±∞ can be thought of as an uncertain truth value (it can be any one of those contained in The semiring I(R ±∞ ) is a partial order (more specifically, it is a bounded distributive lattice) and therefore does not fit existing monitoring frameworks that consider only linear orders (e.g., the max-min semiring R ±∞ of the extended reals and the associated sliding-max/min algorithms). In this section we start with our investigation of how to generalize the "robustness degree" of [22] to our abstract algebraic setting. The result of [22] that relates the robustness degree with the robust semantics is an inequality. For this reason, we focus on idempotent semirings, for which there is a natural partial order ≤ that is induced by semiring addition (x ≤ y iff x + y = y). Since our approach is abstract algebraic (i.e., axiomatic), we have no notion of real-valued distance between elements of D. Moreover, V does not need to be a semiring of real numbers. Instead, we rely on the intuition that for an atomic predicate p : D → V and a data item d ∈ D, the value p(d) gives a degree of truth or falsity. We propose using symbolic traces x = p 0 p 1 . . . p n−1 , which are sequences of atomic predicates, in order to compactly represent sets of concrete traces, which are sequences of data items. If each p i represents a subset S i ⊆ D, then x represents the set for each i} of concrete traces. Moreover, given a concrete trace u = u 0 u 1 . . . u n−1 ∈ D n , we can use the value p 0 (u 0 ) · p 1 (u 1 ) · · · p n−1 (u n−1 ) ∈ V as a quantitative measure of how close the trace u is to the set of traces L. We propose the interpretation of a formula ϕ as a language of symbolic traces. This will allow us to define the "closeness" of a trace u ∈ D n to the specification ϕ as a (semiring) sum of all the closeness values w.r.t. each symbolic trace in the symbolic language of ϕ. We will also see that this interpretation of a formula ϕ as a symbolic language is compatible with the standard interpretation of ϕ as a set of concrete traces. Using these definitions we obtain a generalization of the theorem of [22] that relates the robustness degree with the robust semantics. Additionally, we characterize precisely the class of semirings for which this generalization is possible. Let V be an idempotent semiring. For predicates p, q : The intuition for p ≤ q is that p is a stronger predicate than q. We write F(D, V ) to denote the set of atomic quantitative predicates, which always includes the predicates 1 and 0. For symbolic traces x, y ∈ F(D, V ) ∞ with λ = |x| = |y| we define x ≤ y if x(i) ≤ y(i) for every i < λ. These relations ≤ on predicates and traces are partial orders. We define the symbolic satisfaction relation |=, where x, i |= ϕ says that the formula ϕ : For atomic formulas, we put x, i |= p iff x(i) ≤ p. The definition is given by induction on ϕ in the usual way. For a formula ϕ : MTL(D, V ), length λ ∈ ω ∪ {ω} and a position i < λ, we define the symbolic language SL(ϕ, for every u ∈ D n . Informally, the value x[u] quantifies how close the concrete trace u is to the symbolic trace x. For the symbolic trace x = "x ≥ 1" "x ≤ 5" "x ≥ 2" and the concrete trace u = 3 6 8 we get that For the formula ϕ = p ∧ F 1 q, where p and q are atomic predicates, we have that SL(ϕ, The definition of the robustness degree in [22] where u is a trace, L is a set of traces, and dist is a metric. Notice that this is a supremum over a potentially infinite set. The semirings that we have considered so far have an addition operation that can model a finitary supremum. In order to model an infinitary supremum, we need to consider semirings that have an infinitary addition operation. A complete semiring is an algebraic structure (V, +, , ·, 0, 1), where i∈I x i is the sum of the I-indexed tuple of elements (x i ) i∈I , that satisfies: (1) i∈∅ x i = 0, i∈{j} x i = x j , i∈{j,k} x i = x j + x k for j = k, and k∈K i∈I k x i = i∈I x i where I = k∈K I k and the index sets (I k ) k∈K are pairwise disjoint, (2) (V, ·, 1) is a monoid, (3) the infinite distributivity properties ( i∈I x i ) · y = i∈I (x i y) and x · ( i∈I y i ) = i∈I (xy i ) hold for every index set I and all x i , y ∈ V , and (4) 0 is an annihilator for multiplication. A complete semiring V is idempotent if i∈I x i = x for every non-empty index set I with x i = x for every i ∈ I. Informally, val(ϕ, u, i) is a measure of how close the trace u is to satisfying ϕ at position i. It is an abstract algebraic variant of the robustness degree [22] . Let D be a set of data items and V be an idempotent complete semiring. Then, the following are equivalent: (1) The multiplication of V is idempotent and 1 is the top element of V . (2) For every ϕ : MTL(D, V ), u ∈ D + and i < |u|, val(ϕ, u, i) ≤ ρ(ϕ, u, i). Proof. Assume that (1) holds. Let n ≥ 1 be an integer. For a symbolic language L ⊆ F(D, V ) n and for u ∈ D n , we define val(L, u) = x∈L x(u). Let {L i } i∈I be a collection of languages with L i ⊆ F(D, V ) n . Then, by the idempotence of multiplication. This property extends to val(L 1 ∩ · · · ∩ L k , u) ≤ val(L 1 , u) · · · val(L k , u). Now, we will prove (2) (3) and (4). The proof that (2) implies (1) is not too difficult, and we therefore omit it. Theorem 7 could be considered an abstract algebraic counterpart of the result of [22] (page 4268, Theorem 13) for discrete finite traces. We will discuss later how it can be used to obtain the original result (for the max-min semiring R ±∞ ) as a corollary. Additionally, Theorem 7 gives a precise equational characterization of the class of semirings for which the relationship between the two semantics holds. Let D be a set of data items, V be a semiring and h : V → B. For a formula ϕ : MTL(D, V ), length λ ∈ ω ∪ {ω} and i < λ, we define the concrete trace language |= h x(i) for every i < n. Lemma 8 below establishes a correspondence between the symbolic and concrete language of a formula ϕ, which we need to connect Theorem 7 to the concrete setting of [22] . In this section, we consider the concrete quantitative setting where V is the maxmin semiring R ±∞ . We will obtain the result of [22] that relates the robustness degree with the robust semantics as a consequence of Theorem 7. A metric space is a set M together with a function dist : M ×M → R ≥0 , called metric, satisfying: (1) dist(x, y) = 0 iff x = y for all x, y ∈ M , (2) dist(x, y) = dist(y, x) for all x, y ∈ M , and (3) dist(x, z) ≤ dist(x, y)+dist(y, z) for all x, y, z ∈ M . Given a metric dist on M we define the distance function Dist as follows: Let D be a metric space of points (data items). Let p be a propositional letter (symbol), and O(p) ⊆ D be its interpretation, that is, the set of points for which p is true. The corresponding quantitative predicate is p : D → R ±∞ given by p(d) = Dist(d, O(p)) for every d ∈ D. Given the metric dist on D, we obtain a metric dist : be the set of traces (of length n) that satisfy ϕ at i (defined using the interpretation function O). Corollary 9 below was proved in [22] . We will give a proof that relies on the algebraic variant that we presented earlier. Proof. We will use the semiring R ±∞ ±0 ∼ = B × R ∞ ≥0 instead of R ±∞ , so that the value 0 is not ambiguous (it can be either true or false when we use R ±∞ ). That is, we will have a positive zero +0 (true) and a negative zero −0 (false). The semiring homomorphism h : R ±∞ ±0 → B sends the positive (resp., negative) elements to (resp., ⊥). We will interpret a predicate symbol p as the quantitative predicate p : By negating the above inequality we get that which is ≤ x∈SL(ϕ,n,i) x[u] = val(ϕ, u, i). From Theorem 7 we get val(ϕ, u, i) ≤ ρ(ϕ, u, i) and therefore −dist(u, CL O (ϕ, n, i)) ≤ ρ(ϕ, u, i). From Corollary 9 we can also obtain ρ(ϕ, u, i) ≤ dist(u, ∼CL O (ϕ, n, i) ). This inequality is equivalent to −dist(u, ∼CL O (ϕ, n, i)) ≤ −ρ(ϕ, u, i), which in turn is equivalent to −dist(u, CL O (∼ϕ, n, i)) ≤ ρ(∼ϕ, u, i) . The operation ∼ on formulas is a pseudo-negation, that is, ∼ϕ is the formula that results by "dualizing" all connectives and negating the atomic predicates. This operation is meaningful for the semiring R ±∞ . The final inequality is an instance of Corollary 9 for ∼ϕ. Theorem 7 and Corollary 9 are not used later for the monitoring algorithm. The significance of our theorem is that it can be instantiated to give the existing result from [22] . This serves as a sanity check for our algebraic framework and it supports the semiring-based semantics of Sect. 2. For an infinite input trace u ∈ D ω , the output of the monitor for the time instant t should be ρ(ϕ, u, t), but the monitor has to compute it by observing only a finite prefix of u. In order for the output value of the monitor to agree with the standard temporal semantics over infinite traces we may need to delay an output item until some part of the future input is seen. For example, in the case of F 1 p we need to wait for one time unit: the output at time t is given after the input item at time t + 1 is seen. In other words, the monitor for F 1 p has a delay (the output is falling behind the input) of one time unit. Symmetrically, we can allow monitors to emit output early when the correct value is known. For example, the output value for P 1 p is 0 in the beginning and the value at time t is already known from time t − 1. So, we also allow monitors to have negative delay (the output is running ahead of the input). The function dl : MTL → Z gives the amount of delay required to monitor a formula. It is defined by dl(p) = 0 and The monitor TL(ϕ) for a formula ϕ is a variant of a Mealy machine. If dl(ϕ) = 0, the TL(ϕ) is precisely a Mealy machine (one output item per input item) with inputs D and outputs V . If = dl(ϕ) > 0, then TL(ϕ) emits no output for the first steps and then behaves like a Mealy machine. If = dl(ϕ) < 0, then TL(ϕ) emits items upon initialization and continues to behave like a Mealy machine. The monitor emit(n, v) emits n copies of the value v ∈ A upon initialization and then echoes the input trace. The monitor ignore(n) discards the first n items of the trace and proceeds to echo the rest of the trace. The monitor wnd(n, v, op) performs an aggregation, given by the associative function op : A × A → A, over a sliding window of size n. It initializes the window using the value v : A and emits output at the arrival of every item. The monitor wndV(n, op) is different in that it starts with an empty window and it only starts emitting output when the window fills up with n items. We will combine monitors using the operations serial composition >> and parallel composition par. In the serial composition G >> H the output trace of G is propagated as input trace to H. In the parallel composition par(G, H) the input trace to copied to two concurrently executing monitors G and H and their output traces are combined. Both combinators >> and par are given by variants of the product construction on state machines. In the case of par the output traces of G and H may not be synchronized (one may be ahead of the other), which requires some bounded buffering in order to properly align them. The construction for par is described in [37] . Some variants of the combinators of Figure 3 are part of the StreamQL language [29] , which has been proposed for the processing of streaming time series. The identities of Fig. 2 suggest that MTL monitoring can be reduced to a small set of computational primitives. In fact, the primitives described earlier are sufficient to specify the monitors, as shown in Fig. 4 . We write π 1 : A × B → A for the left projection and π 2 : A × B → B for the right projection. Let u ∈ D + and n = |u|. If n > a then ρ(ϕ S [0,a] ψ, u, n − 1) = ρ (ϕ S ψ, v, a) , where v is the suffix of u with a + 1 items. If n ≤ a then ρ(ϕ S [0,a] ψ, u, n − 1) = TL(p) = map(p) TL(ϕ ∨ ψ) = par(TL(ϕ), TL(ψ)) >> map(+) TL(Pϕ) = TL(ϕ) >> aggr(0, +) TL(P a ϕ) = TL(ϕ) >> emit(a, 0) TL(P [a,∞) ϕ) = TL(PaPϕ) TL(ϕ S ψ) = par(TL(ϕ), TL(ψ)) >> aggr(0, opS ) if m = n then // full new block // convert new block to old ρ(ϕ S ψ, 0 a+1−n u, a). So, we can implement a monitor for the connective S [0,a] by computing S over a window of exactly a + 1 data items. Proposition 10 (Aggregation for S, U). Let V be a semiring. For every trace u = u 0 u 1 . . . u n−1 ∈ (V ×V ) + of length n = |u|, the values ρ(π 1 Sπ 2 , u, n−1) and ρ(π 1 U π 2 , u, 0) can be written as aggregates of the form π 2 (u 0 ⊗ u 1 ⊗ · · · ⊗ u n−1 ). Proposition 10 justifies the translation of S [0,b] /U [0,b] into monitors (Fig. 4) . Now, we will describe the data structure that performs the sliding aggregation. It is used in Fig. 3 in the monitors wnd and wndV. The implementation is shown in Fig. 4 . Suppose that the current window (of size n) is [x 0 , x 1 , . . . , x n−1 ]. We maintain a buffer of the form [x n−m , . . . , x n−1 , y 0 , . . . , y n−1−m ], where the part [x n−m , . . . , x n−1 ] is the block of newer elements ("new block") and the part [y 0 , . . . , y n−1−m ] contains aggregates of the older elements ("old block"). They satisfy the invariant y i = x i ⊗· · ·⊗x n−1−m for every i = 0, . . . , n−1−m. We also maintain the aggregate z = x n−m ⊗ · · · ⊗ x n−1 of the new block. So, the overall aggregate of the window is agg = y 0 ⊗z. When a new item d arrives, we evict the aggregate y 0 corresponding to the oldest item x 0 and replace it by d. Thus, the new block is expanded with the additional item d and therefore we also update the aggregates z and agg. When the new block becomes full (i.e., m = n) then we convert it to an old block by performing all partial aggregations from right to left. This conversion requires n − 1 applications of ⊗, but it is performed once every n items. So, the algorithm needs O(1) amortized time-per-item. Proof. The algorithm needs space that is exponential in the size of ϕ because of the connectives of the form X [a,∞) and X [a,b] . The monitor uses buffers of size a or b − a. Since the constants a, b are written in binary notation, we need space that is exponential in the size. The O(|ϕ|) amortized time per element hinges on the algorithm of Fig. 4 , which is used for S [0,b] and U [0,b] . As discussed earlier, this algorithm needs O(1) amortized time-per-item. We have implemented our semiring-based monitoring framework in Rust. We compare our implementation with the verified lattice-based monitors of [13] and the monitoring tool Reelay [40] . We perform our experiments using the (R ±∞ , max, min) semiring for truth values, which are approximately represented using 64-bit floating-point numbers. We have observed that all three tools process items at a roughly constant rate. We summarize the performance of a monitor with the average time it takes to process one data item (i.e., amortized time-per-item). In Fig. 5 , we consider formulas X [0,n] , X n , X [n,2n] , X [n,∞) where X ∈ {S, P}. We show the time-per-item for the monitors for n = 1, 10, 10 2 , 10 3 , 10 4 , 10 5 , 10 6 . We have also evaluated how the monitors for future temporal connectives scale with respect to the constants in the intervals. In Fig. 6 , we benchmark all tools using formulas from the Timescales benchmark [39] . Our monitors are generally more than 100 (resp., 10) times faster than Reelay (resp., the lattice-based tool of [13] ). The profiling tools Valgrind [38] and Heaptrack [41] are used to analyze the memory consumption of the monitors. Our Rust implementation, given a formula, begins by allocating a fixed amount of memory and does not allocate any more memory during the rest of the computation. Reelay allocates and de-allocates memory throughout its execution. The lattice-based monitor is implemented in OCaml (which is a garbage-collected language) and consumes a larger amount of memory. In Fig. 5 , we plot the peak memory usage of the monitors. We note that our tool does not seem to be allocating an increasing amount of memory for P n and similar formulas. This is because the corresponding monitor for P n emits output as early as possible and therefore does not need to use a buffer. In the case of the lattice-based monitor and our tool, we observe that the memory consumption does not depend on the input trace (it only depends on the formula). In the case of Reelay, it appears that the memory consumption depends on the input trace. We have plotted the behavior for two different input traces: one that consists of an increasing sequence of values ("reelay-ascending"), and another one that is decreasing ("reelay-descending"). We have only measured the memory usage of Reelay for up to n = 2 13 , as the execution becomes very slow beyond this value. We use case studies from the automotive domain, which have been suggested as benchmarks for hybrid system verification [25] . The Automatic Transmission System has two input signals (a throttle and a break) and three output signals: the gear sequence (g i for each gear i), the engine rotation speed (in [25] , we consider five properties: 10] ((¬g 3 )S ((¬g 2 )S (¬g 1 ))))). All constants in the temporal connectives are in seconds, and we choose the constants v = 120 and ω = 4500. Formula A 3 says that before changing from the second to the first gear, at least 2.5 seconds must first pass. Formula A 4 says that keeping the engine speed low enough should ensure that the vehicle does not exceed a certain speed. Formula A 5 says that changing the gear from the first to the fourth within 10 seconds, and then having the engine speed exceed ω will cause the vehicle speed to exceed v. The other case study is a Fault-Tolerant Fuel Control System. We monitor two properties. The first is (F uelF lowRate > 0) . The other property is to ensure that whenever the air-to-fuel ratio goes out of bounds, then within 1 second it should settle back and stay there for a second. This is written as F 2 = (H [0,1] airF uelRatio < 1)S [0,2] airF uelRatio < 1. The experimental results are shown in Fig. 6 . All of our experiments were executed on a laptop with an Intel Core i7 10610U CPU clocked at 2.30GHz and 16GB of memory. Each value reported is the mean of 20 executions of the experiment. The whiskers in the plots indicate the standard deviation across all executions. Fainekos and Pappas [22] define the robustness degree of satisfaction in terms of the distance of the signal from the set of desirable ones (or its complement). They also suggest an under-approximation of the robustness degree which can be effectively monitored. This is called the robust semantics and is defined by induction on STL formulas, by interpreting conjunction (resp., disjunction) as min (resp., max) of R ±∞ . Our paper explores this robust semantics (and the related approximation guarantee) in the general algebraic setting of semirings. In [27] , the authors study a generalization of the robustness degree by considering idempotent semirings of real numbers. They also propose an online monitoring algorithm that uses symbolic weighted automata. While this approach computes the precise robustness degree in the sense of [22] , the construction of the relevant automata incurs a doubly exponential blowup if one considers STL specifications. In [13] , it is observed that an extension of the robust semantics to bounded distributive lattices can be effectively monitored. In this paper, we generalize this semantics by considering semirings (bounded distributive lattices are semirings). Semirings are also used in [9] , where the authors consider a spatio-temporal logic. They consider the class of constraint semirings, which require the semiring order to induce a complete lattice. Efforts have been made to define notions of robustness that take temporal discrepancies into account. In [20] , we see a definition of temporal robustness by considering the effect of shifting the signal in time. The "edit distance" between discretized signals is proposed as a measure of robustness in [26] . Abbas et al. [3] define a notion of (τ, ε) closeness between signals, which considers temporal and value-based guarantees separately. In [2] , a metric based on conformance is put forward for applications in cardiac electrophysiology. Averaging temporal operators are used in [5] , which assign a higher value to temporal obligations that are satisfied earlier. A key ingredient for the efficient monitoring of STL is a streaming algorithm for sliding-window maximum [19, 15] . The tool Breach [17, 18] , which is used for the falsification of temporal specifications over hybrid systems, uses the sliding-maximum algorithm of [32] . In contrast, we use a more general sliding aggregation which applies to any associative operation (not only max/min) and does not require the truth values to be totally ordered. Different approaches for interpreting future temporal connectives in the context of online monitoring have been studied. While [16] assumes the availability of a predictor to interpret future connectives, [21] considers robustness intervals: the tightest intervals which cover the robustness for all possible extensions of the available trace prefix. Reelay [40] exclusively uses past-time connectives. The transducer-based framework of [37] can be used to monitor rich temporal properties which depend on bounded future input by allowing some bounded delay in the output. There is a large amount of work on formalisms, domain-specific languages and associated tools for quantitative online monitoring and, more generally, for data stream processing. The synchronous language LOLA [14] has served as the basis for the StreamLAB tool [23] , which is used for monitoring cyber-physical systems. Quantitative Regular Expressions [36] and associated automata-theoretic models with registers [7, 8, 6] have been used to express complex online detection algorithms for medical monitoring [1, 4] . There are many synchronous languages and models of computation based on Kahn's dataflow model [28] that have been used for signal processing [31] and embedded controller design [12, 11, 10] . The construction of online monitors described in Sect. 5 relies on a set of combinators that constitute a simple domain-specific language for stream processing. Our focus here, however, is on providing efficient monitors for MTL formulas with a quantitative semantics, rather than designing a general-purpose language for monitor specification. The compositional construction of automata-based monitors from temporal specifications has also been considered in [34, 35, 24] . We have presented a new efficient algorithm for the online monitoring of MTL properties over discrete traces. We have used an abstract algebraic semantics based on semirings, which can be instantiated to the widely-used Boolean (qualitative) and robustness (quantitative) semantics, as well as to other partially ordered semirings. We also provide a theorem that relates our quantitative semantics with an algebraic generalization of the robustness degree of [22] . We have provided an implementation of our algebraic monitoring framework, and we have shown experimentally that our monitors scale reasonably well and are competitive against the state-of-the-art tool Reelay [40] . Real-time decision policies with predictable performance Generalized robust MTL semantics for problems in cardiac electrophysiology Formal property verification in a conformance testing framework Quantitative regular expressions for arrhythmia detection Time robustness in MTL and expressivity in hybrid system falsification Streamable regular transductions Automata-based stream processing Modular quantitative monitoring Monitoring mobile and spatially distributed cyber-physical systems Synchronous programming with events and relations: The SIGNAL language and its semantics The Esterel synchronous programming language: Design, semantics LUSTRE: A declarative language for real-time programming A verified online monitor for metric temporal logic with quantitative semantics LOLA: Runtime monitoring of synchronous systems Robust online monitoring of signal temporal logic On-line monitoring for temporal logic robustness Breach, a toolbox for verification and parameter synthesis of hybrid systems Breach: A MATLAB toolbox for simulation-based design of dynamical/CPS/hybrid systems Efficient robust monitoring for STL Robust satisfaction of temporal logic over real-valued signals Efficient guiding strategies for testing of temporal properties of hybrid systems Robustness of temporal logic specifications for continuous-time signals StreamLAB: Stream-based monitoring of cyber-physical systems From real-time logic to timed automata Benchmarks for temporal logic requirements for automotive systems Quantitative monitoring of STL with edit distance An algebraic framework for runtime verification The semantics of a simple language for parallel programming StreamQL: A query language for processing streaming time series Specifying real-time properties with metric temporal logic Static scheduling of synchronous data flow programs for digital signal processing Streaming maximum-minimum filter using no more than three comparisons per element Monitoring temporal properties of continuous signals Real time temporal logic: Past, present, future From MITL to timed automata StreamQRE: Modular specification and efficient evaluation of quantitative queries over streaming data Online signal monitoring with bounded lag The Valgrind Developers: Valgrind: An instrumentation framework for building dynamic analysis tools Timescales: A benchmark generator for MTL monitoring tools The Reelay monitoring tool Heaptrack: A heap memory profiler for Linux Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/ 4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.