A Markov chain model checker

被引：0
|
作者：
Hermanns, H
Katoen, JP
Meyer-Kayser, J
Siegle, M
机构：
[1] Univ Twente, Formal Methods & Tools Grp, NL-7500 AE Enschede, Netherlands
[2] Univ Erlangen Nurnberg, Lehrstuhl Informat 7, D-91058 Erlangen, Germany
来源：
TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS | 2000年 / 1785卷
关键词：
D O I：
暂无
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
Markov chains are widely used in the context of performance and reliability evaluation of systems of various nature. Model checking of such chains with respect to a given (branching) temporal logic formula has been proposed for both the discrete [17,6] and the continuous time setting [4,8]. In this paper, we describe a prototype model checker for discrete and continuous-time Markov chains, the Erlangen-Twente Markov Chain Checker (E proves MC2), where properties are expressed in appropriate extensions of CTL. We illustrate the general benefits of this approach and discuss the structure of the tool. Furthermore we report on first successful applications of the tool to non-trivial examples, highlighting lessons learned during development and application of E proves MC2.
引用
收藏
页码：347 / 362
页数：16
相关论文
共 50 条
  • [21] Model selection for hidden Markov chain
    Dortet-Bernadet, V
    COMPTES RENDUS DE L ACADEMIE DES SCIENCES SERIE I-MATHEMATIQUE, 2001, 332 (05): : 469 - 472
  • [22] A coarse-grained Markov chain is a hidden Markov model
    MacDonald, Iain L.
    PHYSICA A-STATISTICAL MECHANICS AND ITS APPLICATIONS, 2020, 541
  • [23] Markov chain model selection by misclassitied model probabilities
    Chen, Pai-Lien
    Sen, Pranab K.
    COMMUNICATIONS IN STATISTICS-THEORY AND METHODS, 2007, 36 (1-4) : 143 - 153
  • [24] INITIAL ENLARGEMENT IN A MARKOV CHAIN MARKET MODEL
    Gasbarra, Dario
    Morlanes, Jose Igor
    Valkeila, Esko
    STOCHASTICS AND DYNAMICS, 2011, 11 (2-3) : 389 - 413
  • [25] Research on the Risk Model Based on Markov Chain
    Cai Shuqin
    Wang Ge
    Liu Yan
    2008 ISECS INTERNATIONAL COLLOQUIUM ON COMPUTING, COMMUNICATION, CONTROL, AND MANAGEMENT, VOL 3, PROCEEDINGS, 2008, : 368 - +
  • [26] Validation of a Markov chain canopy reflectance model
    Kuusk, A
    Andrieu, B
    Chelle, M
    Aries, F
    INTERNATIONAL JOURNAL OF REMOTE SENSING, 1997, 18 (10) : 2125 - 2146
  • [27] Evaluation Method based on Markov Chain Model
    Liang, Li
    Qi-Sheng, Guo
    Xiu-yue, Yang
    7TH INTERNATIONAL CONFERENCE ON SYSTEM SIMULATION AND SCIENTIFIC COMPUTING ASIA SIMULATION CONFERENCE 2008, VOLS 1-3, 2008, : 1511 - 1514
  • [28] A Markov Chain Model for an EMS System with Repositioning
    Alanis, Ramon
    Ingolfsson, Armann
    Kolfal, Bora
    PRODUCTION AND OPERATIONS MANAGEMENT, 2013, 22 (01) : 216 - 231
  • [29] A Markov chain model of particle deposition in the lung
    Sonnenberg, Adam H.
    Herrmann, Jacob
    Grinstaff, Mark W.
    Suki, Bela
    SCIENTIFIC REPORTS, 2020, 10 (01)
  • [30] A Markov Chain Model for the Evolution of Sex Ratio
    Stark, Alan E.
    Seneta, Eugene
    TWIN RESEARCH AND HUMAN GENETICS, 2023, 26 (01) : 21 - 25
12345