A Probabilistic Assume-Guarantee Reasoning Framework Based on Genetic Algorithm
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 i...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
IEEE
2019-01-01
|
| Series: | IEEE Access |
| Subjects: | |
| Online Access: | https://ieeexplore.ieee.org/document/8744527/ |
| _version_ | 1818415884309364736 |
|---|---|
| author | Yan Ma Zining Cao Yang Liu |
| author_facet | Yan Ma Zining Cao Yang Liu |
| author_sort | Yan Ma |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-12-14T11:42:05Z |
| format | Article |
| id | doaj.art-6f53022ccd0f456e9d16daf0f88d8675 |
| institution | Directory Open Access Journal |
| issn | 2169-3536 |
| language | English |
| last_indexed | 2024-12-14T11:42:05Z |
| publishDate | 2019-01-01 |
| publisher | IEEE |
| record_format | Article |
| series | IEEE Access |
| spelling | doaj.art-6f53022ccd0f456e9d16daf0f88d86752022-12-21T23:02:46ZengIEEEIEEE Access2169-35362019-01-017838398385110.1109/ACCESS.2019.29246398744527A Probabilistic Assume-Guarantee Reasoning Framework Based on Genetic AlgorithmYan Ma0Zining Cao1Yang Liu2https://orcid.org/0000-0001-6647-7950College of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing, ChinaCollege of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing, ChinaCollege of Information Engineering, Nanjing University of Finance and Economics, Nanjing, ChinaProbabilistic 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.https://ieeexplore.ieee.org/document/8744527/Probabilistic assume-guarantee reasoninggenetic algorithminterface alphabetcounterexamplestochastic model checking |
| spellingShingle | Yan Ma Zining Cao Yang Liu A Probabilistic Assume-Guarantee Reasoning Framework Based on Genetic Algorithm IEEE Access Probabilistic assume-guarantee reasoning genetic algorithm interface alphabet counterexample stochastic model checking |
| title | A Probabilistic Assume-Guarantee Reasoning Framework Based on Genetic Algorithm |
| title_full | A Probabilistic Assume-Guarantee Reasoning Framework Based on Genetic Algorithm |
| title_fullStr | A Probabilistic Assume-Guarantee Reasoning Framework Based on Genetic Algorithm |
| title_full_unstemmed | A Probabilistic Assume-Guarantee Reasoning Framework Based on Genetic Algorithm |
| title_short | A Probabilistic Assume-Guarantee Reasoning Framework Based on Genetic Algorithm |
| title_sort | probabilistic assume guarantee reasoning framework based on genetic algorithm |
| topic | Probabilistic assume-guarantee reasoning genetic algorithm interface alphabet counterexample stochastic model checking |
| url | https://ieeexplore.ieee.org/document/8744527/ |
| work_keys_str_mv | AT yanma aprobabilisticassumeguaranteereasoningframeworkbasedongeneticalgorithm AT ziningcao aprobabilisticassumeguaranteereasoningframeworkbasedongeneticalgorithm AT yangliu aprobabilisticassumeguaranteereasoningframeworkbasedongeneticalgorithm AT yanma probabilisticassumeguaranteereasoningframeworkbasedongeneticalgorithm AT ziningcao probabilisticassumeguaranteereasoningframeworkbasedongeneticalgorithm AT yangliu probabilisticassumeguaranteereasoningframeworkbasedongeneticalgorithm |