# isola04

Grosu/Smolka: Quantitative Model Checking

## Quantitative Model Checking*

Radu Grosu and Scott A. Smolka

We present QMC, a one-sided error Monte Carlo decision procedure for the LTL model-checking problem . Besides serving as a randomized algorithm for LTL model checking, QMC delivers quantitative information about the likelihood that . In particular, given a specification of a finite-state system, an LTL formula , and parameters and , QMC performs random sampling to compute an estimate of the expectation that the language of the Büchi automaton is empty; is such that iff . A random sample in our case is a lasso, i.e. an initialized random walk through ending in a cycle. The estimate output by QMC is an -approximation of --one that is within a factor of with probability at least --and is computed using a number of samples that is optimal to within a constant factor, in expected time and expected space , where is 's recurrence diameter. Experimental results demonstrate that QMC is fast, memory-efficient, and scales extremely well.

In Proc. of ISoLa'04, the 1st International Symposium on Leveraging Applications of Formal Methods, November 2004, Paphos, Cyprus.

*R. Grosu was partially supported by the NSF Faculty Early Career Development Award CCR01-33583.