Information Technology Reference
In-Depth Information
And if
w
0
=
ϕ
instead. Although this semantics, which
was also proposed in [21], gives rise to mixed languages, i.e., languages consisting of
finite and infinite traces, we shall only ever be concerning ourselves with either finite-
trace or infinite-trace languages, but not mixed ones. It is easy to see that over infinite
traces this semantics matches the definition of standard LTL. Recall, LTL is a decidable
logic; in fact, the satisfiability problem for LTL is known to be PSpace-complete [22].
As there are no commonly accepted rules for what qualifies as a monitor (not even
in the runtime verification community), there exist a myriad of different approaches
to checking that an observed behaviour satisfies (resp. violates) a formal specification,
such as an LTL formula. Some of these (cf. [17,5]) consist in solving the word prob-
lem (see Definition 2). A monitor following this idea can either first record the entire
system behaviour in form of a trace
u
|
=
ϕ
holds, we usually write
w
|
Σ
+
,where
Σ
is a finite alphabet of events, or
process the events incrementally as they are emitted by the system under scrutiny. Both
approaches are documented in the literature (cf. [17,15,16,5]), but only the second one
is suitable to detect property violations (resp. satisfaction) right when they occur.
∈
Definition 2.
The
word problem for LTL
is defined as follows.
Input:
Aformula
ϕ
∈
LTL(AP)
and some trace
u
∈
(2
AP
)
+
.
Question:
Does
u
|
=
ϕ
hold?
In [21], a bilinear algorithm for this problem was presented (an even more efficient
solution was recently given in [19]). Hence, the first sort of monitor, which is really
more of a test oracle than a monitor, solves a classical decision problem. The second
sort of monitor, however, solves an entirely different kind of problem, which cannot be
stated in complexity-theoretical terms at all: its input is an LTL formula and a finite
albeit unbounded trace which
grows
incrementally. This means that this monitor solves
the word problem for each and every new event that is added to the trace at runtime. We
can therefore say that the word problem acts as a lower bound on the complexity of the
monitoring problem that such a monitor solves; or, in other words, the problem that the
online monitor solves is at least as hard as the problem that the offline monitor solves.
There are approaches to build efficient (i.e., trace-length independent) monitors that
repeatedly answer the word problem (cf. [17]). However, such approaches violate our
second basic assumption, mentioned in the introduction, in that they are necessarily
non-monotonic. To see this, consider
ϕ
=
a
U
b
and some trace
u
=
{
a
}{
a
}
...
{
a
}
of length
n
. Using our finite-trace interpretation,
u
|
=
ϕ
.However,ifweadd
u
n
+1
=
{
=
ϕ
.
1
For the user, this essentially means that she cannot trust the
verdict of the monitor as it may flip in the future, unless of course it is obvious from
the start that, e.g., only safety properties are monitored and the monitor is built merely
to detect violations, i.e., bad prefixes. However, if we take other monitorable languages
into account as we do in this paper, i.e., those that have either good or bad prefixes (or
both), we need to distinguish between satisfaction and violation of a property (and want
the monitor to report either occurrence truthfully).
b
}
,weget
u
|
1
Note that this effect is not particular to our choice of finite-trace interpretation. Had we used,
e.g., what is known as the weak finite-trace semantics, discussed in [14], we would first have
had
u |
=
ϕ
and if
u
n
+1
=
∅
, subsequently
u |
=
ϕ
.
