Information Technology Reference
In-Depth Information
for HMM state estimation [7] is used to estimate the state of the HMM and the moni-
tor DFA. We extended the forward algorithm to handle observation gaps, by using the
HMM to estimate the unobserved states and events. The time complexity of the RVSE
algorithm for a single observation is
O
(
N
h
·
N
d
)
for a gap event, where
N
h
and
N
d
are the numbers of states of the HMM and the
DFA, respectively. The
approximately precomputed RVSE
(AP-RVSE) algorithm, de-
scribed briefly in Section 1, significantly reduces the runtime overhead of RVSE by pre-
computing and storing the results of the matrix calculations performed by RVSE [1].
N
d
) for a non-gap event and
O
(
N
h
·
3
Problem Statement
The problem statement is based closely on [10]. A problem instance is defined by an
HMM
H
modeling the monitored system, an observation sequence
o
1:
T
, and a temporal
property
φ
over sequences of actions of the monitored system.
The observation sequence contains events that are occurrences of actions performed
by the monitored system. In addition, it may contain the symbol
gap
(
L
) denoting a pos-
sible gap whose length is drawn from a length distribution
L
, a probability distribution
over the natural numbers:
L
(
) is the probability that the gap has length
. In the rest of
this paper, we consider a simpler definition of gaps, with gap symbols of form
gap
(
),
where the length
of each gap is encoded in the trace.
The HMM
H
models the monitored system. The HMM need not be an exact model
of the system; it simply embodies the available information about the system's behav-
ior. It can be learned automatically from complete traces using standard learning algo-
rithms [7]. Let
S
H
denote the set of states of the HMM, i.e., the set of possible values
of its state variable.
The property
φ
is represented by a DFA
M
=
, consisting of a
set
S
M
of states, an initial state
m
init
, an alphabet
A
, a transition relation
δ
,andaset
F
of final (also called “accepting”) states. The alphabet
A
is a subset of the observable
actions of the HMM; actions not in
A
leave the DFA's state unchanged.
1
The goal is to compute
P
(
φ
S
M
,m
init
,A,δ,F
o
1:
T
), that is, the probability that the system's behavior
satisfies
φ
, given observation sequence
o
1:
T
. This probability is computed from the
probability distribution on composite states, where a
composite state
(
x,s
) is a pair
containing an HMM state
x
and a DFA state
s
. Specifically,
P
(
φ
|
o
1:
t
)=
x
t
∈S
H
,s
t
∈F
P
(
x
t
,s
t
|
o
1:
t
)
/
x
t
∈S
H
,s
t
∈S
M
P
(
x
t
,s
t
|
|
o
1:
t
)
where
P
(
x
t
,s
t
|
o
1:
t
) is the probability that the HMM is in state
x
t
and the DFA is in
state
s
t
after observation sequence
o
1:
t
.
4
System Model
The composition of the HMM
H
modeling the monitored system and the monitor DFA
M
defines a DBN
D
representing the entire system. This DBN is illustrated in Figure 1.
It shows dependencies among the state variables and observation variables during the
t
'th time step as well as the dependencies of the state variables
X
t
and
S
t
from the
1
In Section 5 we use a different, HMM-like notation for the DFA.
