Automated Assume-Guarantee Reasoning through Implicit Learning
Abstract
We propose a purely implicit solution to the contextual assumption generation problem in assume-guarantee reasoning. Instead of improving the L* algorithm — a learning algorithm for finite automata, our algorithm computes implicit representations of contextual assumptions by the CDNF algorithm — a learning algorithm for Boolean functions. We report three parametrized test cases where our solution outperforms the monolithic interpolation-based Model Checking algorithm.