Information Technology Reference
In-Depth Information
A
ϕ,v
, in the usual manner.
T1.
[Create SA.] Create an SA,
,σ
) be the event that was read.
T3.
[Update potentially locally accepting runs.] Let
B
and
B
be (initially empty)
buffers. If
B
=
A
T2.
[Wait for new event.] Let (
∅
, for each
q
∈
Q
0
and for each
q
∈
δ
→
(
q,
(
A
,σ
)):add
(
q
,
[
δ
↓
(
q,
(
A
,σ
))]) to
B
. Otherwise, set
B
=
B
, and subsequently
B
=
∅
.Next,
B
and for all
q
∈
,σ
)):add(
q
,
[
obl
new
,
for all (
q,
[
obl
1
,...,obl
n
])
∈
δ
→
(
q,
(
A
,σ
)).
T4.
[Create submonitors.] For each (
q,
[
obl
new
,obl
1
...,obl
n
])
obl
1
,...,obl
n
]) to
B
,where
obl
new
=
δ
↓
(
q,
(
A
∈
B
: call Algorithm M
with argument
ψ
(under corresponding
v
) for each
A
ψ,v
that occurs in
obl
new
.
T5.
[Iterate over candidate runs.] Assume
B
=
. Create a counter
j
=0
and set (
q,
[
obl
0
,...,obl
n
]) =
b
j
to be the
j
th element of
B
.
T6.
[Send, receive, replace.] For all 0
{
b
0
,...,b
m
}
,σ
) to all submonitors corre-
sponding to SAs occurring in
obl
i
, and wait for the respective verdicts. For every
returned
≤
i
≤
n
:send(
A
(resp.
⊥
) replace the corresponding SA in
obl
i
with
(resp.
⊥
).
T7.
[Corresponding run has violated obligations?] For all 0
≤
i
≤
n
:if
obl
i
=
⊥
,
remove
b
j
from
B
andgotoT9.
T8.
[Obligations met?] For all 0
≤
i
≤
n
:if
obl
i
=
, remove
obl
i
.
m
,set
j
to
j
+1andgotostepT6.
T10.
[Communicate verdict.] If
B
=
T9.
[Next run in buffer.] If
j
≤
, send “no runs” to the calling Algorithm M and
return, otherwise send “some run(s)” and go back to T2.
∅
❚
For a given
ϕ
,u
) to denote the successive
application of Algorithm M for formula
ϕ
,firston
u
0
,then
u
1
, and so forth. We then
get
∈
LTL
FO
and (
A
,u
), let us use
M
ϕ
(
A
Theorem 7.
M
ϕ
(
A
,u
)=
⇒
A
,u
)
∈
good(
ϕ
)
(resp. for
⊥
and
bad(
ϕ
)
).
(
5.3
Experimental Results
To demonstrate feasibility and to get an intuition on runtime performance we have im-
plemented the above.
4
The only liberty we took in deviating from our description is
the following: since the SAs for
ϕ
∈
LTL
FO
on the different levels basically con-
sist of ordinary GBAs for the respective subformulae of
ϕ
, we have used an “off the
shelf” GBA generator, lbt
5
. Moreover, our algorithm bears the advantage that it is pos-
sible to precompute the SAs that are required at runtime (i.e., we replaced step T1
in Algorithm T with a look-up in a precomputed table of SAs and merely use a new
valuation each time). We also compared our implementation with the somewhat naive
(but, arguably, easier to implement) approach of monitoring, described in [6]. There,
we used formula rewriting, sometimes referred to as progression (cf. [2]): a function,
P
, continuously “rewrites” a formula
ϕ
∈
LTL
FO
using an observed event,
σ
,s.t.,
σw
=
P
(
ϕ,σ
) holds.
As a benchmark for our tests, we have used several formulae derived from the well-
known specification patterns [13], and added quantification to crucial positions.
|
=
ϕ
⇔
w
|
4
Available as open source Scala project on
