location: Current position: Home >> Scientific Research >> Paper Publications

Genetic algorithm-based assume-guarantee reasoning for stochastic model checking

Hits:

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

Title of Paper:Genetic algorithm-based assume-guarantee reasoning for stochastic model checking

Journal:Proc. - IEEE/ACIS Int. Conf. Softw. Eng. Res., Manag. Appl., SERA

Abstract:Compositional stochastic model checking in the assume-guarantee style is a theoretically feasible way to alleviate the state explosion problem. The key for assume-guarantee reasoning is how to generate assumption. A main automated approach for assume-guarantee are based on learning assumptions. However, L∗-based learning assumptions for stochastic systems produces many intermediate results which need to be recorded. To overcome this, we propose a novel learning technique based on genetic algorithm for compositional stochastic model checking of Markov decision process, which is a randomized algorithm essentially. There are no intermediate results need to be recorded in the genetic algorithm-based learning algorithm, except the encoding of the problem domain and the training set. It can reduce the space complexity largely with respect to derivation algorithms. We implement a prototype tool for it and report encouraging results. © 2019 IEEE.

Translation or Not:no

Date of Publication:2019-05-01

Co-author:Ma, Yan,Liu, Yang

Correspondence Author:Cao Zi Ning

Pre One:A PSO-Based CEGAR Framework for Stochastic Model Checking

Next One:面向CPS的混成AADL建模与模型转换