Information Technology Reference
In-Depth Information
necessary. Hence, the longer the trace, the greater the average difference in size (similar
in case of
ϕ
3
and
ϕ
4
).
At first glance, it may seem a curious coincidence that the left markers of each bar
align perfectly, because this indicates that for all three traces that belong to a given
formula, the SA-based monitor is in the worst case by exactly the same constant
k
bigger than the progression-based one, irrespective of the trace. However, it makes sense
if we consider when this worst case occurs; that is, whenever the SA-based monitor (and
consequently also the progression-based one) does not have to memorise any data at all,
in which case the size of the SA-based monitor's look-up table weighs the most; that is,
the size of the look-up table is almost equal to
k
. Usually this happens when monitoring
commences, hence, there is a perfect alignment on all traces. On the other hand, the
worst case for progression arises whenever the amount of data to be memorised by the
monitor has reached its maximum. As this depends not only on the formula, but also on
the content of the randomly generated traces (and in some of the examples also on their
lengths, as seen in the previous example), we generally don't observe alignment on the
right.
For those examples that, on average, favour progression, note that the difference
in size is less dramatic—a fact, which may be slightly obfuscated by the pseudo-
logarithmic scale of the
x
-axis. Again, the differences in these examples (
ϕ
1
,
ϕ
5
,
ϕ
6
,
and
ϕ
7
) can be mostly explained by the fact that an SA-based monitor generally wastes
more space for “book keeping”. Naturally, all examples are also exposed to a degree of
randomness due to the generated traces, which would also deserve closer investigation.
Hence, these tests are indicative as well as promising, but certainly not conclusive yet.
6
Related Work
This is by no means the first work to discuss monitoring of first-order specifications.
Motivated by checking temporal triggers and temporal constraints, the monitoring prob-
lem for different types of first-order logic has been widely studied, e.g., in the database
community. In that context, Chomicki [10] presents a method to check for violations
of temporal constraints, specified using (metric) past temporal operators. The logic in
[10] differs from LTL
FO
, in that it allows natural first-order quantification over a sin-
gle countable and constant domain, whereas quantified variables in LTL
FO
range over
elements that occur at the current position of the trace (see also [16,5]). Presumably, to
achieve the same effect, [10] demands that policies are what is called “domain indepen-
dent”, so that all statements refer to known objects. As such, domain independence is
a property of the policy and shown to be undecidable. In contrast, one could say that
LTL
FO
has a similar notion of domain independence already built-in, because of its
quantifier. Like LTL
FO
, the logic in [10] is also undecidable; no function symbols are
allowed and relations are required to be finite. However, despite the fact that the pre-
fix problem is not phrased as a decision problem, its basic idea is already denoted by
Chomicki as the potential constraint satisfaction problem. In particular, he shows that
the set of prefixes of models for a given formula is not recursively enumerable. On the
other hand, the monitor in [10] does not tackle this problem and instead solves what we
have introduced as the word problem, which, unlike the prefix problem, is decidable.
