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