Model Checking CSL for Markov Population Models

被引：2

作者：

Spieler, David ^{[1
]}

Hahn, Ernst Moritz ^{[2
]}

Zhang, Lijun ^{[2
]}

机构：

[1] Saarland Univ, Dept Comp Sci, Modeling & Simulat Grp, Saarbrucken, Germany

[2] Chinese Acad Sci, Inst Software, State Key Lab Comp Sci, Beijing, Peoples R China

来源：

ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE | 2014年 / 154期

基金：

中国国家自然科学基金;

关键词：

D O I：

10.4204/EPTCS.154.7

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

Markov population models (MPMs) are a widely used modelling formalism in the area of computational biology and related areas. The semantics of a MPM is an infinite-state continuous-time Markov chain. In this paper, we use the established continuous stochastic logic (CSL) to express properties of Markov population models. This allows us to express important measures of biological systems, such as probabilistic reachability, survivability, oscillations, switching times between attractor regions, and various others. Because of the infinite state space, available analysis techniques only apply to a very restricted subset of CSL properties. We present a full algorithm for model checking CSL for MPMs, and provide experimental evidence showing that our method is effective.

引用

页码：93 / 107

页数：15

共 50 条

[21] Diagnostic checking of Markov multiplicative error models
Guo, Bin
Li, Shuo
[J]. ECONOMICS LETTERS, 2018, 170 : 139 - 142
[22] Model Checking Interactive Markov Chains
Zhang, Lijun
Neuhaesser, Martin R.
[J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS, 2010, 6015 : 53 - +
[23] Model checking quantum Markov chains
Feng, Yuan
Yu, Nengkun
Ying, Mingsheng
[J]. JOURNAL OF COMPUTER AND SYSTEM SCIENCES, 2013, 79 (07) : 1181 - 1198
[24] Precisely deciding CSL formulas through approximate model checking for CTMCs
Feng, Yuan
Zhang, Lijun
[J]. JOURNAL OF COMPUTER AND SYSTEM SCIENCES, 2017, 89 : 361 - 371
[25] Prioritizing Methods to Accelerate Probabilistic Model Checking of Discrete-Time Markov Models
Mohagheghi, Mohammadsadegh
Karimpour, Jaber
Isazadeh, Ayaz
[J]. COMPUTER JOURNAL, 2020, 63 (01): : 105 - 122
[26] Backward bisimulation in Markov chain model checking
Sproston, Jeremy
Donatelli, Susanna
[J]. IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 2006, 32 (08) : 531 - 546
[27] Model Checking of Open Interval Markov Chains
Chakraborty, Souymodip
Katoen, Joost-Pieter
[J]. ANALYTICAL AND STOCHASTIC MODELLING TECHNIQUES AND APPLICATIONS, ASMTA 2015, 2015, 9081 : 30 - 42
[28] LTL Model Checking of Interval Markov Chains
Benedikt, Michael
Lenhardt, Rastislav
Worrell, James
[J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, TACAS 2013, 2013, 7795 : 32 - 46
[29] Model checking hyperproperties for Markov decision processes
Dobe, Oyendrila
Abraham, Erika
Bartocci, Ezio
Bonakdarpour, Borzoo
[J]. INFORMATION AND COMPUTATION, 2022, 289
[30] Bounded model checking for Markov decision processes
[J]. Zhou, C.-H. (chzhou@ujs.edu.cn), 1600, Science Press (36):

← 1 2 3 4 5 →