Uniform Monte-Carlo Model Checking

被引:0
作者
Oudinet, Johan [1 ,2 ]
Denise, Alain [1 ,2 ,3 ]
Gaudel, Marie-Claude [1 ,2 ]
Lassaigne, Richard [4 ,5 ]
Peyronnet, Sylvain [1 ,2 ,3 ]
机构
[1] Univ Paris Sud, Lab LRI, UMR8623, F-91405 Orsay, France
[2] CNRS, F-91405 Orsay, France
[3] INRIA Saclay, F-91893 Orsay, France
[4] Univ Paris 07, Equipe Logique Mathemat, F-75221 Paris 05, France
[5] CNRS, Paris Ctr, F-75000 Paris, France
来源
FUNDAMENTAL APPROACHES TO SOFTWARE ENGINEERING | 2011年 / 6603卷
关键词
SEARCH ALGORITHM; EXPLORATION;
D O I
暂无
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
Grosu and Smolka have proposed a randomised Monte-Carlo algorithm for LTL model-checking. Their method is based on random exploration of the intersection of the model and of the Buchi automaton that represents the property to be checked. The targets of this exploration are so-called lassos, i.e. elementary paths followed by elementary circuits. During this exploration outgoing transitions are chosen uniformly at random. Grosu and Smolka note that, depending on the topology, the uniform choice of outgoing transitions may lead to very low probabilities of some lassos. In such cases, very big numbers of random walks are required to reach an acceptable coverage of lassos, and thus a good probability either of satisfaction of the property or of discovery of a counter-example. In this paper, we propose an alternative sampling strategy for lassos in the line of the uniform exploration of models presented in sonic previous work. The problem of finding all elementary cycles in a directed graph is known to be difficult: there is no hope for a polynomial time algorithm. Therefore, we consider a well-known sub-class of directed graphs, namely the reducible flow graphs, which correspond to well-structured programs and most control-command systems. We propose an efficient algorithm for counting and generating uniformly lassos in reducible flowgraphs. This algorithm has been implemented and experimented on a pathological example. We compare the lasso coverages obtained with our new uniform method and with uniform choice among the outgoing transitions.
引用
收藏
页码:127 / +
页数:3
相关论文
共 21 条
[21]   Conformational sampling and structure prediction of multiple interacting loops in soluble and β-barrel membrane proteins using multi-loop distance-guided chain-growth Monte Carlo method [J].
Tang, Ke ;
Wong, Samuel W. K. ;
Liu, Jun S. ;
Zhang, Jinfeng ;
Liang, Jie .
BIOINFORMATICS, 2015, 31 (16) :2646-2652