Sagar Chaki

Sagar Chaki, Edmund Clarke, Nishant Sinha, Prasanna Thati, Proceedings of the 17th International Conference on Computer Aided Verification (CAV), LNCS 3576, page 534-547, July 6-10, 2005.

Abstract: We address the issue of efficiently automating assume-guarantee reasoning for simulation conformance between finite state systems and specifications. We focus on a non-circular assume-guarantee proof rule, and show that there is a weakest assumption that can be represented canonically by a deterministic tree automata (DTA). We then present an algorithm L^T that learns this DTA automatically in an incremental fashion, in time that is polynomial in the number of states in the equivalent minimal DTA. The algorithm assumes a teacher that can answer membership and candidate queries pertaining to the language of the unknown DTA. We show how the teacher can be implemented using a model checker. We have implemented this framework in the ComFoRT toolkit and we report encouraging results (over an order of magnitude improvement in memory consumption) on non-trivial benchmarks.