Wed Jun 30, 11-12, 4549 Boelter Hall
Monte Carlo LTL model checking
Scott Smolka
SUNY Stony Brook
We present MC2, what we believe to be the first randomized,
Monte Carlo algorithm for temporal-logic model checking.
Given a specification S of a finite-state system,
an LTL formula phi, and parameters epsilon and delta,
MC2 takes M=log(delta)/\log(1-epsilon) random samples
(random walks ending in a cycle, i.e lassos)
from the Buechi automaton B=B_S x B_(not phi) to decide
if L(B)={}. Let p_Z be the expectation of an accepting lasso in B.
Should a sample reveal an accepting lasso l, MC2 returns false with l as a witness.
Otherwise, it returns true and reports that the probability of finding
an accepting lasso through further sampling, under the assumption that
p_Z >= epsilon, is less than delta.
It does so in time O(MD) and space O(D), where D is B's recurrence diameter,
using an optimal number of samples M.
Our experimental results demonstrate that MC2 is fast, memory-efficient,
and scales extremely well.
(joint work with Radu Grosu)
Host: Jens Palsberg