¹College of Information and Computer Engineering, Northeast Forestry University, Harbin, China
²College of Computer Science and Technology, Harbin Engineering University, Harbin, China

---

Abstract—with the wide application of probabilistic systems, the performance analysis for probabilistic system with model checking have attracted wide attention. For conditional probability formulae of complex parametric system, this paper proposes a counterexample generation method of conditional probability properties based on continuous time probabilistic model. We use continuous time Markov reward model with comprehensive feature representation ability as the system model need to be verified, give satisfiability probability solution algorithm of probabilistic computation tree logic multiple constraints until formulae path properties after model pretreatment, put forward the counterexample generation method of conditional probability on multiple constraints until formulae and give the example analysis. The theoretical analysis and example result show that the feasibility and validity of the method.

Index Terms—probabilistic system, performance analysis, model checking, conditional probability, counterexample generation

[PDF]

Cite: Mingyu Ji, Di Wu, Yanmei Li, Zhiyan Chen, "Counterexample Generation for Conditional Probability in Probabilistic Model Checking," Journal of Computers vol. 8, no. 11, pp. 3272-3279, 2013.