International Journal of Networked and Distributed Computing

Volume 8, Issue 2, March 2020, Pages 94 - 107

Compositional Stochastic Model Checking Probabilistic Automata via Assume-guarantee Reasoning

Authors
Yang Liu*, Rui Li
School of Information Engineering, Nanjing University of Finance & Economics, Nanjing, Jiangsu 210046, China
*Corresponding author. Email: yliu@nufe.edu.cn
Corresponding Author
Yang Liu
Received 4 April 2019, Accepted 1 May 2019, Available Online 9 April 2020.
DOI
https://doi.org/10.2991/ijndc.k.190918.001How to use a DOI?
Keywords
Stochastic model checking, assume-guarantee reasoning, symmetric assume-guarantee rule, learning algorithm, probabilistic automata
Abstract

Stochastic model checking is the extension and generalization of the classical model checking. Compared with classical model checking, stochastic model checking faces more severe state explosion problem, because it combines classical model checking algorithms and numerical methods for calculating probabilities. For dealing with this, we first apply symmetric assume-guarantee rule symmetric (SYM) for two-component systems and symmetric assume-guarantee rule for n-component systems into stochastic model checking in this paper, and propose a compositional stochastic model checking framework of probabilistic automata based on the NL* algorithm. It optimizes the existed compositional stochastic model checking process to draw a conclusion quickly, in cases the system model does not satisfy the quantitative properties. We implement the framework based on the PRISM tool, and several large cases are used to demonstrate the performance of it.

Copyright
© 2019 The Authors. Published by Atlantis Press SARL.
Open Access
This is an open access article distributed under the CC BY-NC 4.0 license (http://creativecommons.org/licenses/by-nc/4.0/).

Download article (PDF)
View full text (HTML)

Journal
International Journal of Networked and Distributed Computing
Volume-Issue
8 - 2
Pages
94 - 107
Publication Date
2020/04
ISSN (Online)
2211-7946
ISSN (Print)
2211-7938
DOI
https://doi.org/10.2991/ijndc.k.190918.001How to use a DOI?
Copyright
© 2019 The Authors. Published by Atlantis Press SARL.
Open Access
This is an open access article distributed under the CC BY-NC 4.0 license (http://creativecommons.org/licenses/by-nc/4.0/).

Cite this article

TY  - JOUR
AU  - Yang Liu
AU  - Rui Li
PY  - 2020
DA  - 2020/04
TI  - Compositional Stochastic Model Checking Probabilistic Automata via Assume-guarantee Reasoning
JO  - International Journal of Networked and Distributed Computing
SP  - 94
EP  - 107
VL  - 8
IS  - 2
SN  - 2211-7946
UR  - https://doi.org/10.2991/ijndc.k.190918.001
DO  - https://doi.org/10.2991/ijndc.k.190918.001
ID  - Liu2020
ER  -