Search for highly-ionizing particles in pp collisions at the LHC's Run-1 using the prototype MoEDAL detector

The European Physical Journal C, 82 (8)

section_name: Introduction

section_content: System monitoring is a wide-spread requirement for many kinds of systems, ranging from enterprise data centers to power grids. Both public and private companies are increasingly required to monitor whether their system usage complies with normative regulations. For example, US hospitals must follow the US Health Insurance Portability and Accountability Act (HIPAA) and financial services must conform to the Sarbanes-Oxley Act (SOX). Firstorder temporal logics are not only well-suited for formalizing such regulations, they also admit efficient monitoring. When used online, these monitors observe the actions of agents, such as users and their processes, and report violations. This can be in real-time, as the actions occur. Alternatively, the actions are logged and the monitor checks them later, such as during an audit. See, for example, [6, 19]. 

Current logic-based monitoring approaches are limited in their support for expressing and monitoring properties of aggregations. Such properties are often needed to express compliance policies, such as the following simple example from fraud prevention: A user must not withdraw more than $10,000 within a 31 day period from his credit card account. To formalize this policy, we need an operator to express the aggregation of the withdrawal amounts over the specified time window, grouped by the users. In this article, we address the problem of expressing and monitoring first-order temporal properties built from such aggregation operators.
section_name: Motivation

section_content: First, we extend metric first-order temporal logic (MFOTL) with aggregation operators and with functions. This follows Hella et al. 's [20] extension of first-order logic with aggregations. We also ensure that the semantics of aggregations and grouping operations in our language mimics that of SQL. As an illustration, a formalization in our language of the above frauddetection policy is ∀u. ∀s. [SUM a a. [0,31) withdraw(u, a)](s; u) → s 10000. 

(P0)

The SUM operator, at the current time point, groups all withdrawals for a user u over the past 31 days and sums up their amounts a. The aggregation formula defines a binary relation where the first coordinate is the SUM's result s and the second coordinate is the user u for whom the result is calculated. If the user's sum is greater than 10,000, then the policy is violated at the current time point. The formula (P0) therefore states that the aggregation condition must hold for each user and every time point. For comparison, an SQL query for determining the violations with respect to the above policy at a specific time is SELECT SUM(a) AS s, u FROM W GROUP BY u HAVING SUM(a) > 10000. 

Here W is the dynamically created view consisting of the withdrawals of all users within the 31 day time window relative to the given time. Note that the subscript a of the formula's aggregation operator in (P0) corresponds to a in the SQL query and the third appearance of a in (P0) is implicit in the query, as it is fixed by the view's definition. The second a in (P0) is redundant; its inclusion emphasizes that the variable a is bound, i. e., it does not correspond to a coordinate in the resulting relation. Not all formulas in our language are monitorable. Unrestricted use of logic operators may require infinite relations to be built and manipulated. The second part of our solution, therefore, is a monitorable fragment of our language. It can express all our examples, which represent typical policy patterns, and it allows the liberal use of aggregations and functions. We extend our monitoring algorithm for MFOTL [8] to this fragment. In more detail, the algorithm processes log files sequentially and evaluates formulas in a bottom-up manner, using extended relational algebra operators to compute the evaluation of a formula from the evaluation of its direct subformulas. In particular, aggregation formulas are handled as the homonymous relational algebra operators. Functions are handled similarly to Prolog, where variables are instantiated before functions are evaluated. 

We have implemented our monitoring solution and we evaluate it, comparing it with the relational database management system PostgreSQL [23] and the stream-processing tool STREAM [2]. Our evaluation focuses on two aspects: the suitability of our proposed language for formalizing complex policies with aggregations (our examples are from the domain of fraud detection) and the performance of our prototype implementation. The results show that our language is better suited for specifying policies than SQL and our prototype's performance is superior to PostgreSQL's performance. This is because temporal reasoning must be explicitly encoded in SQL queries and PostgreSQL does not process logged data sequentially in time. STREAM's query language CQL [3] has limited support for temporal reasoning and several temporal constructs must be explicitly encoded, as is the case with SQL. It is thus less suited than our language for specifying the example policies. However, STREAM's performance is better than our tool's. Nevertheless, the performance of our prototype tool is still within the same order of magnitude as STREAM's performance and it is efficient enough for practical use.
section_name: Solution

section_content: Although aggregations have appeared previously in monitoring, our language is the first to add expressive SQL-like aggregation operators to a first-order temporal language. This enables us to express complex compliance policies with aggregations. Our prototype implementation is therefore the first tool to handle such policies, and it does so with acceptable performance.
section_name: Contributions

section_content: Our MFOTL extension is inspired by the aggregation operators in database query languages like SQL and by Hella et al. 's extension of first-order logic with aggregation operators [20]. Hella et al. 's work is theoretically motivated: they investigate the expressiveness of such an extension in a non-temporal setting. A minor difference between their aggregation operators and ours is that their operators yield terms rather than formulas, as in our extension. 

Monitoring algorithms for different variants of first-order temporal logics have been proposed by Hallé and Villemaire [19], Bauer at al. [10], and Basin et al. [8]. Except for the counting quantifier [10], none of them support aggregations. Bianculli et al. [11] present a policy language based on a first-order temporal logic with a restricted set of aggregation operators that can only be applied to atomic formulas. For monitoring, they require a fixed finite domain and provide a translation to a propositional temporal logic. Such a translation is not possible in our setting since variables range over an infinite domain. In the context of database triggers and integrity constraints, Sistla and Wolfson [24] describe an integration of aggregation operators into their monitoring algorithm for a first-order temporal logic. Their aggregation operators are different from those presented here in that they involve two formu-las that select the time points to be considered for aggregation and they use a database query to select the values to be aggregated from the selected time points. 

Other monitoring approaches that support aggregations are LarvaStat [14], LOLA [16], EAGLE [4], and an approach based on algebraic alternating automata [17]. These approaches allow one to aggregate over the events in system traces, where events are either propositions or parametrized propositions. They do not support grouping, which is needed to obtain statistics per group of events, e. g., the events generated by the same agent. Moreover, quantification over data elements and correlating data elements is more restrictive in these approaches than in a first-order setting. 

Most data stream management systems like STREAM [2] and Gigascope [15] handle SQL-like aggregation operators. For example, in STREAM's query language CQL [3] one selects events in a specified time range, relative to the current position in the stream, into a table that one aggregates. The temporal expressiveness of such languages is weaker than our language; in particular, linear-time temporal operators are not supported.
section_name: Related work

section_content: The remainder of the article is structured as follows. In Sect. 2, we extend MFOTL with aggregation operators. In Sect. 3, we present our monitoring algorithm, which we evaluate in Sect. 4. In Sect. 5, we draw conclusions.
section_name: Organization

section_name: MFOTL with aggregation operators

section_content: We use standard notation for sets and set operations. We also use set notation with sequences. For instance, for a set A and a sequence s = (s 1,. . ., s n ), we write A ∪ s for the union

We denote the empty multi-set by ∅. 

Given a domain D, an aggregation operator is a function from multi-sets with domain D to D ∪{⊥ ∞ } such that finite multi-sets are mapped to elements of D \{⊥ ∞ } and infinite multisets are mapped to ⊥ ∞. Common aggregations operators on finite non-empty multi-sets M that only contain rational numbers are: On the empty multi-set, the definition of the aggregations operators CNT and SUM is straightforward, namely, CNT(∅) := SUM(∅) := 0. However, the definition of the other aggregations operators MIN, MAX, and AVG on the empty multi-set is less standard. For example, the average over an empty multi-set is undefined. We can define AVG(∅) := ⊥, where ⊥ is a special domain element representing undefinedness. Analogously, we can define MIN(∅) and MAX(∅) as ⊥, or we can assume special domain elements ∞ and -∞ and define MIN(∅) and MAX(∅) as ∞ and -∞, respectively. Note that when ⊥, ∞, and -∞ are domain elements, one must extend the above definitions to finite, non-empty multi-sets that contain such elements. This can, for example, be done by ignoring such elements and their multiplicity. For readability, we omit a definition of these aggregation operators on such "ill-formed" multi-sets. These definitions are not relevant for the results of this article.
section_name: Preliminaries

section_content: A signature S is a tuple (F, R, ι), where F is a finite set of function symbols, R is a finite set of predicate symbols disjoint from F, and the function ι : F ∪ R → N assigns to each symbol s ∈ F ∪ R an arity ι(s). In the following, let S = (F, R, ι) be a signature and V a countably infinite set of variables, where

Function symbols of arity 0 are called constants. Let C ⊆ F be the set of constants of S. Terms over S are defined inductively: Constants and variables are terms, and f (t 1,. . ., t n ) is a term if t 1,. . ., t n are terms and f is a function symbol of arity n > 0. We denote by fv(t) the set of the variables that occur in the term t. We denote by T the set of all terms over S, and by T ∅ the set of ground terms, that is, terms without variables. A substitution θ is a function from variables to terms. We use the same symbol θ to denote its homomorphic extension to terms. 

Given a finite set Ω of aggregation operators, the MFOTL Ω formulas over the signature S are given by the grammar

where r, t and the t i s, I, and ω range over the elements in R, T, I, and Ω, respectively, x and y range over elements in V, and z and ḡ range over sequences of elements in V. Note that we overload notation: ω denotes both an aggregation operator and its corresponding symbol. This grammar extends MFOTL's grammar [21] in two ways. First, it introduces aggregation operators. Second, terms may also be built from function symbols and not just from variables and constants. For ease of exposition, we do not consider future-time temporal operators. 

We call [ω t z. ψ](y; ḡ) an aggregation formula. It is inspired by the homonymous relational algebra operator. Intuitively, by viewing variables as (relation) attributes, ḡ are the attributes on which grouping is performed, t is the term on which the aggregation operator ω is applied, and y is the attribute that stores the result. The variables in z are ψ's attributes that do not appear in the described relation. We define the semantics in Sect. 2. 3, where we also provide examples. 

The set of free variables of a formula ϕ, denoted fv(ϕ), is defined as expected for the standard logic connectives. For an aggregation formula, it is defined as fv [ω t z. ϕ](y; ḡ) := {y} ∪ ḡ. A variable is bound if it is not free. We denote by f v(ϕ) the sequence of free variables of a formula ϕ that is obtained by ordering the free variables of ϕ by their occurrence when reading the formula from left to right. A formula is well-formed if, for each of its subformulas [ω t z. ψ](y; ḡ), it holds that (a) y ∈ ḡ, (b) fv(t) ⊆ fv(ψ), (c) the elements of z and ḡ are pairwise distinct, and (d) z = fv(ψ) \ ḡ. Note that, given condition (d), the use of one of the sequences z and ḡ is redundant. However, we use this syntax to make the free and bound variables explicit in aggregation formulas. Throughout this article, we consider only well-formed formulas. 

To omit parentheses, we assume that Boolean connectives bind stronger than temporal connectives, and unary connectives bind stronger than binary ones, except for the quantifiers, which bind weaker than Boolean ones. As syntactic sugar, we use standard Boolean connectives such as ϕ ∧ ψ := ¬(¬ϕ ∨ ¬ψ), the universal quantifier ∀x. ϕ := ¬∃x. ¬ϕ, and the temporal operators ϕT I ψ := ¬(¬ϕS I ¬ψ), I ϕ := t S I ϕ, and I ϕ := f T I ϕ, where I ∈ I, t := p ∨ ¬p, and f := ¬t, for some predicate symbol p of arity 0, assuming without loss of generality that R contains such a symbol. Non-metric variants of the temporal operators are easily defined, for example, ϕ := [0,∞) ϕ.
section_name: Syntax

section_content: We distinguish between predicate symbols whose corresponding relations are rigid over time and those that are flexible, i. e., their interpretations can change over time. We denote by R r and R f the sets of rigid and flexible predicate symbols, where R = R r ∪R f with R r ∩R f = ∅. We assume that R r contains the binary predicate symbols ≈ and ≺, which have their expected interpretation, namely, equality and ordering. 

A structure D over the signature S consists of a domain D = ∅ and interpretations r ), for each f ∈ F and r ∈ R. A temporal structure over the signature S is a pair ( D, τ ), where D = (D 0, D 1,. . . ) is a sequence of structures over S and τ = (τ 0, τ 1,. . . ) is a sequence of non-negative integers with the following properties. 

1. The sequence τ is monotonically increasing, that is, τ i ≤ τ i+1, for all i ≥ 0. Moreover, τ makes progress, that is, for every τ ∈ N, there is some index i ≥ 0 such that τ i > τ. 2. All structures D i, with i ≥ 0, have the same domain, denoted D. 3. Function symbols and rigid predicate symbols have rigid interpretations, that is,

, for all f ∈ F, p ∈ R r, and i ≥ 0. We also write f D and p D for f D i and p D i, respectively. 

We call the elements in the sequence τ timestamps and the indices of the elements in the sequences D and τ time points. 

A valuation is a mapping v : V → D. For a valuation v, a variable sequence x = (x 1,. . ., x n ) ∈ V n, and d = (d 1,. . ., d n ) ∈ D n, we write v[ x → d] for the valuation that maps x i to d i, for 1 ≤ i ≤ n, and the other variables' valuation is unaltered. We abuse notation by also applying a valuation v to terms. That is, given a structure D, we extend v homomorphically to terms. 

For the remainder of the article, we fix a countable domain D that contains the rational numbers Q and elements like ⊥ ∞ and ⊥. We only consider a single-sorted logic. One could alternatively have sorts for the different types of elements like data elements and the aggregations. Furthermore, we assume that function symbols are always interpreted by total functions. Partial functions like division over scalar domains can be extended to total functions, e. g., by mapping elements outside the function's domain to ⊥. Since the treatment of partial functions is not essential to our work, we treat ⊥ as any other element of D. Alternative treatments are possible, for example based on multi-valued logics [22]. Definition 1 Let ( D, τ ) be a temporal structure over the signature S, with D = (D 0, D 1,. . . ) and τ = (τ 0, τ 1,. . . ), ϕ a formula over S, v a valuation, and i ∈ N. We define the relation

Note that the semantics for the aggregation formula is independent of the order of the variables in the sequence z. 

For a temporal structure ( D, τ ), a time point i ∈ N, a formula ϕ, a valuation v, and a sequence z of variables with z ⊆ fv(ϕ), we define the set

We drop the superscript when it is clear from the context. We drop the subscript when z = f v(ϕ). In this case the valuation v is irrelevant and [[ϕ]] ( D, τ,i) denotes the set of satisfying elements of ϕ at time point i in ( D, τ ). 

With this notation, we illustrate the semantics for aggregation formulas in the case where we aggregate over a variable. We use the same notation as in Definition 1. In particular, consider a formula ϕ = [ω x z. ψ](y; ḡ), with x ∈ V, and a valuation v. Note that v (and thus also v[z → d]) fixes the values of the variables in ḡ because these are free in ϕ. The multi-set M is as follows. 

Example 2 Let ( D, τ ) be a temporal structure over a signature with a ternary predicate symbol p, with p D 0 = {(1, b, a), (2, b, a), (1, c, a), (4, c, b)}. Moreover, let ϕ be the formula [SUM x x, y. p(x, y, g)](s; g) and z = (x, y). At time point 0, for a valuation If we group on the variable x instead of g, we get [[[SUM x y, g. p(x, y, g)](s; x)]] = {(2, 1), (2, 2), (4, 4)}, and [[[SUM x x, y, g. p(x, y, g)](s)]] = {(8)}, if we do not group on any variable. Finally, note that if the multi-set over which we aggregate is infinite, the aggregated value is ⊥ ∞. For example, we have

Example 3 This example illustrates the special case where aggregation operators are applied on formulas that have no satisfying elements. Let ( D, τ ) be a temporal structure over a signature with a binary predicate symbol q, with q D 0 = ∅. We have [[[ω x x. q(x, y)](s; y)]] = ∅, for any aggregation operator ω, while

The issue with the definition of aggregation operators on empty multi-sets, illustrated by Example 3, also appears in SQL. There, aggregation operators return the special domain element NULL on empty multi-sets. 

Example 4 Consider the formula ϕ = [SUM a a. ψ](s; u), where ψ is the formula [0,31) withdraw(u, a). Let ( D, τ ) be a temporal structure with the relations withdraw D 0 = {(Bob, 9), (Bob, 3)} and withdraw D 1 = {(Bob, 3)}, and the timestamps τ 0 = 5 and τ 1 = 8. We have that

Our semantics ignores the fact that the tuple (Bob, 3) occurs at both time points 0 and 1. Note that the withdraw events do not have unique identifiers in this example. 

To account for multiple occurrences of an event, we can attach to each event additional information to make it unique. For example, assume we have a predicate symbol ts at hand that records the timestamp at each time point, i. e., ts 3, 5), (Bob, 3, 8)}. To further distinguish between withdraw events at time points with equal timestamps, we would need additional information about the occurrence of an event, for example information obtained from a predicate symbol tpts that is interpreted as

The multiplicity issue illustrated by Example 4 also appears in databases. SQL is based on a multi-set semantics and one uses the DISTINCT keyword to switch to a set-based semantics. However, it is problematic to define a multi-set semantics for first-order logic that associates a tuple d ∈ D |fv(ϕ)| with a multiplicity denoting how often d satisfies the formula ϕ rather than a Boolean value. For instance, there are several ways to define a multi-set semantics for disjunction: the multiplicity of d for ψ ∨ ψ can be either the maximum or the sum of the multiplicities of d for ψ and ψ. Depending on the choice, standard logical laws become invalid, for example the distributivity of existential quantification or conjunction over disjunction. Defining a multi-set semantics for negation is even more problematic.
section_name: Semantics

section_content: In this section, we present our monitoring algorithm for MFOTL Ω. The algorithm is inspired by those in [8, 9, 12] and it is based on formulating the evaluation of formulas ϕ in a fragment 123 Fig. 2 The derivation rules defining the fragment F of monitorable formulas of MFOTL Ω in terms of extended relational algebra operators applied to the evaluation of the direct subformulas of ϕ. We start with an overview of our monitoring approach. 

We assume that policies are of the form ∀ x. ϕ, where ϕ is an MFOTL Ω formula and x is the sequence of ϕ's free variables. The policy requires that ∀ x. ϕ holds at every time point in the temporal structure ( D, τ ). In the following, we assume that ( D, τ ) is a temporal database, i. e., (1) the domain D is countably infinite, (2) the relation p D i is finite, for each p ∈ R f and i ∈ N, (3) p D is a recursive relation, for each p ∈ R r, and (4) f D is computable, for each f ∈ F. We also assume that the aggregation operators in Ω are computable functions on finite multi-sets. 

The inputs of our monitoring algorithm are a formula ψ, which is logically equivalent to ¬ϕ, and a temporal database ( D, τ ), which is processed iteratively. The algorithm outputs, again iteratively, the relation [[ψ]] ( D, τ,i), for each i ≥ 0. As ψ and ¬ϕ are equivalent, the tuples in [[ψ]] ( D, τ,i) are the policy violations at time point i. Note that we drop the outermost quantifier as we are interested not only in whether the policy is violated. An instantiation of the free variables x that satisfies ψ provides additional information about the violations.
section_name: Monitoring algorithm

section_content: Not all formulas are effectively monitorable. Consider, for example, the policy formalization ∀x. ∀y. p(x) → q(x, y), with the formula ψ = p(x)∧¬q(x, y) that we use for monitoring. There are infinitely many violations for time points i with p

) is infinite and its elements cannot be enumerated in finite time. We define a fragment of MFOTL Ω that guarantees finiteness. Furthermore, the set of violations at each time point can be effectively computed bottom-up over the formula structure. In the following, we treat the Boolean connective ∧ and the temporal operator T I as primitives.
section_name: Monitorable fragment

section_content: The set F of monitorable formulas with respect to (H p ) p∈R r is defined by the rules given in Fig. 2, where H p ⊆ {1,. . ., ι(p)}, for each p ∈ R r. 

Let be a label of a rule from Fig. 2. We say that a formula ϕ ∈ F is of kind if there is a derivation tree for ϕ having as its root a rule labeled by. 

Before describing some of the rules, we first explain the meaning of the set H p, for p ∈ R r with arity k. The set H p contains the indexes j for which we can determine the values of the variable x j that satisfy p(x 1,. . ., x k ), given that the values of the variables x i with i = j are fixed. Formally, given a temporal database ( D, τ ) and a rigid predicate symbol p of arity k > 0, we say that an index j, with 1 ≤ j ≤ k, is effective for p if for any ā ∈ D k-1, the set {d ∈ D | (a 1,. . ., a j-1, d, a j,. . ., a k-1 ) ∈ p D} is finite. For instance, for the rigid predicate ≈, the set of effective indexes is H ≈ = {1, 2}. Similarly, for the rigid predicate ≺ N, defined as a ≺ N b iff a, b ∈ N and a < b, we have H ≺ N := {1}. 

We describe the intuition behind the first four rules in Fig. 2. The meaning of the other rules should then be obvious. The first rule (FLX) requires that in an atomic formula p(t 1,. . ., t ι( p) ) with p ∈ R f, the terms t i are pairwise distinct variables. This formula is monitorable since we assume that p's interpretation is always a finite relation. For the rules (RIG ∧ ) and (RIG ∧¬ ), consider formulas of the form ϕ ∧ p(t 1,. . ., t ι( p) ) and ϕ ∧ ¬ p(t 1,. . ., t ι( p) ) with p ∈ R r and ι( p) i=1 fv(t i ) ⊆ fv(ϕ). In both cases, the second conjunct further restricts the satisfying tuples of ϕ. An example is the formula ϕ(x, y) ∧ x + 1 ≈ y. If ϕ is monitorable, the conjunction is also monitorable as it can be evaluated by removing from [[ϕ]] the tuples that do not satisfy the second conjunct x + 1 ≈ y. The rule (RIG ∧ ) treats the case where one of the terms t i is a variable that does not appear in ϕ. We require here that the index j is effective, so that the values of this variable are determined by the values of the other variables, which themselves are given by the tuples in [[ϕ] ]. An example is the formula p(x, y) ∧ z ≈ x + y. The required conditions on t j are necessary. If j is not effective, then we cannot guarantee finiteness. Consider, for example, the formula q(x) ∧ x ≺ y. If we do not require that t j is a variable, then we would have to solve equations to determine the value of the variable that does not occur in ϕ. Consider, for example, the formula q(x) ∧ x ≈ y • y. 

The rule (FLX) may seem quite restrictive. However, one can often rewrite a formula of the form p(t 1,. . ., t n ) with p ∈ R f into an equivalent formula in F. For instance, p(x +1, x) can be rewritten to ∃y. p(y, x) ∧ x + 1 ≈ y. Alternatively, one can add additional rules that handle such cases directly. 

The following lemma shows that ϕ's membership in F guarantees the finiteness of [[ϕ] ]. The proof consists of a straightforward induction on the formula structure. 

Lemma 6 Let ( D, τ ) be a temporal database, i ∈ N a time point, ϕ a formula, and H p the set of effective indexes for p, for each p ∈ R r. If ϕ is a monitorable formula with respect to

There are formulas like (x ≈ y)S p(x, y) that describe finite relations but are not in F. Finiteness can also be guaranteed by semantic notions like domain independence or syntactic notions like range restriction, see, for example, [1] and also [8, 13] for a generalization of these notions to a temporal setting. If we restrict ourselves to MFOTL without future operators, the range restricted fragment in [8] is more general than the fragment F. This is because, in contrast to the rules in Fig. 2, range restrictions are not local conditions, that is, conditions that only relate formulas with their direct subformulas. However, the evaluation procedures in [1, 8, 13] also work in a bottom-up recursive manner. So one still must rewrite the formulas to evaluate them bottom-up. No rewriting is needed for formulas in F. Furthermore, the fragment ensures that aggregation operators are always applied to finite multi-sets. Thus, for any ϕ ∈ F, the element ⊥ ∞ ∈ D never appears in a tuple of
section_name: Definition 5

section_content: Our monitoring algorithm is based on interpreting MFOTL Ω connectives in terms of extended relational algebra operators. This interpretation is represented by equalities between the evaluation of a formula and the evaluation of its direct subformulas, for each kind of formula defined in Sect. 3. 1. Such equalities extend the standard ones [1] that express the relationship between first-order logic (without function symbols) and relational algebra, to function symbols, temporal operators, and group-by operators. Before presenting the equalities, we introduce the extended relational algebra operators.
section_name: MFOTL Ω and extended relational algebra operators

section_content: We start by defining constraints. We assume a given infinite set of variables Z = {z 1, z 2,. . . } ⊆ V, ordered by their indices. A constraint is a formula r (t 1,. . ., t n ) or its negation, where r is a rigid predicate symbol of arity n and the t i s are constraint terms, i. e., terms with variables in Z. We assume that for each domain element d ∈ D, there is a corresponding constant, also denoted by d. A tuple (a 1,. . ., a k ) satisfies the constraint

, where v is a valuation with v(z i ) = a i, for all i ∈ {1,. . ., k}. Satisfaction of a constraint ¬r (t 1,. . ., t n ) is defined similarly. 

In the following, let C be a set of constraints, A ⊆ D m, and B ⊆ D n. The selection of A with respect to C is the m-ary relation

Let s be a sequence of columns in A × B. The join and the antijoin of A and B with respect to s and C are defined as

and

Let ω be an operator in Ω, G a set of k ≥ 0 columns in A, and t a constraint term. 

The ω-aggregate of A on t with grouping by G is the (k + 1)-ary relation

Here ḡ = (g 1, g 2,. . ., g k ) is the maximal subsequence of (1, 2,. . ., m) such that g i ∈ G, for 1 ≤ i ≤ k, and M ā : D m-k → N is the finite multi-set

where h is the maximal subsequence of (1, 2,. . ., m) with no element in G and
section_name: Extended relational algebra operators

section_content: Let ( D, τ ) be a temporal database, i ∈ N, and ϕ ∈ F. We express [[ϕ]] ( D, τ,i) in terms of the generalized relational algebra operators. The following equalities follow directly from the semantics of MFOTL Ω formulas and the definition of the extended relational algebra operators. 

Kind (FLX). This case is straightforward. For a predicate symbol p ∈ R f of arity n and pairwise distinct variables x 1,. . .,

Kinds Then

and

where the substitution θ :

Kind (RIG ∧ ). Let ψ ∧ p(t 1,. . ., t n ) be a formula of kind (RIG ∧ ), with f v(ψ) = (y 1,. . ., y ). 

Then

For instance, let ϕ(x, y, z) = ψ(y, z)∧x ≺ y +z. Assume that

Kinds (GEN ∧ ) and (GEN ∧¬ ). Let ψ ∧ ψ and ψ ∧ ¬ψ be formulas of kind (GEN ∧ ) and respectively

and

where (a) s = (1,. . ., n, n + i 1,. . ., n + i ) with i j such that (i 1,. . ., i ) is the maximal subsequence of (1,. . ., ) with y i j / ∈ fv(ψ), and (b) C = {z j ≈ z n+h | y j = y h, 1 ≤ j ≤ n, and 1 ≤ h ≤ }. For instance, if ϕ = p(x, y) ∧ q(y, z) then s = (1, 2, 4) and

123 Kind (GEN ∃ ). Let ∃x. ψ be a formula of kind (GEN ∃ ) with f v(ψ) = (y 1,. . ., y k ). Then

where j = (1,. . ., k) if x ∈ fv(ψ) and otherwise j = (1,. . ., j -1, j + 1,. . ., k) with j such that x = y j. 

Kind (GEN ). Let I ψ be a formula of kind (GEN ). Then

Kinds (GEN S ) and (GEN ¬S ). Let ψS I ψ and ¬ψS I ψ be two formulas of kind (GEN S ) and respectively (GEN ¬S ), with f v(ψ) = (y 1,. . ., y n ) and f v(ψ ) = (y 1,. . ., y ). Then

and

where s and C are as for the case of kinds (GEN ∧ ) and (GEN ∧¬ ). For instance, for f v(ψ) = (x, y, z) and f v(ψ ) = (z, z, x), we have s = (1, 2, 3, 5) and C = {z 1 ≈ z 6, z 3 ≈ z 4 }.
section_name: Interpreting MFOTL Ω connectives as extended regular algebra operators

section_content: Then

where s and C are as for the case of kinds (GEN ∧ ) and (GEN ∧¬ ). This equality follows the semantics of the T operator, that is, ( D, τ, v, i) | ψT I ψ iff ( D, τ, v, j) | ψ for all j with j ≤ i and τ i -τ j ∈ I, or there is a j with j ≤ i and τ i -

where f v(ψ) = (y 1,. . ., y n ), for some n ≥ 0, G = {i | y i ∈ ḡ}, and the substitution θ : fv(ψ) → {z 1,. . ., z n } is given by θ(x) = z j, where j is the index of x in f v(ψ). For instance, for [SUM x+y x, y. p(x, y, z)](s; z), we have G = {3} and θ(t) = z 1 + z 2. 

Remark We do not have a translation from formulas in F into extended relational algebra expressions because one cannot fix in advance the relational symbols used by such expressions. Indeed, the right-hand side of the equalities for the kind (RIG ∧ ) and the kinds corresponding to temporal operators depend not only on the left-hand side formula, but also on the temporal database. 

Fig. 3 The init and eval procedures
section_name: Kinds (GEN T ). Let ψT I ψ be a formula of kind (GEN T ).

section_content: For a given formula ψ ∈ F, the algorithm iteratively processes the given temporal database ( D, τ ). At each time point i, it calls the procedure eval to compute [[ψ]] ( D, τ,i). The input of eval at time point i is the formula ψ, the time point i with its timestamp τ i, and the interpretations of the flexible predicate symbols, i. e., r D i, for each r ∈ R f. Note that D's domain and the interpretations of the rigid predicate symbols and the function symbols, including the constants, do not change over time. We assume that they are fixed in advance. The computation of [[ψ]] ( D, τ,i) is by recursion over ψ's formula structure. To accelerate the computation of [[ψ]] ( D, τ,i), the monitoring algorithm maintains state for each temporal subformula, storing previously computed intermediate results. The monitor's state is initialized by the procedure init and updated in each iteration by the procedure eval. We describe the algorithm's state for each temporal operator when we present the pseudo-code that handles the operator. 

The pseudo-code of the procedures init and eval is given in Fig. 3. Our pseudo-code (also used in the Figs. 4 and 5 ) is written in a functional-programming style with pattern matching. The symbol denotes the empty sequence, + + sequence concatenation, h::L the sequence with head h and tail L, and λx. f (x) denotes a function f. The functions hd(L) and tl(L) return the head and respectively the tail of the non-empty list L.
section_name: Algorithmic realization

section_content: We now describe the eval procedure in more detail. The cases correspond to the rules defining the set of monitorable formulas. The pseudo-code for the cases corresponding to non-temporal Fig. 4 The eval_since procedure Fig. 5 The eval_palways procedure connectives follows closely the equalities given in Sect. 3. 2. 2. Note that extended relational algebra operators have standard, efficient implementations [18], which can be used to evaluate the expressions on the right-hand side of these equalities. 

The predicates kind_rig and kind_rig' check whether the input formula ϕ is indeed of the intended kind. The get_info_* procedures return the parameters used by the corresponding relational algebra operators. For instance, get_info_rig returns the singleton set consisting of the constraint corresponding to the restrictions p(t 1,. . ., t ι( p) ) or ¬ p(t 1,. . ., t ι( p) ). Similarly, get_info_rig' returns the effective index corresponding to the unique variable that appears only in the right conjunct of ϕ. The procedure reval( p, k, ā) returns the set {d ∈ D | (a 1,. . ., a k-1, d, a k,. . ., a n-1 ) ∈ p D}, for any ā ∈ D n-1, where n is the arity of the rigid predicate symbol p.
section_name: First-order connectives

section_content: Computing the aggregation ω H t (A) is standard [18]. Namely, one iterates through the tuples in the relation A and maintains a data structure that associates an accumulated value for the aggregation term t to each group of A, that is, to each tuple of values for the aggregation attributes in H. The accumulation depends on the aggregation operator. For instance, for CNT, it is the number of tuples of A seen so far that belong to the group, for SUM, it is the sum of values for t corresponding to such tuples, and for AVG it is the pair of the values used for CNT and SUM. The accumulated values are updated at each iteration. For instance, for CNT, the accumulated value is increased by one. When A's scan is finished, the aggregated value for each group is obtained from the accumulated value. Suitable data structures are hash tables and balanced search trees as they allow for fast lookups and updates. 

Finally, note that when handling an aggregation operator, one only needs a suitable accumulation, functions for initializing and updating this accumulation, and a function f for obtaining the aggregated value from the accumulated value. In the general case, the accumulation consists of all the values for t seen so far and the function f is the aggregation operator itself. For many aggregation operators, for instance for the ones in considered in this article, the computation of the accumulated value can be carried out more efficiently.
section_name: Aggregation operators

section_content: Consider first the case where the formula ϕ is of the form I ψ. In this case, the state stores between the iterations i -1 and i, when i > 0, the timestamp of the last time point, namely τ ϕ := τ i-1, and the tuples that satisfy ψ at last time point i -1, i. e., the relation, τ,i-1). To evaluate ϕ at the current time point i, we recursively evaluate the subformula ψ at i, we update the state, and we return the relation resulting from the evaluation of ψ at the previous time point, provided that the temporal constraint is satisfied. Otherwise we return the empty relation. Note that by storing the relation [[ψ]] ( D, τ,i) at time point i, the subformula ψ need not be evaluated again at time point i during the evaluation of ψ at time point i + 1. 

Consider now the case where the formula ϕ is of the form ψS I ψ or ¬ψS I ψ, where I = [a, b), for some a ∈ N and b ∈ N ∪ {∞}. This case is mainly handled by the subprocedure eval_since, given in Fig. 4. For clarity of presentation, we assume that ϕ = ψS I ψ, the other case being similar. The evaluation of ϕ reflects the logical equivalence ψS I ψ ≡ d∈I ψS [d,d] ψ. Note that we abuse notation here, as the right-hand side is not a formula when b = ∞. The function interval_right_margin(ϕ) returns b. 

The state at time point i, that is, after the procedure eval(ϕ, i, τ i, Γ i ) has been executed, consists of the list L ϕ of tuples (τ j, R i j ) ordered with j ascending, where j is such that j ≤ i and τ i -τ j < b and with

with s and C defined as in Sect. 3. 2. 2. We have

The computation of this union is performed in the last line of the eval_since procedure. Note that, in general, not all the relations R i j in the list L ϕ are needed for the evaluation of ϕ at time point i. However, the relations R i j with j such that τ i -τ j ∈ I, that is τ i -τ j < a, are stored for the evaluation of ϕ at future time points i > i. By storing these relations, the subformulas ψ 1 and ψ 2 need not be evaluated again at time points j < i during the evaluation of ψ at time point i. 

We now explain how the state is updated at time point i from the state at time point i -1. We first drop from the list L ϕ the tuples that are no longer relevant. More precisely, we drop the tuples that have as their first component a timestamp τ j for which the distance to the current timestamp τ i is too large with respect to the right margin of I. This is done by the procedure drop_old. Next, the state is updated using the logical equivalence αSβ ≡ (α ∧ (αSβ)) ∨ β. This is accomplished in two steps. First, we update each element of L ϕ so that the tuples in the stored relations also satisfy ψ at the current time point i. This step corresponds to the conjunction in the above equivalence and it is performed by the map function. The update is based on the equality, τ,i). Note that the join distributes over the intersection. The second step, which corresponds to the disjunction in the above equivalence, consists of appending the tuple, τ,i). 

Finally, we consider the case where the formula ϕ is of the form ψT I ψ. The pseudocode for this case in the eval procedure reflects the logical equivalence ψT I ψ ≡ ( I ψ ) ∨ (ψ S I ψ ∧ ψ ). This case is mainly handled by the procedures eval_palways and eval_since', which correspond to the left-hand and respectively the right-hand side of the union operator of the right-hand side of the equality given in Sect. 3. 2. 2. The pseudo-code of the eval_since' procedure is similar to that of the eval_since procedure, and thus omitted. The only difference consists in replacing the assignment

The list L ϕ, which is part of the state maintained for ϕ, has the same meaning as for the case of the S I operator. Note also that the order of the parameters in the call to eval_since' is reversed in comparison to eval_since; this matches the previously given equivalence. The pseudo-code of the eval_palways is given in Fig. 5 and it represents the evaluation of formulas of the form I ψ ("always in the past ψ "). This procedure uses and maintains the other part of the state for ϕ, namely the list H ϕ. At time point i, after the procedure eval(ϕ, i, τ i, Γ i ) has been executed, the list H ϕ consists of the tuples (τ j, [[ψ ]] ( D, τ, j) ) with j ≤ i and τ i -τ j ∈ I, ordered with j ascending. The list H ϕ is updated at each iteration by eliminating old tuples using the same procedure drop_old as in the S I case, and by appending the tuple, τ,i) ). The procedure eval_palways returns the intersection on the left-hand side of the union operator of the equality for the T I operator. As in the S I case, this intersection is computed by calling the standard fold_left function on the list H ϕ, this time using the auxiliary procedure aux_palways. 

The following theorem states the correctness of our algorithm. Its proof follows the algorithm's presentation, and it proceeds by induction using the lexicographic ordering on tuples (i, |ϕ|), where i ∈ N and |ϕ| denotes ϕ's size, defined as expected. 

Theorem 7 Let ( D, τ ) be a temporal database, i ∈ N, and ψ ∈ F. The procedure eval(ψ, i, τ i, Γ i ) returns the relation [[ψ]] ( D, τ,i), whenever init(ψ ), eval(ψ, 0, τ 0, Γ 0 ),. . ., eval(ψ, i -1, τ i-1, Γ i-1 ) were called previously in this order, where Γ j = ( p D j ) p∈R f is the family of interpretations of flexible predicates at j, for every time point j ∈ N.
section_name: Temporal operators

section_content: Several optimizations are possible when evaluating formulas, in particular those formulas of the form ψ 1 S I ψ 2 and ψ 1 T I ψ 2. For instance, when I = [0, ∞), for the S I operator, it is sufficient to store the resulting relation from the previous time point as we have, τ,i). Further optimizations for incrementally updating the relations of the temporal formulas are described in [8]. 

We also present an optimization for the frequently occurring pattern [ω x z. I ψ](y; ḡ). Instead of applying the aggregation operator to the relation for the formula I ψ, we directly compute the aggregation from the relations for the formula ψ at the time points in the specified time window. The approach is an adaptation of the one for handling stand-alone aggregation operators, where one maintains a map between groups and accumulated values. For [ω x z. I ψ](y; ḡ), this map is not re-built from scratch at each time point; instead, it is stored and updated at each time point. In addition to a function for updating accumulations when tuples "enter" the relation for I ψ, we also use a function to update accumulations when tuples "leave" this relation. For instance, for CNT, one decreases the accumulated value by 1. By using a multi-set for storing the relation for I ψ, we can efficiently determine when a tuple enters and when it leaves this relation.
section_name: Optimizations

section_content: In this section, we evaluate our extension of metric first-order temporal logic with aggregation operators. First, we evaluate whether MFOTL Ω is a suitable language for expressing complex policies with aggregations. Second, we evaluate the performance of our prototype monitor, comparing it with the stream-processing tool STREAM [2] and the relational database PostgreSQL [23]. In contrast to existing logic-based monitoring solutions, both of these tools support the aggregation of data values and their performance is comparable to other state-of-the-art tools in their respective domains.
section_name: Evaluation

section_content: To evaluate MFOTL Ω 's suitability for specifying policies with aggregations, we compare specifications in MFOTL Ω with those in the prominent query languages CQL [3] (STREAM's query language) and SQL. For the comparison, we use the following six policies rooted in the domain of fraud detection. 

1. The sum of withdrawals of each user in the last 31 days does not exceed the limit of $10,000. 2. Similar to the first policy, except that the withdrawals must not exceed $10,000 only when the flag for checking the limit is set. 3. Similar to the second policy, except that the withdrawal limit is set by the user. 4. The maximal withdrawal of each user in the last week must be at most twice the average of the user's withdrawals over the last 91 days. 5. The average number of withdrawals per user in the last 31 days must not exceed a given threshold of 150, where the average is taken over all users. 6. For each user, the number of withdrawal peaks in the last 31 days does not exceed a threshold of 5, where a withdrawal peak is a value at least twice the average over the last 31 days. 

The MFOTL Ω formulas that formalize the given policies are presented in Fig. 6. Note that since we restrict ourselves in this article to the past-only fragment of MFOTL Ω, the outermost temporal operator ("always") is not part of our definition of the logic given in Sect. 2. However, we include it in our formalizations to emphasize that policies must be fulfilled at all time points. We use withdraw(u, a) to denote that the user u has withdrawn the amount a and ts(τ ) to denote the timestamp τ of a time point. 

In the MFOTL Ω formalization of the first policy, the SUM operator adds all the withdrawal amounts in the past 31 days, and we require that the result is less than 10,000. We use ts(τ ) to differentiate the different withdrawals of the same amount made by the user within a given time window (see Example 4). The formalization of the second policy is a simple extension of the first, where we just add the condition that a user's limit is set. We use limit_on(u) to denote that a user u sets the limit flag and limit_off (u) to denote that u unsets it. Using the temporal operator S, we express the existence of a time point in the past where the user has set the limit flag and has not unset it since then. To formalize the third policy, we use limit(u, ) to represent that u sets his limit to. To simulate setting no limit, a user can set an arbitrarily high limit, and we assume that when a new account is opened, the limit is set to some default value. The S operator is now used to find the latest limit that has been set by the user. This limit is then used to constrain the sum of all withdrawals. 

For the fourth policy, AVG computes the average withdrawal amount over the last 91 days and MAX finds the maximum withdrawal amount for the last week. We require that the maximum is at most double the average. For the fifth policy, we first use CNT to count the number of withdrawals made over last 31 days by each user. We then use AVG to compute the average number of withdrawals per user during this time period, which we require not to exceed 150. Finally for the sixth policy, we use AVG to compute the average withdrawal over the last 31 days for each user. The CNT operator then counts all withdrawals with amounts greater than twice the calculated average. We require that the count is not greater than 5. 

Before we compare MFOTL Ω with SQL and CQL, we remark that the given MFOTL Ω formalizations follow the common pattern ∀ x. ∀ ȳ. ϕ( x, ȳ) ∧ c( x, ȳ) → ψ( ȳ) ∧ c ( ȳ), where c and c represent restrictions, i. e., formulas of the form r (t) and ¬r (t) with r ∈ R r. The formula to be monitored, i. e., ϕ( x, ȳ) ∧ c( x, ȳ) ∧ ¬(ψ( ȳ) ∧ c ( ȳ)) is in the fragment F if ϕ and ψ are in F, and both c and c satisfy the conditions of the (RIG) rules. See Fig. 2 in Sect. 3. 1. It can be easily checked that this is indeed the case for the given formulas (P1) to (P6) and we can thus use our monitoring solution for them.
section_name: Specification language

section_content: SQL does not have temporal operators, and thus all temporal reasoning must be explicitly specified. This can be done by adapting the standard embedding of temporal logic into firstorder logic to represent MFOTL Ω formulas as SQL queries. The key ideas underlying the embedding are the following. First, we add to each predicate two additional attributes, tp and ts, which represent the time point and the timestamp of an event's occurrence. Second, we use the tpts predicate from Example 4, with two attributes, tp and ts, whose interpretation consists of all pairs of time points and associated timestamps. Finally, we express temporal constraints by arithmetic expressions over the newly introduced temporal data, that is, the data values for the tp and ts attributes. The tpts predicate is needed to preserve the semantic equivalence between MFOTL Ω and its embedding in first-order logic, as there can be time points at which no event occurs. Expressing first-order formulas with aggregations as extended relational algebra expressions is done in a standard way [1]. 

To illustrate this approach, consider the following SQL query for reporting violations with respect to the first policy (P1). A drawback of using SQL is that the queries are less succinct because they must explicitly account for temporal constraints within policies. Therefore, without an automated translation from MFOTL Ω to SQL, queries for complex policies are difficult to specify and maintain. Moreover, and regardless of whether an automated translation is used, queries are hard to simplify and optimize. This is not just due to the query's complexity, the structure is also lost: since there is no distinction between temporal data and other data, an SQL engine cannot exploit the policy's temporal dimension to optimize the query's execution. Our performance evaluation in Sect. 4. 2 illustrates this point.
section_name: Comparison with SQL

section_content: STREAM's query language CQL for data streams extends SQL with the sliding window construct. This construct takes as input a stream of timestamped events and a range. For each event in the stream, it outputs a relation that contains the current event and all the preceding events that fall within the given range. CQL's time model differs from MFOTL Ω 's and thus the meaning of range in CQL and MFOTL Ω do not match. In CQL, there is no notion of time points and the sliding window evaluation is applied after each received event. 

To illustrate the sliding window construct, consider the following CQL query, which returns all the violations of the first policy (P1). Here, the sliding window construct, syntactically denoted with the [. . . ] expression, is applied over the withdraw stream. That is, for each event e with timestamp τ, a relation is created that contains e and all the events that happened between τ and τ -31 days. Finally, both SELECT queries are evaluated using the standard SQL semantics. The CQL's sliding windows construct roughly corresponds to the I operator in MFOTL Ω, where I is of the form [0, t) with t ∈ N ∪ {∞}. All other MFOTL Ω operators must be implicitly encoded. To illustrate, consider the following CQL query to find violations of the second policy (P2). To mimic the semantics of the S operator, we first count the number of limit_on and limit_off events for each user and produce the corresponding cnt_on and cnt_off relations. 

The [RANGE Unbounded] sliding window ranges over the entire stream up to the currently processed position. Second, we create the limit_is_on stream, which contains the users u that have the limit turned on at the current timestamp. The limit is turned on for user u if there are as many limit_on events as limit_off events. We assume here that, for each user, the limit is initially turned off and that the limit_on and limit_off events alternate. Finally, for each (s, u) tuple in sum_rel, we check whether u has turned his limit on at the current timestamp and, if so, whether s is greater than 10,000. The previous workaround for policy (P2) does not apply to policy (P3). Here we must find the latest limit set for each user, and this is not possible without directly accessing the timestamps of events. Thus, to express the policy (P3) in CQL, we assume that events in the limit stream are tuples of the form (τ, u, ) timestamped by τ, in contrast to withdraw events which are tuples of the form (u, a). We encode the MFOTL Ω subformula ¬∃. limit(u, ) S limit(u, ) with an SQL query that uses the timestamp field explicitly, in a manner similar to the approach used to express temporal operators in SQL. This encoding can be generalized and used for any MFOTL Ω temporal operator. However, it has similar drawbacks to using SQL, as seen by STREAM's performance on (P3). 

Temporal reasoning using only the sliding window in STREAM is limited in general. For example, we cannot check that certain event patterns happen at every time point in a given time window, whereas in MFOTL Ω we can simply use the I operator. Moreover, we cannot select tuples from a time window that is strictly in the past. It is therefore in general not clear how to specify in CQL temporal constraints of the form ϕS I ψ, with 0 / ∈ I. To illustrate the first limitation, consider the following policy. If during the past week a user's acount balance is continually negative, that is, the amount withdrawn exceeds the amount deposited at each time point during the week, then the user must not withdraw more money from his account. In MFOTL Ω, this policy is formalized by the following formula, where deposit(u, a) has the expected meaning. The following policy illustrates the second limitation. If a user makes a withdrawal larger than $1,000, then he must not have been in-debt during the last seven days. In MFOTL Ω, this policy is formalized by the formula ∀u. ∃a. withdraw(u, a) ∧ a 1000 → ¬indebt(u)S [8,∞) outdebt(u), where we assume that the time points when the user u goes into debt and out of debt are marked by indebt(u) and outdebt(u), respectively. The subformula ¬indebt(u)S [8,∞) outdebt(u) holds when the last outdebt event for the user u happened more than 7 days ago and no indebt event for u has happened since then. Here we assume that each user is initially not in debt, and this is marked with a corresponding outdebt event. 

In summary, the sliding window operator is restrictive, even in CQL's simple underlying time model, namely, a stream of timestamped events. Since the sliding window operator is CQL's only construct for performing temporal reasoning directly, one must often combine it in ad-hoc ways with other language constructs to express temporal constraints. In contrast, MFOTL Ω has richer support for expressing temporal constraints over a more sophisticated time model (e. g., time points are timestamped and multiple events can happen at the same time point). In particular, the temporal operator S I in combination with the other Boolean connectives often allows one to express temporal properties naturally.
section_name: Comparison with CQL

section_content: For our performance evaluation, we use the policies from Sect. 4. 1 and synthetically generated logs with different time spans (in days). 1 The logs contain withdraw events from 500 users, except for (P6), for which we consider only 100 users. Each user makes on average five withdrawals per day. The SQL queries for PostgreSQL and the CQL queries for STREAM are manually obtained from the corresponding MFOTL Ω formulas (P1)-(P6). The MFOTL Ω formulas and SQL queries have the same semantics, while the semantic differences between MFOTL Ω and CQL are not substantial for the policies and logs considered. In particular, the tools (PostgreSQL version 9. 1. 4, STREAM version 0. 6. 0, and our prototype, which extends our monitoring tool MonPoly [5] ) output the same violations. Finally, note that the formulas differ in the number of temporal and aggregation operators, as well as their respective nesting. Table 1 shows the running times of the three tools on a standard desktop computer with 8 GB of RAM and an Intel Core i5 CPU with 2. 67 GHz. PostgreSQL's running times only account for the query evaluation, performed once per log file, and not for populating the database. For MAX aggregations, STREAM aborts with a runtime error. We mark this in the table with the symbol ‡. Overall, our tool's performance is between STREAM's and PostgreSQL's for our examples. We also note that STREAM and our tool scale linearly in our experiments with respect to the logs' time spans. This is not the case for Post-greSQL. 

Regarding memory usage, our tool uses less than 50 MB for each policy, and memory consumption does not depend on the logs' time span. STREAM's memory usage is set in advance as a configuration parameter. In these experiments, we set this parameter to 1. 5 GB for policy (P3) and to 64 MB for the other policies. STREAM runs out of memory for (P3). Setting the parameter higher, e. g. to 2 GB, leads to a memory-related runtime error for (P3), which is also marked with the symbol ‡ in the table. PostgreSQL's memory consumption increases with the time span. It varies from around 400 MB for (P1) and (P5), to 2. 5 GB for (P2) and (P6), and to around 4 GB for (P3), for the last value of the time span for which a timeout does not occur. 

In the following, we comment on the running times. We first focus on our tool. We observe that the formulas (P1), (P2), and (P5) are roughly equally hard to monitor. This is because their running times are dominated by the evaluation of the subformula of the form [ω a a, τ. [0,31) withdraw(u, a) ∧ ts(τ )](v; u), which is common to all three formulas. In more detail, the number of tuples satisfying the temporal subformula at a time point is on average 31mn, where m is the average number of withdrawals per day of a user and n is the number of users. This size is significantly larger than the size of the relations corresponding to the additional subformulas in (P2) and (P5). For (P2), at each time point, on average the relations for limit_on(u) and limit_off (u) contain (n/10)/2 tuples each and the relation for ¬limit_off (u) S limit_on(u) contains n/2 tuples, because the limit flag is toggled for each user on average every 10 days. For (P5), the outer aggregation operator AVG is applied to a relation of average size n. Note that in general the nesting of aggregation operators does not have a substantial impact on the running times, since aggregating over a relation does not increase its size. 

For formulas (P3), (P4), and (P6), the main impact on the running times is due to the computation of the natural join [[ϕ]] [[ψ]], where ϕ and ψ denote the two main conjuncts in the formalization of the formulas (P2), (P3), (P4), and (P6). The formula (P3) is slower to monitor than (P2) because the natural join can be optimized when fv(ψ) ⊆ fv(ϕ), which is the case for (P2) but not for (P3). This remark also applies to (P4) and (P6). The relations for the additional subformulas in (P3) are also larger than in (P2): on average, the relation for limit(u, ) contains n/10 tuples and the relation for ¬∃. limit(u, ) S limit(u, ) contains n tuples because the limits are changed on average every 10 days for each user. The formula (P4) takes longer to monitor than (P3) because it uses a significantly larger time window. Finally, (P6) takes significantly longer to monitor than (P4) because the input and output relations of the main join operator are also larger. For (P3) and (P4), the two input relations and the output relation each have size n. For (P6), the sizes of the input relations are on average n and 31mn while the output relation is on average of size 31mn. 

PostgreSQL performs worst in these experiments. This is not surprising as PostgreSQL was not designed for this application domain. In particular, PostgreSQL has no support for temporal reasoning and we treat time as just another data value, as explained in Sect. 4. 1. Treating time as data has the following disadvantages. First, it is not suited for the online event processing: query evaluation does not scale because the database grows over time and the query must be reevaluated on the entire database each time new events are added. Second, even for offline processing (as done in our experiments), the query evaluation procedure does not take advantage of the temporal ordering of events. This deficiency is most evident when evaluating the SQL queries for the formulas (P2) and (P3). We note that while PostgreSQL is faster on (P3) than on (P2), it consumes significantly more memory for (P3) than for (P2). 

In contrast to PostgreSQL, STREAM is designed for online event processing and its running times, except for policy (P3), are consistently better than those of our tool. For the policy (P3), we have bypassed STREAM's default temporal reasoning by treating time as data, and we observe a very high memory consumption, as is the case with PostgreSQL. We also remark that the extension needed to go from formalizing (P1) to formalizing (P2) has a larger impact on STREAM's performance than on our tool. This is because extending the CQL query for (P1) requires a workaround, which does not use the sliding window construct. 

Even though STREAM generally outperforms our tool, the performance differences are not as significant as one might expect. One reason why our tool is slower is because it must account for MFOTL Ω 's underlying time model, which is more complex than CQL's. MFOTL Ω has also a richer tool set than CQL to express temporal patterns.
section_name: Tool performance

section_content: Existing logic-based policy monitoring approaches offer little support for aggregations. To rectify this shortcoming, we extended metric first-order temporal logic with expressive SQLlike aggregation operators and presented a monitoring algorithm for this language. Our experimental results for a prototype implementation of the algorithm are promising. The prototype's performance is in the reach of optimized stream-processing tools, despite its richer input language and its lack of systematic optimization. As future work, we will investigate performance optimizations for our monitor. In general, it remains to be seen how logic-based monitoring approaches can benefit from the techniques used in stream processing.
section_name: Conclusion

section_name: Acknowledgments

section_content: This work was partially supported by the Zurich Information Security and Privacy Center (ZISC).
section_name: Acknowledgments