Earticle

초록

영어

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.

목차

Abstract
 1. Introduction
 2. Probability model
 3. Temporal logic
 4. Counterexample of until Constraint Path Formula
 5. Automaton Computation Method
 6. Example Analysis
 7. Conclusion and Future Work
 Acknowledgements
 References

키워드

저자

• Mingyu Ji [ College of Information and Computer Engineering, Northeast Forestry University, Harbin 150040, China ]
• Zhiyuan Chen [ College of Computer Science and Technology, Harbin Engineering University, Harbin 150001, China ]
• Yanmei Li [ College of Computer Science and Technology, Harbin Engineering University, Harbin 150001, China ]

참고문헌

발행기관

간행물

표지보기 관심저널 등록

• 간행물명

  International Journal of Control and Automation

• 간기

  월간

• pISSN

  2005-4297

• 수록기간

  2008~2016

• 십진분류

  KDC 505 DDC 605