Hits:

Affiliation of Author(s):计算机科学与技术学院/人工智能学院/软件学院

Title of Paper:A Probabilistic Assume-Guarantee Reasoning Framework Based on Genetic Algorithm

Journal:IEEE ACCESS

Key Words:Probabilistic assume-guarantee reasoning genetic algorithm interface alphabet counterexample stochastic model checking

Abstract: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 No.:2169-3536

Translation or Not:no

Date of Publication:2019-01-01

Co-author:Ma, Yan,Liu, Yang

Correspondence Author:Liu, Yang,Cao Zi Ning