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
关键词
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
相关论文
共 50 条
  • [1] Heuristic Model Checking using a Monte-Carlo Tree Search Algorithm
    Poulding, Simon
    Feldt, Robert
    GECCO'15: PROCEEDINGS OF THE 2015 GENETIC AND EVOLUTIONARY COMPUTATION CONFERENCE, 2015, : 1359 - 1366
  • [2] Monte Carlo model checking
    Grosu, R
    Smolka, SA
    TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS, 2005, 3440 : 271 - 286
  • [3] UNIFORM OPTIMIZATION OF WEIGHT MONTE-CARLO ESTIMATES
    MIKHAILOV, GA
    ZHIGLIAVSKII, AA
    DOKLADY AKADEMII NAUK SSSR, 1988, 303 (02): : 290 - 293
  • [4] MONTE-CARLO SIMULATION OF A MODEL OF A SURFACTANT
    ABRAHAM, DB
    SMITH, ER
    JOURNAL OF PHYSICS A-MATHEMATICAL AND GENERAL, 1981, 14 (05): : L193 - L197
  • [5] MONTE-CARLO INVESTIGATION OF THE MITSUI MODEL
    ZINENKO, VI
    TOMSHINA, NG
    JOURNAL OF PHYSICS C-SOLID STATE PHYSICS, 1983, 16 (25): : 4997 - 5007
  • [6] A MONTE-CARLO STUDY OF THE XY MODEL
    FUCITO, F
    PHYSICS LETTERS A, 1983, 94 (02) : 99 - 102
  • [7] MONTE-CARLO MODEL OF PLASMA AFTERGLOW
    BLECHA, J
    VEIS, S
    ACTA PHYSICA SLOVACA, 1981, 31 (06) : 329 - 339
  • [8] MONTE-CARLO SIMULATION OF THE CUBIC MODEL
    SABLIK, MJ
    COOK, M
    VUONG, N
    PHANI, L
    ZAWONSKI, M
    PHANI, M
    JOURNAL OF APPLIED PHYSICS, 1979, 50 (11) : 7385 - 7387
  • [9] MONTE-CARLO MODEL OF TRACKING BEHAVIOR
    ADAMS, JA
    WEBBER, CE
    HUMAN FACTORS, 1963, 5 (01) : 81 - 102
  • [10] A MONTE-CARLO STUDY OF THE BNNNI MODEL
    AYDIN, M
    YALABIK, MC
    JOURNAL OF PHYSICS A-MATHEMATICAL AND GENERAL, 1989, 22 (18): : 3981 - 3989