We present mc2, what we believe to be the first randomized, Monte Carlo algorithm for temporal-logic model checking, the classical problem of deciding whether or not a property specified in temporal logic holds of a system specification. Given a specification S of a finite-state system, an LTL (Linear Temporal Logic) formula , and parameters \epsilon and \delta , mc2 takes N=ln(\delta)/ln(1-\epsilon) random samples (random walks ending in a cycle, i.e lassos) from the Buechi automaton B=B_S × B_¬ to decide if L(B)=\emptyset. Should a sample reveal an accepting lasso l, mc2 returns false with l as a witness. Otherwise, it returns true and reports with probability at least 1-\delta that p_Z < \epsilon, where p_Z is the expectation of an accepting lasso in B. It does so in time O(N · D) and space O(D), where D is B's recurrence diameter, using a number of samples N that is optimal to within a constant factor. Our experimental results demonstrate that mc2 is fast, memory-efficient, and scales extremely well.

Joint work with Radu Grosu