We present MC , what we believe to be the first randomized, Monte Carlo algorithm for temporal-logic model checking. Given a specification of a finite-state system, an LTL formula , and parameters and , MC takes random samples (random walks ending in a cycle, i.e lassos) from the Büchi automaton to decide if . Let be the expectation of an accepting lasso in . Should a sample reveal an accepting lasso , MC returns false with as a witness. Otherwise, it returns true and reports that the probability of finding an accepting lasso through further sampling, under the assumption that , is less than . It does so in time and space , where is 's recurrence diameter, using an optimal number of samples . Our experimental results demonstrate that MC is fast, memory-efficient, and scales extremely well.
In Proc. of TACAS'05, the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, April 2005, Edinburgh, UK.
*R. Grosu was partially supported by the NSF Faculty Early Career
Development Award CCR01-33583.