A study of complex property counterexample generation method for markov model

作者：Ji, Mingyu; Chen, Zhiyuan; Li, Yanmei

来源：International Journal of Control and Automation, 2014, 7(2): 251-262.

DOI：10.14257/ijca.2014.7.2.24

• Automaton
• Computation methods
• Counter examples
• Generation algorithm
• Probabilistic computation tree logic
• Probabilistic modeling
• Probabilistic systems
• Until formula

With the wide application of probabilistic systems, the research of counterexample generation for probabilistic system with model checking has attracted wide attention. For counterexample of complex parametric system, proposes a counterexample generation algorithm for multiple until constraint formulae of probabilistic computation tree logic act on continuous time probabilistic model and gives another counterexample computation method based on automaton theory. At last, the example analysis is given. The theoretical analysis and example result show that the feasibility and validity of the method.

• 单位
  东北林业大学; 哈尔滨工程大学