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 10012-1185

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) 998-83101

Abstract

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 $\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, memory-efficient, and scales very well.