Statistical verification of probabilistic properties with unbounded until
Venue
Proceedings of the 13th Brazilian Symposium on Formal Methods, Springer, Berlin / Heidelberg (2010), pp. 144-160
Publication Year
2010
Authors
Håkan L. S. Younes, Edmund M. Clarke, Paolo Zuliani
BibTeX
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.
