Chinese Age Pension System and Analysis

DOI

10.2991/aebmr.k.201128.083How 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

© 2020, the Authors. Published by Atlantis Press.

Open Access

This is an open access article distributed under the CC BY-NC license (http://creativecommons.org/licenses/by-nc/4.0/).

Download article (PDF)

TY  - CONF
AU  - Congying Wang
PY  - 2020
DA  - 2020/11/30
TI  - Chinese Age Pension System and Analysis
BT  - Proceedings of the 2020 2nd International Conference on Economic Management and Cultural Industry (ICEMCI 2020)
PB  - Atlantis Press
SP  - 431
EP  - 439
SN  - 2352-5428
UR  - https://doi.org/10.2991/aebmr.k.201128.083
DO  - 10.2991/aebmr.k.201128.083
ID  - Wang2020
ER  -