Information Technology Reference
In-Depth Information
Basin et al. [4] extend Chomicki's monitor towards bounded future operators using
the same logic. Furthermore, they allow infinite relations as long as these are repre-
sentable by automatic structures, i.e., automata models. In this way, they show that the
restriction on formulae to be domain independent is no longer necessary. LTL
FO
,in
comparison, is more general, in that it allows computable relations and functions. On
the other hand, LTL
FO
lacks syntax to directly specify metric constraints.
The already cited work of Halle and Villemaire [16] describes a monitoring algo-
rithm for a logic with quantification identical to ours, but without function symbols or
arbitrary computable relations. The resulting monitors are generated “on the fly” by us-
ing syntax-directed tableaux. In our approach, however, it is possible to pre-compute the
individual BAs for the respective subformulae of a policy/levels of the SA, and thereby
bound the complexity of that part of our monitor at runtime by a constant factor.
Sistla and Wolfson [23] also discuss a monitor for database triggers whose conditions
are specified in a logic, which uses an assignment quantifier that binds a single value or
a relation instance to a global, rigid variable. Their monitor is represented by a graph
structure, which is extended by one level for each updated database state, and as such
proportional in size to the number of updates.
Finally, there are works dealing with so called parametric monitoring which, al-
though not based on first-order logic, offer support for monitoring traces carrying data
(cf. [1,24,9]). The approach followed by [9] is to “slice” a trace according to the pa-
rameters occurring in it and then to forward the
n
(effectively propositional) subtraces
to
n
monitor instances of the same specification; for example, one per logged-in user
or per opened file. In [1], a similar technique is applied for matching regular expres-
sions with the program trace, when restricted to the symbols declared in an expression.
All approaches allow the user to add variables to a specification, but only [24] offers
quantifiers. However, to restrict their scope, they must directly precede a positive so
called parameterised proposition, which is ensured by syntactic rules that prohibit arbi-
trary nesting or use of negation that could otherwise help to get around this constraint.
None of the approaches support arbitrary nesting of quantifiers and temporal operators,
use of negation, or function symbols to name just some important restrictions. How-
ever, on the plus side, one is able to use optimised monitoring techniques, developed in
the propositional domain, and apply them—with these restrictions in mind—to traces
carrying data. For Java, a widely used such implementation is JavaMOP [18].
7
Conclusions
To the best of our knowledge, our algorithm is the first to devise impartial monitors,
i.e., address the prefix problem instead of a (variant of the) word problem, for policies
given in an undecidable first-order temporal logic. Moreover, unlike other approaches,
such as [23,16] and even [6], we are even able to precompute most of the state space
required at runtime as the different levels of our SAs correspond to standard GBAs that
can be generated before monitoring commences. As required, our monitor is monotonic
and in principle trace-length independent. The latter, however, deserves closer exami-
nation. Consider formula
ϕ
8
in Fig. 2: once the left hand side of the implication holds,
it basically forces the monitor to memorise all occurrences of
x
for all events and keep
