Information Technology Reference
In-Depth Information
P(x
3
)
HMM in x
3
RVSE
AP-RVSE
RVPF
1.0
0.5
0.0
0
20
40
60
80
time t
P(x
3
)
HMM in x
3
RVSE
AP-RVSE
RVPF
1.0
0.5
0.0
0
20
40
60
80
time t
Fig. 8.
Estimation of probability of HMM state
x
3
with GF = 50% and GL = 1 before and after
correction through peek operations
the use of particles to estimate the Euclidean component, showing that this technique
works significantly better than standard PF.
Sistla
et al.
use PF to investigate the effectiveness of algorithms for monitorability
and strong monitorability of partially observable stochastic systems [8,9]. Familiarity
with PF is assumed and no further details, except for the number of particles used, are
provided. This application of PF is closest in nature to RVPF but there are significant
differences, as witnessed by the contrasting goals of RVPF. In particular, we seek to
show how PF can be a highly effective technique for runtime verification, and give a
detailed presentation of the RVPF algorithm and its experimental evaluation. Further-
more, we extend PF to handle gaps and peek events. Our experimental results, which
compare the accuracy and overhead of RVPF with those of RVSE [10] and approximate
precomputed RVSE [1], confirm RVPF's versatility.
The problem we consider—estimating the probability that a safety property is vio-
lated by a program execution when monitoring gaps may be present—was introduced
in [10]. There an optimal but compute-intensive solution based on the forward algo-
rithm was given. In this paper, we additionally consider
peek events
, which required us
to reformulate the problem in terms of DBNs. We also show how to enhance our RVPF
algorithm with the
sequential importance resampling
(SIR) strategy using an optimal
importance density function, to reduce the variance in state estimation in our setting.
