PCTL∗ stochastic model checking label-extended probabilistic Petri net system model

Stochastic model checking is using the verification method of model checking to quantitative verification system model with stochastic behaviours. In recent years, stochastic model checking make a great advancement. In this paper, the high level system model PPN is extended with label, and is used to as the formal model for system with stochastic behaviours; PCTL* is selected to as the property specification, which is strictly more expressive than PCTL and LTL with probability bounds. Then the PCTL* stochastic model checking algorithm for LPPN (label-extended probabilistic Petri net) is presented, and it is implemented in the visual tool which can model, simulation and stochastic model checking of LPPN. In the last, an illustrative example is used to demonstrate the feasibility of the algorithm and the tool.