Information Technology Reference
In-Depth Information
Theorem 4. The model checking problem for LTL FO is in ExpSpace.
The reason for this result is that we can devise a reduction of that problem to LTL model
checking in exponential space. While the PSpace-lower bound is easy, e.g., via reduc-
tion of the LTL FO word problem, we currently do not know how tight these bounds are
and, therefore, leave this as an open problem. Note also that the results of both Theo-
rem 3 and Theorem 4 are obtained even without taking into account the complexities of
the interpretations of function symbols and I -operators; that is, for these results to hold,
we assume that interpretations do not exceed polynomial, resp. exponential space.
We have seen in
2 that the prefix problem lies at the heart of an impartial monitor.
While in LTL it was possible to build an impartial monitor using a model checker (albeit
a very inefficient one), the following shows that this is no longer possible.
§
Lemma 2. Let
A
be a first-order structure and ϕ
LTL FO ,then
L
( ϕ ) A =
{
(
A
,w )
|
(2 Ev ) ω , and (
A A
,w
A
,w )
|
= ϕ
}
. Testing if
L
( ϕ ) A
=
is generally undecidable.
Theorem 5. The prefix problem for LTL FO is undecidable.
Proof (Sketch). As in Theorem 1: (
A
)
bad( X ϕ ) iff
L
( ϕ ) A =
for any σ
Ev.
5
Monitoring LTL FO
A corollary of Theorem 5 is that there cannot exist a complete monitor for LTL FO -
definable infinite trace languages. Yet one of the main contributions of our work is
to show that one can build a sound and efficient LTL FO monitor using a new kind of
automaton. Before we go into the details of the actual monitoring algorithm, let us
first consider the automaton model, which we refer to as spawning automaton (SA).
SAs are called that, because when they process their input, they potentially “spawn” a
positive Boolean combination of “children SAs” (i.e., subautomata) in each such step.
Let
+ ( X ) denote the set of all positive Boolean formulae over the set X .Wesay
that some set Y
B
+ ( X ), written Y
X satisfies a formula β
∈B
|
= β , if the truth
assignment that assigns true to all elements in Y and false to all X
Y satisfies β .
Definition 8. A spawning automaton , or simply SA, is given by
A
=( Σ,l,Q,Q 0 ,
δ ,
F
) ,where Σ is a countable set called alphabet, l
N 0 the level of
A
, Q a finite set of
states, Q 0
Q a set of distinguished initial states, δ a transition relation, δ what is
called a spawning function, and
F
=
{
F 1 ,...,F n |
F i
Q
}
an acceptance condition
2 Q and δ : Q
+ (
<l ) ,
(to be defined later on). We have δ : Q
×
Σ
−→
×
Σ
−→ B
A
<l =
{A |A is an SA with level less than l
where
A
}
.
A
over input w
Σ ω is a mapping ρ :
N 0 −→
Q ,s.t. ρ (0)
Q 0
Definition 9. A run of
and ρ ( i +1)
δ ( ρ ( i ) ,w i ) for all i
N 0 . ρ is locally accepting if Inf( ρ )
F i
=
for all F i ∈F
,where Inf( ρ ) denotes the set of states visited infinitely often. It is called
accepting if l =0 and it is locally accepting. If l> 0 , ρ is called accepting if it is
locally accepting and for all i ∈ N 0 there is a set Y ⊆A
<l ,s.t. Y | = δ ( ρ ( i ) ,w i ) and
A
Y have an accepting run, ρ , over w i .The accepted language of
all automata
A
,
Σ ω , for which it has at least one accepting run.
L
(
A
) , consists of all w
 
Search WWH ::




Custom Search