Please use this identifier to cite or link to this item: https://doi.org/10.1109/ACCESS.2019.2924639
Title: A Probabilistic Assume-Guarantee Reasoning Framework Based on Genetic Algorithm
Authors: Ma, Y.
Cao, Z.
Liu, Y. 
Keywords: counterexample
genetic algorithm
interface alphabet
Probabilistic assume-guarantee reasoning
stochastic model checking
Issue Date: 2019
Publisher: Institute of Electrical and Electronics Engineers Inc.
Citation: Ma, Y., Cao, Z., Liu, Y. (2019). A Probabilistic Assume-Guarantee Reasoning Framework Based on Genetic Algorithm. IEEE Access 7 : 83839-83851. ScholarBank@NUS Repository. https://doi.org/10.1109/ACCESS.2019.2924639
Rights: Attribution-NonCommercial-NoDerivatives 4.0 International
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. © 2013 IEEE.
Source Title: IEEE Access
URI: https://scholarbank.nus.edu.sg/handle/10635/210066
ISSN: 2169-3536
DOI: 10.1109/ACCESS.2019.2924639
Rights: Attribution-NonCommercial-NoDerivatives 4.0 International
Appears in Collections:Staff Publications
Elements

Show full item record
Files in This Item:
File Description SizeFormatAccess SettingsVersion 
10_1109_ACCESS_2019_2924639.pdf5.83 MBAdobe PDF

OPEN

NoneView/Download

SCOPUSTM   
Citations

3
checked on Sep 23, 2022

Page view(s)

52
checked on Sep 22, 2022

Google ScholarTM

Check

Altmetric


This item is licensed under a Creative Commons License Creative Commons