Grosu/Smolka: Monte Carlo Model Checking

Monte Carlo Model Checking*

Radu Grosu and Scott A. Smolka

We present MC$ ^2$ , what we believe to be the first randomized, Monte Carlo algorithm for temporal-logic model checking. 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$, MC$ ^2$ takes $ \small\tt M=\ln(\delta)/\ln(1-\epsilon)$ random samples (random walks ending in a cycle, i.e lassos) from the Büchi automaton $ \small\tt B=B_S \times B_{\neg\varphi}$ to decide if $ \small\tt L(B)=\emptyset$. Let $ \small\tt p_Z$ be the expectation of an accepting lasso in $ \small\tt B$. Should a sample reveal an accepting lasso $ \small\tt l$, MC$ ^2$ returns false with $ \small\tt l$ as a witness. Otherwise, it returns true and reports that the probability of finding an accepting lasso through further sampling, under the assumption that $ \small\tt p_Z\geq\epsilon$, is less than $ \small\tt\delta$. It does so in time $ \small\tt O(M{}D)$ and space $ \small\tt O(D)$, where $ \small\tt D$ is $ \small\tt B$'s recurrence diameter, using an optimal number of samples $ \small\tt M$. Our experimental results demonstrate that MC$ ^2$ is fast, memory-efficient, and scales extremely well.

In Proc. of TACAS'05, the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, April 2005, Edinburgh, UK.

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