Current automated approaches for compositional model checking in the assume-guarantee style are based on learning of assumptions as deterministic automata. We propose an alternative approach based on abstraction refinement. Our new method computes the assumptions for the assume-guarantee rules as conservative and not necessarily deterministic abstractions of some of the components, and refines those abstractions using counterexamples obtained from model checking them together with the other components. Our approach also exploits the alphabets of the interfaces between components and performs iterative refinement of those alphabets as well as of the abstractions. We show experimentally that our preliminary implementation of the proposed alternative achieves similar or better performance than a previous learning-based implementation. © 2008 Springer-Verlag.
CITATION STYLE
Gheorghiu Bobaru, M., Pǎsǎreanu, C. S., & Giannakopoulou, D. (2008). Automated assume-guarantee reasoning by abstraction refinement. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5123 LNCS, pp. 135–148). https://doi.org/10.1007/978-3-540-70545-1_14
Mendeley helps you to discover research relevant for your work.