Computer Science Colloquium
Monte Carlo Model Checking
Scott Smolka
SUNY Stony Brook
Friday, October 22, 2004 11:30 A.M.
Room 1302 Warren Weaver Hall
251 Mercer Street
New York, NY 100121185
Directions: http://cs.nyu.edu/csweb/Location/directions.html
Colloquium Information: http://cs.nyu.edu/csweb/Calendar/colloquium/index.html
Hosts:
Zvi Kedemkedem@cs.nyu.edu, (212) 99883101
Abstract
We present mc2, what we believe to be the first randomized, Monte Carlo
algorithm for temporallogic 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 finitestate
system, an LTL (Linear Temporal Logic) formula $\varphi$, and parameters
$\epsilon$ and $\delta$, mc2 takes $N=\ln(\delta)/\ln(1\epsilon)$
random samples (random walks ending in a cycle, i.e lassos) from the
Buechi automaton $B=B_S \times B_{\neg\varphi}$ to decide if
$L(B)=\emptyset$. Should a sample reveal an accepting lasso $l$, mc2
returns false with $l$ as a witness. Otherwise, it returns true and
reports with probability at least $1\delta$ that $p_Z < \epsilon$,
where $p_Z$ is the expectation of an accepting lasso in $B$. It does so
in time $O(N \cdot 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, memoryefficient, and scales very well.
top  contact webmaster@cs.nyu.edu
