Uniform Monte Carlo Model Checking

Title: Uniform Monte Carlo Model Checking

Speaker: Lei Song (MPI Saarbrücken and Saarland University)

Time: 15:00, 18 July 2013

Venue: Lecture Room, 3rd Floor, Building #5, State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences

In order to deal with the infamous state space explosion problem of LTL model checking, Grosu and Smolka proposed a Monte Carlo model

checking algorithm MC2 which is both time and memory efficient. The main idea of MC2 is to find an accepting lasso i.e. a path with a

cycle, in the given B\”{u}chi automaton by random walking. For each iteration, MC2 chooses a state randomly from the successors of the

current state until a lasso is found. In this way all the lassos cannot be sampled uniformly, it may happen that some lassos are

sampled for several times while others have not been sampled at all. Therefore in the models where the probability of the accepting lassos

being sampled is very low, MC2 will often terminate without finding them, and give us the wrong answer. We present in this paper a revised

algorithm of MC2 where we can guarantee that all the lassos will be “sampled” uniformly, thus each lasso will have the same chance to be

visited, and the algorithm will always return a more reliable answer than MC2.

Lei Song is a Post-Doc researcher associated with groups Automation of Logic of MPI Saarbrücken and Dependable Systems and Software of Saarland

University, under direction of Professor Holger Hermanns, since Nov. 2012. Before that, he was a PhD student working with Jens Chr. Godskesen

at IT University of Copenhagen and Flemming Nielson at Technical University of Denmark. His research interests include: Concurrency,

Probabilistic Process Algebra, Verification and Model Checking.