Grosu/Smolka: Quantitative Model Checking
Quantitative Model Checking*
Radu Grosu and Scott A. Smolka
We present QMC, a one-sided error Monte Carlo decision procedure for
the LTL model-checking problem
. Besides
serving as a randomized algorithm for LTL model checking, QMC delivers
quantitative information about the likelihood that
. In particular, given a specification
of a finite-state system, an LTL formula
, and
parameters
and
, QMC performs
random sampling to compute an estimate
of
the expectation
that the language
of
the Büchi automaton
is
empty;
is such that
iff
. A random sample in our case is a lasso,
i.e. an initialized random walk through 
ending in a cycle. The
estimate
output by QMC is an
-approximation of
--one that is
within a factor of
with probability at
least
--and is computed using a number of samples
that is optimal to within a constant factor, in expected
time
and expected space
,
where
is
's recurrence diameter.
Experimental results demonstrate that QMC is fast, memory-efficient,
and scales extremely well.
In Proc. of ISoLa'04, the 1st International Symposium on Leveraging
Applications of Formal Methods, November 2004, Paphos, Cyprus.
*R. Grosu was partially supported by the NSF Faculty Early Career
Development Award CCR01-33583.