Grosu/Smolka: Monte Carlo Model Checking
## Monte Carlo Model Checking*

*Radu Grosu and Scott A. Smolka*
We present
`MC`
,
what we believe to be the first randomized, Monte Carlo algorithm for
temporal-logic model checking. Given a specification
of a finite-state system, an LTL formula
, and parameters
and
, `MC` takes
random samples (random
walks ending in a cycle, i.e *lassos*) from the Büchi automaton
to decide if
. Let
be the
expectation of an accepting lasso in
. Should a sample reveal an accepting
lasso
, `MC` returns false with
as a witness. Otherwise, it returns true
and reports that the probability of finding an accepting lasso through further
sampling, under the assumption that
, is less than
.
It does so in time
and space
, where
is
's
recurrence diameter, using an optimal number of samples
. Our experimental
results demonstrate that `MC` 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.