Statistical verification of probabilistic properties with unbounded until
Abstract
We consider statistical (sampling-based) solution methods for verifying
probabilistic properties with unbounded until. Statistical solution methods
for probabilistic verification use sample execution trajectories for a system
to verify properties with some level of confidence. The main challenge with
properties that are expressed using unbounded until is to ensure termination
in the face of potentially infinite sample execution trajectories. We describe
two alternative solution methods, each one with its own merits. The first method
relies on reachability analysis, and is suitable primarily for large Markov
chains where reachability analysis can be performed efficiently using symbolic
data structures, but for which numerical probability computations are expensive.
The second method employs a termination probability and weighted sampling. This
method does not rely on any specific structure of the model, but error control
is more challenging. We show how the choice of termination probability—when
applied to Markov chains—is tied to the subdominant eigenvalue of the
transition probability matrix, which relates it to iterative numerical solution
techniques for the same problem.
Sample citation
Håkan L. S. Younes,
Edmund M. Clarke, and
Paolo Zuliani. 2010.
Statistical verification of probabilistic properties with unbounded until. In
Proceedings of the 13th Brazilian Symposium on Formal Methods, edited by Jim Davies, Leila Silva, and Adenilso Simao, vol. 6527 of
Lecture Notes in Computer Science, 144–160, Natal, Brazil. Springer.
Full paper