View article

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 p _Z 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 p _Z ≥ ε, 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 …