Information Technology Reference
In-Depth Information
G
∀
x
:
w.
((
q
(
x
)
∧¬
r
(
x
))
⇒¬
r
(
x
)
U
∃
y
:
w.
(
p
(
x,y
)
∧¬
r
(
x
))))
ϕ
8
G
∀
x
:
w. p
(
x
)
∨
((
q
(
x
)
∧¬r
(
x
))
U
(
r
(
x
)
∨
((
¬q
(
x
)
∧¬r
(
x
))
U
(
r
(
x
)
∨
((
q
(
x
)
∧¬r
(
x
))
U
(
r
(
x
)
∨
(
¬q
(
x
)
W
r
(
x
)
∨
G
q
(
x
)))))))))
⇒
(
¬
q
(
x
)
∧¬
r
(
x
))
U
(
r
(
x
)
ϕ
7
G
∀x
:
w.
((
q
(
x
)
∧
(
¬r
(
x
)
∧
(
F
r
(
x
))))
⇒
((
p
(
x
)
⇒
(
¬r
(
x
)
U
(
s
(
x
)
∧¬r
(
x
))))
U
r
(
x
)))
ϕ
6
G
∀
x
:
w.
((
q
(
x
)
∧
(
¬
r
(
x
)
∧
(
F
r
(
x
))))
⇒
(
p
(
x
)
U
r
(
x
)))
ϕ
5
G
∀x
:
w.
(
q
(
x
)
⇒
(
F
(
q
(
x
)
∧
(
F
p
(
x
)))))
ϕ
4
G
∀x
:
w.
((
q
(
x
)
∧
(
¬r
(
x
)
∧
(
F
r
(
x
))))
⇒
(
¬
p
(
x
)
U
r
(
x
)))
ϕ
3
Trace length
100
1000
10000
G
(
∃
x
:
w. q
(
x
)
⇒
G
∀
y
:
w.
¬
p
(
y
))
ϕ
2
G
∀x
:
w. ¬p
(
x
)
ϕ
1
-100 -50
-10
-1
0
1
10
50
100
1000
10000
Fig. 2.
Difference in space consumption at runtime: SA-based monitor vs. progression
Some of the results are visualised in Fig. 2. For each LTL
FO
formula corresponding
to a pattern, we randomly generated 20 traces of lengths 100, 1000,and10000, respec-
tively, and passed them to both algorithms. We then measured the average space con-
sumption of each algorithm at different trace lengths. For progression this is measured
simply in terms of the length of the formula at a given time, whereas for the SA-based
monitor
M
ϕ,v
it is determined recursively as follows: Recall,
M
ϕ,v
first creates two in-
stances of Algorithm T,
T
ϕ,v
and
T
¬ϕ,v
, each of which creates a buffer, call it
B
ϕ
,resp.
B
¬ϕ
.Let
B
=
B
ϕ
∪ B
¬ϕ
,and(
q
i
,
[
obl
i,
0
,...,obl
i,n
]) be the
i
-th element of
B
,then
|
=
|B|−
1
i
=0
=
|B|−
1
i
=0
|obl
i,
0
|
|obl
i,n
|
M
ϕ,v
|
|
(
q
i
,
[
obl
i,
0
,...,obl
i,n
])
|
(1 +
+
...
+
),
+
A
ψ,v
∈obl
i,j
|
|obl
i,j
|
where
, i.e., the sum of the top-level monitor's
constituents as well as that of all of its submonitors. Finally, we also need to add the
total size of the precomputed GBA look-up table.
The end markers on the left of each horizontal bar show how much bigger in the
worst case
an SA-based monitor is for a given formula compared to the corresponding
progression-based monitor (and vice versa for the right markers). The small shapes in
the middle denote the
average
size difference of the two monitors over the whole length
of a trace. This difference is most striking for
ϕ
2
on longer traces (e.g.,
Δ
=
|
obl
i,j
|
M
ψ,v
|
10000
for traces of length 10000), where the average almost coincides with the worst case.
As such, this example brings to surface one of the potential pitfalls of progression,
namely that a lot of redundant information can accumulate over time: If
≥
x
:
w. q
(
x
)
ever becomes true, then
P
, which operates purely on a syntactic level, will produce a
new conjunct
G
∃
∀
y
:
w.
¬
p
(
y
) for each new event, even though semantically it is not
