Model Checking CSLTA with Deterministic and Stochastic Petri Nets

被引：0
|
作者：
Amparore, Elvio Gilberto [1 ]
Donatelli, Susanna [1 ]
机构：
[1] Univ Turin, Dipartimento Informat, I-10124 Turin, Italy
来源：
2010 IEEE-IFIP INTERNATIONAL CONFERENCE ON DEPENDABLE SYSTEMS AND NETWORKS DSN | 2010年
关键词：
Stochastic Model Checking; DSPN; MARKOV-CHAINS;
D O I：
暂无
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
CSLTA is a stochastic temporal logic for continuous-time Markov chains (CTMC), that can verify the probability of following paths specified by a Deterministic Timed Automaton (DTA). A DTA expresses both logic and time constraints over a CTMC path, yielding to a very flexible way of describing performance and dependability properties. This paper explores a model checking algorithm for CSLTA based on the translation into a Deterministic and Stochastic Petri Net (DSPN). The algorithm has been implemented in a simple Model Checker prototype, that relies on existing DSPN solvers to do the actual numerical computations.
引用
收藏
页码：605 / 614
页数：10
相关论文
共 50 条
  • [31] Model checking Bounded Prioritized Time Petri Nets
    Berthomieu, Bernard
    Peres, Florent
    Vernadat, Francois
    [J]. AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, PROCEEDINGS, 2007, 4762 : 523 - +
  • [32] DSPNEXPRESS - A SOFTWARE PACKAGE FOR THE EFFICIENT SOLUTION OF DETERMINISTIC AND STOCHASTIC PETRI NETS
    LINDEMANN, C
    [J]. PERFORMANCE EVALUATION, 1995, 22 (01) : 3 - 21
  • [33] Efficient approximate transient analysis for a class of deterministic and stochastic Petri nets
    Ciardo, G
    Li, GZ
    [J]. IEEE INTERNATIONAL COMPUTER PERFORMANCE AND DEPENDABILITY SYMPOSIUM -PROCEEDINGS, 1998, : 34 - 43
  • [34] Performance Analysis of Manufacturing Systems Using Deterministic and Stochastic Petri Nets
    Haleh, Hassan
    Bahari, Arman
    Moody, Behnoosh
    [J]. JOURNAL OF MATHEMATICS AND COMPUTER SCIENCE-JMCS, 2014, 11 (01): : 1 - 12
  • [35] An efficient algorithm for the transient analysis of a class of Deterministic Stochastic Petri nets
    Gribaudo, M
    Sereno, M
    [J]. 2004 INTERNATIONAL CONFERENCE ON DEPENDABLE SYSTEMS AND NETWORKS, PROCEEDINGS, 2004, : 835 - 844
  • [36] Performance analysis of SoC communication by application of deterministic and stochastic Petri nets
    Blume, H
    von Sydow, T
    Noll, TG
    [J]. COMPUTER SYSTEMS: ARCHITECTURES, MODELING, AND SIMULATION, 2004, 3133 : 484 - 493
  • [37] Usability of Deterministic and Stochastic Petri Nets in the Wood Industry: A Case Study
    Horvath, Adam
    [J]. ADVANCED COMPUTATIONAL METHODS FOR KNOWLEDGE ENGINEERING, 2014, 282 : 119 - 127
  • [38] SEMICOMMUTATION AND DETERMINISTIC PETRI NETS
    OCHMANSKI, E
    [J]. LECTURE NOTES IN COMPUTER SCIENCE, 1990, 452 : 430 - 438
  • [39] Identification of deterministic Petri nets
    Cabasino, Maria Paola
    Giua, Alessandro
    Seatzu, Carla
    [J]. WODES 2006: EIGHTH INTERNATIONAL WORKSHOP ON DISCRETE EVENT SYSTEMS, PROCEEDINGS, 2006, : 325 - +
  • [40] STOCHASTIC PETRI NETS
    FLORIN, G
    NATKIN, S
    [J]. TSI-TECHNIQUE ET SCIENCE INFORMATIQUES, 1985, 4 (01): : 143 - 160
12345