.png){kind=icon}
.png){kind=icon}
Return
A Probabilistic Assume-Guarantee Reasoning Framework Based on Genetic Algorithm
.png){kind=icon}
OA
AI
DOI：10.1109/ACCESS.2019.2924639.png)
.png){kind=icon}
.png){kind=icon}
Share.png){kind=icon}
Save
Abstract
En 中文
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.
Keywords:
Probabilistic assume-guarantee reasoning
genetic algorithm
interface alphabet
counterexample
stochastic model checking
AI Summary
Key information extracted from the uploaded paper, including a brief overview, abstract, background, key highlights, visual analysis, and future outlook.
Journal
IF:
3.6
Papers:
9.7W
Citations:
29.4W
Organization
No organization information available