Reachability Assume-Guarantee

Model checking is a well known formal technique for systems verification and its main challenge is state explosion. Assume-guarantee is a promising way to deal with this challenge, but in the compositional reasoning process we should provide assumption for the model to be verified. Traditionally the assumption is given manually, which constrains its practice application. There are some automatic assumption generation ways based learning algorithm which are time consuming and inefficient. In this paper, we will introduce reachability assume-guarantee reasoning for property equal to some target states’ reachability. We will generate assumption automatically in liner time. The key idea of our approach is getting all the conditions what the property verification needs and which are contained in an automaton. And then we condense the automaton to a complete and non-redundant assumption. Finally we verify the assumption automaton on environment model. In our approach, we will improve the efficiency of assume-guarantee reasoning.