点击次数：

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

发表刊物：IEEE ACCESS

关键字：Probabilistic assume-guarantee reasoning genetic algorithm interface alphabet counterexample stochastic model checking

摘要：Probabilistic assume-guarantee reasoning is a theoretically feasible way to alleviate the state space explosion problem in stochastic model checking. The key to probabilistic assume-guarantee reasoning is how to generate the assumption. At present, the main way to automatically generate assumption is the L* (or symbolic L*) learning algorithm. An important limitation of it is that too many intermediate results are produced and need to be stored. To overcome this, we propose a novel assumption generation method by a genetic algorithm and present a probabilistic assume-guarantee reasoning framework for a Markov decision process (MDP). The genetic algorithm is a randomized algorithm essentially, and there are no intermediate results that need to be stored in the process of assumption generation, except the encoding of the problem domain and the training set. It can obviously reduce the space complexity of the probabilistic assume-guarantee reasoning framework. In order to improve the efficiency further, we combine the probabilistic assume-guarantee reasoning framework with interface alphabet refinement orthogonally. Moreover, we employ the diagnostic submodel as a counterexample for the guidance of augmenting training set. We implement a prototype tool for the probabilistic assume-guarantee reasoning framework and report the encouraging results.

ISSN号：2169-3536

是否译文：否

发表时间：2019-01-01

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

通讯作者：Liu, Yang,曹子宁