Information Technology Reference
In-Depth Information
track of a quantified formula, hence the two
send
-actions will also spawn a conjunction
of subautomata, basically, to check if
eq
(
u,u
)
eq
(
ip,ip
) holds. The respective valu-
ations are given below each SA, whereas the respective current states are marked in grey.
⇒
5.2
Monitor Construction
Before we look at the actual monitor construction, let us first introduce some additional
concepts and notation: For a finite run
ρ
in
A
ϕ
over (
A
,u
), we call
δ
↓
(
ρ
(
j
)
,
(
A
j
,u
j
)) =
obl
j
an
obligation
,where0
,inthat
obl
j
represents the language to be
satisfied after
j
inputs. That is,
obl
j
refers to the language represented by the positive
Boolean combination of spawned SAs. We say
obl
j
is
met
by the input, if (
≤
j<
|
u
|
j
,u
j
)
A
∈
j
,u
j
)
good(
obl
j
) and
violated
if (
bad(
obl
j
).Furthermore,
ρ
is called
potentially
locally accepting
, if it can be extended to a run
ρ
over (
A
∈
A
,u
) together with some infinite
suffix, such that
ρ
is locally accepting.
The monitor for a formula
ϕ
LTL
FO
can now be described in terms of two mutu-
ally recursive algorithms: The main entry point is Algorithm M. It reads an event and
issues two calls to a separate Algorithm T: one for
ϕ
(under a possibly empty valuation
v
) and one for
∈
ϕ
(under a possibly empty valuation
v
). The purpose of Algorithm T
is to detect bad prefixes wrt. the language of its argument formula, call it
ψ
. It does
so by keeping track of those finite runs in
¬
A
ψ,v
that are potentially locally accepting
and where its obligations haven't been detected as violated by the input. If at any time
not at least one such run exists, then a bad prefix has been encountered. Algorithm T,
in turn, uses Algorithm M to evaluate if obligations of its runs are met or violated by
the input observed so far (i.e., it inductively creates submonitors): after the
i
th input, it
instantiates Algorithm M with argument
ψ
(under corresponding valuation
v
) for each
A
ψ
,v
that occurs in
obl
i
and forwards to it all observed events from time
i
on.
Algorithm M
(
Monitor
).
LTL
FO
(under a possibly empty
valuation
v
). Its abstract behaviour is as follows: Let us assume an initially empty
first-order temporal structure (
The algorithm takes a
ϕ
∈
A
,u
). Algorithm M reads an event (
A
,σ
),prints“
”
if (
AA
,uσ
)
∈
good(
ϕ
) (resp. “
⊥
”forbad(
ϕ
)), and returns. Otherwise it prints “?”,
,uσ
) holds.
3
M1.
[Create instances of Algorithm T.] Create two instances of Algorithm T: one with
ϕ
and one with
whereas we now assume that (
A
,u
)=(
AA
ϕ
, and call them
T
ϕ,v
and
T
¬ϕ,v
, respectively.
M2.
[Forward next event.] Wait for next event (
¬
,σ
) and forward it to
T
ϕ,v
and
T
¬ϕ,v
.
M3.
[Communicate verdict.] If
T
ϕ,v
sends “no runs”, print
A
⊥
and return. If
T
¬ϕ,v
sends
“no runs”, print
and return. Otherwise, print “?” and go to M2.
❚
The algorithm takes a
ϕ
∈
Algorithm T
(
Track runs
).
LTL
FO
(under a corresponding
valuation
v
), for which it creates an SA,
A
ϕ,v
.Itthenreadsanevent(
A
,σ
) and returns,
if
,σ
), does not have any potentially locally accepting runs,
for which obligations haven't been detected as violated. Otherwise, it saves the new
state of
A
ϕ,v
, after processing (
A
A
ϕ,v
, waits for new input, and then checks again, and so forth.
3
Obviously, the monitor does not really keep (
A
,u
) around, or it would be necessarily trace-
length dependent. (
A
,u
) is merely used here to explain the inner workings of the monitor.
