点击次数：

所属单位：计算机科学与技术学院/人工智能学院/软件学院

发表刊物：Int. J. Software Engineer. Knowledge Engineer.

摘要：Counterexample-guided abstraction refinement (CEGAR) is an extremely successful methodology for combating the state-space explosion problem in model checking. State-space explosion problem is more serious in the field of stochastic model checking, and it is still a challengeable problem to apply CEGAR in stochastic model checking effectively. In this paper, we formalize the problem of applying CEGAR in stochastic model checking, and propose a novel CEGAR framework for it. In our framework, the abstract model is presented by a quotient probabilistic automaton by making a set of variables or latches invisible, which can distinguish more degrees of abstraction for each variable. The counterexample is described by a diagnostic sub-model. Validating counterexample is performed on diagnostic loop paths, and the directed explicit state-space search algorithm is used for searching diagnostic loop paths. Sample learning, particle swarm optimization algorithm (PSO) and some effective heuristics are integrated for refining abstract model guided by invalid counterexample. A prototype tool is implemented for the framework, and the feasibility and efficiency are shown by some large cases. © 2019 World Scientific Publishing Company.

ISSN号：0218-1940

是否译文：否

发表时间：2019-10-01

合写作者：Ma, Yan,Liu, Yang

通讯作者：曹子宁