Information Technology Reference
In-Depth Information
Definition 3.
For any
L
⊆
Σ
ω
,
u
∈
Σ
∗
is called a
good prefix
(resp.
bad prefix
)iff
uΣ
ω
⊆
L
holds (resp.
uΣ
ω
∩
L
=
∅
).
We shall use good(
L
)
Σ
∗
(resp. bad(
L
)) to denote the set of good (resp. bad)
prefixes of
L
. For brevity, we also write good(
ϕ
) instead of good(
⊆
L
(
ϕ
)), and do the
(
ϕ
)).
A monitor that detects good (resp. bad) prefixes has been termed impartial in [12]
as it not only states something about the past, but also about the future: once a good
(resp. bad) prefix has been detected, no matter how the system would evolve in an
indefinite future, the property would remain satisfied (resp. violated). In that sense,
impartial monitors are monotonic by definition. Moreover in [8], a construction is given,
showing how to obtain trace-length independent (even optimal) impartial monitors for
LTL and a timed extension called TLTL. The obtained monitor basically returns
L
same for bad(
to
the user if
u
bad(
ϕ
) holds, and ? otherwise. Not surprisingly
though, the monitoring problem such a monitor solves is computationally more involved
than the word problem. It solves what we call the prefix problem (of LTL), which can
easily be shown PSpace-complete by way of LTL satisfiability.
Definition 4.
The
prefix problem for LTL
is defined as follows.
Input:
Aformula
ϕ
∈
good(
ϕ
) holds,
⊥
if
u
∈
(2
AP
)
∗
.
∈
LTL(AP)
and some trace
u
∈
Question:
Does
u
good(
ϕ
)
(resp.
bad(
ϕ
)
) hold?
Theorem 1.
The prefix problem for
LTL
is PSpace-complete.
Proof.
For brevity, we will only focus on bad prefixes. It is easy to see that
u
∈
∈
bad(
ϕ
)
iff
. Constructing this conjunction takes polynomial
time and the corresponding emptiness check can be performed in PSpace [22]. For
hardness, we proceed with a reduction of LTL satisfiability. Again, it is easy to see that
L
L
(
u
0
∧
X
u
1
∧
XX
u
2
∧
...
∧
ϕ
)=
∅
(
ϕ
)
∅
iff
σ
∈
bad(
X
ϕ
) for any
σ
∈
2
AP
. This reduction is linear, and as PSpace =
=
We would like to point out the possibility of building an impartial though trace-
length dependent LTL monitor using an “off the shelf” model checker, which accepts
a propositional Kripke structure and an LTL formula as input. Note that here we make
the assumption that Kripke structures produce infinite as opposed to finite traces.
Definition 5.
The
model checking problem for LTL
is defined as follows.
Input:
Aformula
ϕ
co-PSpace, the statement follows.
over
2
AP
.
∈
LTL(AP)
and a Kripke structure
K
Question:
Does
(
ϕ
)
hold?
As in LTL the model checking and the satisfiability problems are both PSpace-complete
[22], we can use a model checking tool as monitor: given that it is straightforward
to construct
L
(
K
)
⊆L
)=
u
(2
AP
)
ω
, in no more than polynomial time, we return
K
,s.t.
L
(
K
ϕ
) holds, and ? if neither
holds. One could therefore be tempted to think of monitoring merely in terms of a
model checking problem, but we shall see that as soon as the logic in question has
an undecidable satisfiability problem this reduction fails. Besides, it can be questioned
whether monitoring as model checking leads to a desirable monitor with its obvious
trace-length dependence and having to repeatedly solve a PSpace-complete problem
for each new event.
to the user if
L
(
K
)
⊆L
(
ϕ
) holds,
⊥
if
L
(
K
)
⊆L
(
¬
