CSL model checking for generalized Stochastic Petri Nets

被引：0

作者：

Cerotti, Davide ^{[1
]}

Donatelli, Susanna ^{[1
]}

Horvath, Andras ^{[1
]}

Sproston, Jeremy ^{[1
]}

机构：

[1] Univ Turin, Dipartimento Informat, I-10149 Turin, Italy

来源：

QEST 2006: THIRD INTERNATIONAL CONFERENCE ON THE QUANTITATIVE EVALUATION OF SYSTEMS | 2006年

关键词：

D O I：

暂无

中图分类号：

C93 [管理学]; O22 [运筹学];

学科分类号：

070105 ; 12 ; 1201 ; 1202 ; 120202 ;

摘要：

This paper presents a Continuous Stochastic Logic (CSL) model-checking algorithm for Generalized Stochastic Petri Nets (GSPNs). CSL is a temporal logic defined over Continuous Time Markov Chains (CTMCs). GSPNs are a class of Stochastic Petri Nets in which sojourn times in states are either exponentially distributed (tangible states) or deterministically zero (vanishing states). Although vanishing states have zero probabilities, they can be relevant for the definition of system properties expressed as CSL formulae: the semantics Of CSL is therefore modified accordingly. The paper then shows how the set of GSPN states which satisfy a CSL-formula can be computed through the solution of CTMCs produced front a series of embedded Discrete Time Markov Chains modified according to the formula being checked.

引用

页码：199 / +

页数：2

共 50 条

[31] Towards TCTLhΔ model checking of Time Petri Nets
Chtourou, Ameni
Sbai, Zohra
[J]. 2016 INTERNATIONAL CONFERENCE ON CONTROL, DECISION AND INFORMATION TECHNOLOGIES (CODIT), 2016, : 563 - 568
[32] Symbolic model checking of dual transition Petri nets
Varea, M
Al-Hashimi, BM
Cortés, LA
Eles, P
Peng, Z
[J]. CODES 2002: PROCEEDINGS OF THE TENTH INTERNATIONAL SYMPOSIUM ON HARDWARE/SOFTWARE CODESIGN, 2002, : 43 - 48
[33] Model Checking Branching Properties on Petri Nets with Transits
Finkbeiner, Bernd
Gieseking, Manuel
Hecking-Harbusch, Jesko
Olderog, Ernst-Rudiger
[J]. AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS (ATVA 2020), 2020, 12302 : 394 - 410
[34] Model checking Bounded Prioritized Time Petri Nets
Berthomieu, Bernard
Peres, Florent
Vernadat, Francois
[J]. AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, PROCEEDINGS, 2007, 4762 : 523 - +
[35] Compositional model checking of concurrent systems, with Petri nets
Sobocinski, Pawel
[J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2016, (204): : 19 - 30
[36] Exploiting stochastic process algebra achievements for generalized stochastic Petri nets
Hermanns, H
Herzog, U
Mertsiotakis, V
Rettelbach, M
[J]. PROCEEDINGS OF THE SEVENTH INTERNATIONAL WORKSHOP ON PETRI NETS AND PERFORMANCE MODELS, 1997, : 183 - 192
[37] Evolution and Decision Model of Major Infectious Disease Based on Generalized Stochastic Petri Nets
Qiao, Xiaojiao
Wang, Xunqing
Xu, Fangchao
[J]. 2016 13TH INTERNATIONAL CONFERENCE ON SERVICE SYSTEMS AND SERVICE MANAGEMENT, 2016,
[38] Analyzing attack trees using generalized stochastic Petri nets
Dalton, George C., II
Mills, Robert F.
Colombi, John M.
Raines, Richard A.
[J]. 2006 IEEE INFORMATION ASSURANCE WORKSHOP, 2006, : 116 - +
[39] On Quantitative Properties Preservation in Reconfigurable Generalized Stochastic Petri Nets
Tigane, Samir
Kahloul, Laid
Hamani, Nadia
Khalgui, Mohamed
Ali, Masood Ashraf
[J]. IEEE TRANSACTIONS ON SYSTEMS MAN CYBERNETICS-SYSTEMS, 2023, 53 (06): : 3311 - 3323
[40] Modeling of Testability Requirement Based on Generalized Stochastic Petri Nets
苏永定
邱静
刘冠军
钱彦岭
[J]. Defence Technology, 2009, 5 (01) : 60 - 64

← 1 2 3 4 5 →