Symbolic model checking for probabilistic processes

被引:0
|
作者
Baier, C [1 ]
Clarke, EM
Hartonas-Garmhausen, V
Kwiatkowska, M
Ryan, M
机构
[1] Univ Mannheim, Fak Math & Informat, D-6800 Mannheim, Germany
[2] Carnegie Mellon Univ, Dept Comp Sci, Pittsburgh, PA 15213 USA
[3] Univ Birmingham, Sch Comp Sci, Birmingham B15 2TT, W Midlands, England
来源
关键词
D O I
暂无
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
We introduce a symbolic model checking procedure fur Probabilistic Computation Tree Logic PCTL over labelled Markov chains as models. Model checking for probabilistic logics typically involves solving linear equation systems in order to ascertain the probability of a given formula holding in a state. Our algorithm is based on the idea of representing the matrices used in the linear equation systems by Multi-Terminal Binary Decision Diagrams (MTBDDs) introduced in Clarke et al [14]. Our procedure, based on the algorithm used by Hansson and Jonsson [24], uses BDDs to represent formulas and MTBDDs to represent Markov chains, and is efficient because it avoids explicit state space construction. A PCTL model checker is being implemented in Verus [9].
引用
收藏
页码:430 / 440
页数:11
相关论文
共 50 条
  • [1] Symbolic model checking of probabilistic processes using MTBDDs and the Kronecker representation
    de Alfaro, L
    Kwiatkowska, M
    Norman, G
    Parker, D
    Segala, R
    [J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, 2000, 1785 : 395 - 410
  • [2] Symbolic model checking for probabilistic timed automata
    Kwiatkowska, Marta
    Norman, Gethin
    Sproston, Jeremy
    Wang, Fuzhi
    [J]. INFORMATION AND COMPUTATION, 2007, 205 (07) : 1027 - 1077
  • [3] Advances in Symbolic Probabilistic Model Checking with PRISM
    Klein, Joachim
    Baier, Christel
    Chrszon, Philipp
    Daum, Marcus
    Dubslaff, Clemens
    Klueppelholz, Sascha
    Maercker, Steffen
    Mueller, David
    [J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS (TACAS 2016), 2016, 9636 : 349 - 366
  • [4] Symbolic Model Checking for Factored Probabilistic Models
    Deininger, David
    Dimitrova, Rayna
    Majumdar, Rupak
    [J]. AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, ATVA 2016, 2016, 9938 : 444 - 460
  • [5] Symbolic model checking for probabilistic timed automata
    Kwiatkowska, M
    Norman, G
    Sproston, J
    Wang, FZ
    [J]. FORMAL TECHNIQUES, MODELLING AND ANALYSIS OF TIMED AND FAULT-TOLERANT SYSTEMS, PROCEEDINGS, 2004, 3253 : 293 - 308
  • [6] Probabilistic symbolic model checking with PRISM: A hybrid approach
    Kwiatkowska, M
    Norman, G
    Parker, D
    [J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANAYLSIS OF SYSTEMS, PROCEEDINGS, 2002, 2280 : 52 - 66
  • [7] Probabilistic symbolic model checking with PRISM: A hybrid approach
    Kwiatkowska M.
    Norman G.
    Parker D.
    [J]. International Journal on Software Tools for Technology Transfer, 2004, 6 (2) : 128 - 142
  • [8] Dual-processor parallelisation of symbolic probabilistic model checking
    Kwiatkowska, M
    Parker, D
    Zhang, Y
    [J]. IEEE COMPUTER SOCIETY'S 12TH ANNUAL INTERNATIONAL SYMPOSIUM ON MODELING, ANALYSIS, AND SIMULATION OF COMPUTER AND TELECOMMUNICATIONS SYSTEMS - PROCEEDINGS, 2004, : 123 - 130
  • [9] A Comparative Study of BDD Packages for Probabilistic Symbolic Model Checking
    van Dijk, Tom
    Hahn, Ernst Moritz
    Jansen, David N.
    Li, Yong
    Neele, Thomas
    Stoelinga, Marielle
    Turrini, Andrea
    Zhang, Lijun
    [J]. DEPENDABLE SOFTWARE ENGINEERING: THEORIES, TOOLS, AND APPLICATIONS, SETTA 2015, 2015, 9409 : 35 - 51
  • [10] Probabilistic Model Checking of BPMN Processes at Runtime
    Falcone, Ylies
    Salaun, Gwen
    Zuo, Ahang
    [J]. INTEGRATED FORMAL METHODS, IFM 2022, 2022, 13274 : 191 - 208