Stochastic model checking can automatically verify and analyse the software-driven autonomous systems with stochastic behaviors, which is a formal verification technique based on system models. When coping with large-scale systems, it suffers from state space explosion problem very seriously. Model abstraction is a potential technique for mitigating this problem. At present, only a few properties specified by PCTL (Probabilistic Computation Tree Logic), such as probabilistic safety and probabilistic reachability, can be preserved in the practical model abstraction of stochastic model checking, which are the proper subset of PCTL* properties. For dealing with this, an effective and efficient three-valued model abstraction framework for full PCTL* stochastic model checking is proposed in this paper. We propose a new abstract model to preserve full PCTL* properties for nondeterministic and probabilistic system, which orthogonally integrates interval probability of transition and game for nondeterminism. A game-based three-valued PCTL* stochastic model checking algorithm is developed to verify abstract model, and a BPSO (binary particle swarm optimization) algorithm integrated with sample learning is designed to refine the indefinite result of three-valued PCTL* stochastic model checking abstract model. It is proved that full PCTL* properties are preserved when the result of three-valued stochastic model checking is definite, and the efficiency of this framework is demonstrated by some large cases.

Yang Liu

Shanghai Maritime University/National University of Singapore

Yan Ma

Nanjing University of Finance and Economics / National University of Singapore

Yongsheng Yang

Shanghai Maritime University