Information Technology Reference
In-Depth Information
Contributions.
Although aggregations have appeared previously in monitoring,
to our knowledge, our language is the first to add expressive SQL-like aggre-
gation operators to a first-order temporal setting. This enables us to express
complex compliance policies with aggregations. Our prototype implementation
of the presented monitoring algorithm is therefore the first tool to handle such
policies, and it does so with acceptable performance.
Related Work.
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 [19]. 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 Halle and Villemaire [18], Bauer at al. [9], and Basin et al. [7].
Except for the counting quantifier [9], none of them support aggregations. Bian-
culli et al. [10] 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 trans-
lation 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 [23] describe an integration
of aggregation operators into their monitoring algorithm for a first-order tempo-
ral logic. Their aggregation operators are different from those presented here in
that they involve two formulas 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 different kinds of aggregations are
LarvaStat [13], LOLA [15], EAGLE [4], and an approach based on algebraic alter-
nating automata [16]. 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 [14]
handle SQL-like aggregation operators. For example, in STREAM's query lan-
guage CQL [3] one selects events in a specified time range, relative to the current
position in the stream, into a table on which one performs aggregations. The tem-
poral expressiveness of such languages is weaker than our language, in particular,
linear-time temporal operators are not supported.
Organization.
In Section 2, we extend MFOTL with aggregation operators. In
Section 3, we present our monitoring algorithm, which we evaluate in Section 4.
In Section 5, we draw conclusions. Additional details are given in the appendix.
