Information Technology Reference
In-Depth Information
As there exist many different ways in which a system can be monitored in this ab-
stract sense, we are going to put forth very specific assumptions concerning the prop-
erties and inner-workings of what we consider a “proper” monitor. None of these as-
sumptions is particularly novel or complicated, but they help describe and distinguish
the task of a “proper” monitor from that of, say, a model checker, which can also be
used to solve monitoring problems as we shall see.
The two basic assumptions are easy to explain: Firstly, we demand that a monitor
is what we call
trace-length independent
, meaning that its efficiency does not decline
with an increasing number of observations. Secondly, we demand that a monitor is
monotonic
wrt. reporting violations (resp. satisfication) of a specification, meaning that
once the monitor returns “
SAT
” to the user, additional observations do not lead to it
returning “
UNSAT
” (and vice versa). We are going to postulate further assumptions,
but these are mere consequences of the two basic ones and are explained in
2.
At the heart of this paper, however, is a custom first-order temporal logic, in the
following referred to as LTL
FO
, which is undecidable. Yet we outline a sound, albeit
incomplete, monitor construction for it based on a new type of automaton, called spawn-
ing automaton. LTL
FO
was originally developed for the specification of runtime veri-
fication properties of Android “Apps” and has already been used in that context (see
[6] for details). Although [6] gave a monitoring algorithm for LTL
FO
basedonformula
rewriting, it turns out that the automata-based construction given in this paper leads to
practically more efficient results.
As our definition of what constitutes a “proper” monitor is not tied to a particular
logic we will develop it first for standard LTL (
§
§
2), the quasi-standard in the area of
runtime verification. In
3, we give a more detailed account of LTL
FO
than was avail-
able in [6], before we lift the results of
§
4). The automata-
based monitor construction for LTL
FO
along with experimental results is described in
§
§
2 to the first-order setting (
§
§
5, related work in
6. Detailed proofs can be found in [7].
2
Complexity of Monitoring in the Propositional Case
In what follows, we assume basic familiarity with LTL and topics like model checking
(cf. [3] for an overview). Despite that, let us first state a formal LTL semantics, since
we will consider its interpretation on infinite and finite traces. For that purpose, let AP
denote a set of propositions, LTL(AP) the set of well-formed LTL formulae over that
set, and for some set
X
set
X
∞
=
X
ω
X
∗
to be the union of the sets of all infinite
and finite traces over
X
.WhenAP is clear from the context or does not matter, we use
LTL instead of LTL(AP). Also, for a given trace
w
=
w
0
w
1
...
, the trace
w
i
is defined
as
w
i
w
i
+1
...
. As a convention we use
u,u
,...
to denote finite traces, by
σ
the trace
of length 1,and
w
for infinite ones or where the distinction is of no relevance.
Definition 1.
Let
ϕ
∪
(2
AP
)
∞
be a non-empty trace, and
i
∈
LTL(AP)
,
w
∈
∈
N
0
,then
w
i
|
=
p
iff
p
∈
w
i
,
where
p
∈
AP
,
w
i
ϕ
iff
w
i
|
=
¬
|
=
ϕ
does not hold
,
w
i
ψ
iff
w
i
=
ϕ
and
w
i
|
=
ϕ
∧
|
|
=
ψ,
w
i
>i
and
w
i
+1
|
=
X
ϕ
iff
|
w
|
|
=
ϕ,
w
i
,w
k
j<k,w
j
|
=
ϕ
U
ψ
iff there is a
k
s.t.
i
≤
k<
|
w
|
|
=
ψ,
and for all
i
≤
|
=
ϕ.
