Information Technology Reference
In-Depth Information
⎧
⎨
4
(
w
(
j
)
)
4
(
w
(
i
)
)
ϕ
ψ
if
complete
(
w
)
succ
a
∗
(
w
)
j≤i
i
∈
succ
a
∗
(
w
)
j
∈
4
(
w
(
j
)
)
ϕ
R
a
ψ
4
(
w
)=
4
(
w
(
i
)
)
ϕ
ψ
⎩
j∈
succ
a
∗
(
w
)
j≤i
i∈
succ
a
∗
(
w
)
otherwise
4
(
w
(
i
)
)
p
ψ
i∈
succ
a
∗
(
w
)
In contrast to the until and release operators two cases have to be distinguished
for their abstract counterparts. If the sequence of abstract successors for a word
is complete, i.e. if the sequence terminates because of an umatched return, the
operators cannot evaluate to
p
or
p
, respectively.
⊥
3.2 Visibly Push-down Mealy Machines (VPMM)
A typical approach to monitoring temporal properties is based on formula rewrit-
ing. When observing a symbol, the formula is evaluated and additionally rewrit-
ten to maintain the gained information. This requires equations for transforming
any formula into a formula where each temporal operator is an X operator or is
guarded by some X. Then, every sub-formula can explicitly be evaluated when
reading only one new letter. For the U operator, the unfolding equation is stan-
dard and the abstract operator can be unfolded analogously:
ϕ
U
ψ
≡
ψ
∨
(
ϕ
∧
X(
ϕ
U
ψ
))
ϕ
U
a
ψ
X
a
(
ϕ
U
a
ψ
))
≡
ψ
∨
(
ϕ
∧
What remains is an unfolding of the abstract next operator X
a
. According
to the semantics, reading a return or an internal symbol it behaves like the
classical X operator, accept that there must not follow a return symbol in the
next step. Evaluating a formula X
a
ϕ
for a call symbol, the evaluation of
ϕ
needs
to be postponed until the matching return symbol is read. If a return follows
immediately it is matching. Otherwise the matching return can be reached by
following the abstract sequence of positions until the first unmatched return.
X
a
(
ϕ
)
≡
¬
call
∧
¬
ret
∧
ϕ
))
(
X(
∨
ϕ
))
∨
(
call
∧
X(
¬
ret
∧
true
U
a
(
¬
call
∧
X(
ret
∧ϕ
))))
(
call
∧
X(
ret
∧
Using this equality for substituting X
a
operators, we can equivalently transform
any CaRet formula s.t. every temporal operator is guarded by X and hence do
a step-wise evaluation. When only the classical operators are considered, the
number of different formulae arising during evaluation is bounded (as long as
