Counterexample-Guided Assume-Guarantee Synthesis through Learning

Assume-guarantee reasoning (AGR) is a promising compositional verification technique that can address the state space explosion problem associated with model checking. Since the construction of assumptions usually requires nontrivial human efforts, a framework was already proposed for generating assumptions automatically using the L* algorithm. However, if the framework shows that a system model does not satisfy a given specification, the designer has to manually refine the system model. To automate this refinement process, we propose a framework that can automatically eliminate all counterexamples from a system model such that the synthesized model satisfies a given safety specification. Further, the framework for synthesis is not only automatic, but is also an iterative L*-based compositional process, i.e., the global state space of the system is never generated in the synthesis process. When a model checker shows that a system model does not satisfy a specification by giving a counterexample, the proposed framework eliminates a class of equivalent counterexamples, that is, the set of counterexamples that transit to the error state through the same final transition. Then, AGR is applied again to check if there is another counterexample. The action of eliminating counterexamples continues until all classes of counterexamples are eliminated from the system model. We prove that the synthesized model satisfies the specification and the synthesis flow terminates after a finite number of iterations. Due to compositional synthesis, our target model for synthesis, namely the component models, is much smaller than the global system state graph.