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 $ \small\tt S\models\varphi$. Besides serving as a randomized algorithm for LTL model checking, QMC delivers quantitative information about the likelihood that $ \small\tt S\models\varphi$. In particular, given a specification $ \small\tt S$ of a finite-state system, an LTL formula $ \small\tt\varphi$, and parameters $ \small\tt\epsilon$ and $ \small\tt\delta$, QMC performs random sampling to compute an estimate $ \small\tt\widetilde{p}_Z$ of the expectation $ \small\tt p_Z$ that the language $ \small\tt L(B)$ of the Büchi automaton $ \small\tt B=B_S \times B_{\neg\varphi}$ is empty; $ \small\tt B$ is such that $ \small\tt L(B)=\emptyset$ iff $ \small\tt S\models\varphi$. A random sample in our case is a lasso, i.e. an initialized random walk through $ B$ ending in a cycle. The estimate $ \small\tt\widetilde{p}_Z$ output by QMC is an $ \small\tt (\epsilon,\delta)$-approximation of $ \small\tt p_Z$--one that is within a factor of $ \small\tt 1 \pm \epsilon$ with probability at least $ \small\tt 1-\delta$--and is computed using a number of samples $ \small\tt N$ that is optimal to within a constant factor, in expected time $ \small\tt O(N \cdot D)$ and expected space $ \small\tt O(D)$, where $ \small\tt D$ is $ \small\tt B$'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.