Monte Carlo Model Checking

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 and δ, MC2 takes N = ln(δ)/ ln(1 − ) random samples (random walks ending in a cycle, i.e lassos) from the B¨uchi automaton B = BS × B¬ϕ to decide if L(B) = ∅. Should a sample reveal an accepting lasso l, MC2 returns false with l as a witness. Otherwise, it returns true and reports that with probability less than δ, pZ < , where pZ 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 very well.

• Type: Conference
• Year: 2005
• Where: TACAS
• Authors: Radu Grosu, Scott A. Smolka
• Keywords: Accepting Lasso, Algorithms, TACAS 2005, Temporal Logic, Temporal Logic Holds