Runtime Verification with Particle Filtering - Runtime Verification - page 154

previous states X t− 1 and S t− 1 , respectively. These relationships hold for consecutive
observations, without gaps.

Fig. 1. DBN D composed from the HMM H and the monitor DFA M . X t and O t denote the
state and observation variables of H at time t , respectively, and S t denotes the state variables of
M , at time t . Note that O t is also M 's input.

4.1 Peek Operations

When a gap occurs, the missing observations cause uncertainty in the state of the DFA.
Our algorithm performs a peek operation, which is a lightweight procedure that inspects
a part of the monitored system's state immediately after a gap, and can be regarded as an
event which is used to reduce the uncertainty in the state of the DFA. Which part of the
program state is considered during a peek operation depends on the particular problem
and is built into the definition of the procedure that implements the peek operation.
Specifically, peek events are useful for applications in which certain DFA states are
known to be inconsistent with certain program states. In such situations, the probabili-
ties associated with composite states containing DFA states which are inconsistent with
the partial program state provided by the peek operation can be zeroed, after which the
probabilities associated with other composite states are renormalized so that they sum
to 1. The additional dependencies between the variables are represented by the DBN in
Figure 2.
Because our algorithm uses peek events to reduce uncertainty in the DFA state, we
characterize the result of a peek operation q t by a probability distribution P ( Q t | S t ),

which is the probability that a peek operation returns Q t given that the DFA is in state
S t . Using Bayes' rule, after a peek operation that returns q t after a gap, the probability
that the DFA is in state s t is P ( s t |

s t ) P ( s t ),where α is a constant
factor used for normalization, and P ( s t ) is the probability that the DFA is in state s t
after processing the gap and before processing the peek event.
We do not directly use peek events to reduce uncertainty in the state of the HMM,
because generally we do not know a correspondence between concrete program states
(provided by peek events) and states of the HMM. This is because the HMM is typically
an abstract model learned automatically from traces. However, if such a correspondence
is known, then peek events can be used to reduce uncertainty in the state of the HMM,
in the same way they are used to reduce uncertainty in the state of the DFA.

q t )= α P ( q t |