Sciweavers

Share
CAV
2005
Springer

Automated Assume-Guarantee Reasoning for Simulation Conformance

10 years 1 months ago
Automated Assume-Guarantee Reasoning for Simulation Conformance
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 LT 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.
Sagar Chaki, Edmund M. Clarke, Nishant Sinha, Pras
Added 26 Jun 2010
Updated 26 Jun 2010
Type Conference
Year 2005
Where CAV
Authors Sagar Chaki, Edmund M. Clarke, Nishant Sinha, Prasanna Thati
Comments (0)
books