Monte Carlo model checking

We present MC², what we believe to be the first randomized, Monte Carlo algorithm for temporal-logic model checking. Given a specification S of a finite-state system, an LTL formula φ, and parameters ε and δ, MC² takes M = ln(δ)/ ln(1 - ε) random samples (random walks ending in a cycle, i.e lassos) from the Büchi automaton B = B_s × B_¬φ to decide if L(B) = θ. Let pz be the expectation of an accepting lasso in B. Should a sample reveal an accepting lasso l, MC² returns false with 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 pz ≥ ε, is less than δ. It does so in time O(MD) and space O(D), where D is B's recurrence diameter, using an optimal number of samples M. Our experimental results demonstrate that MC² is fast, memory-efficient, and scales extremely well.