Information Technology Reference
In-Depth Information
3.3 Determinizing VPMM
In order to be able to actually implement a Vpmm as monitor to evaluate ob-
servations it must be deterministic. We can lift the determinization construc-
tion for Vpa [13] to determinize a Vpmm
P
) by adding
treatment of output symols. We construct an equivalent deterministic Vpmm
P
=(
Q
,Σ,Γ
,δ
,q
0
,
=(
Q,Σ,Γ,δ,Q
0
,
L
) as follows.
In the finite control
Q
=2
Q×Q
L
2
Q
we store, as in the standard subset
construction for finite automata, a set of
current states
R
×
⊆
Q
and additionally
an
effect relation
S
Q
.
Inbetween a call action
a
c
and its corresponding return action
a
r
,
S
summa-
rizes the transitions that were made on every state. That is, when
⊆
Q
×
P
were in
some state
q
just after reading
a
c
and from there possibly reached some state
q
before reading
a
r
,
S
contains the tuple (
q,q
).
The stack of
P
, stores triples (
S
,R
,a
c
)from
Γ ⊆ Q
× Σ
c
where
R
,S
are the current states and the effect relation at the time the last open call
a
c
occurred. In the initial state
q
0
=
{
(
Id
Q
,Q
0
)
}
, there is no recorded effect, i.e.
each
q
points to itself, and the current states are the initial states of
P
.
Internal.
An internal action
a
int
∈
Σ
int
simply updates the set of current states by
applying
δ
element-wise. The effect relation is updated analogously. If (
q,q
)
S
is a recorded effect on
q
and
q
is mapped to
q
by
δ
on reading
a
int
, then in the
next state of
∈
P
werecordthetuple(
q,q
) as effect on
q
.
We let
δ
((
S,R
)
,a
int
,γ
)=(
S
,R
,γ,
) such that
S
=
(
q,q
)
q
,γ
,
:(
q,q
)
S,
(
q
,γ
,
)
δ
(
q
,a
int
,γ
)
{
|∃
∈
∈
}
R
=
q
|∃
R,γ
,
:(
q
,γ
,
)
δ
(
q,a
int
,γ
)
{
q
∈
∈
}
=
|∃
R,γ
,q
:(
q
,γ
,
)
δ
(
q,a
int
,γ
)
{
q
∈
∈
}
As opposed to the construction for Vpa, we have also to compute the current
output
. It is obtained from all possible transitions from the current states
q
R
via reading
a
int
.Since
δ
is non-deterministic these are in general multiple values
that are considered in disjunction. We therefore take the join, i.e. the supremum,
of those.
∈
Call.
Upon reading a call symbol
a
c
∈ Σ
c
, the current states set
R
and the
current effect
S
is stored by pushing them, together with
a
c
,ontothestack.
While the set of current states is maintained by applying
a
c
via
δ
, the effect
relation is reset s.t. every state
q
maps to itself. The output is obtained in the
same way as by reading an internal action.
We let
δ
((
S,R
)
,a
c
,γ
)=(
Id
Q
,R
,
(
S,R,a
c
)
γ,
) such that
R
=
q
|∃
R,γ
,γ
,
:(
q
,γ
,
)
δ
(
q,a
c
,γ
)
{
q
∈
∈
}
=
|∃
R,γ
,γ
,q
:(
q
,γ
,
)
δ
(
q,a
c
,γ
)
{
q
∈
∈
}
