%0 Journal Article %1 sagar2005automated %A Chaki, Sagar %A Clarke, Edmund %A Sinha, Nishant %A Thati, Prasanna %D 2005 %J Computer Aided Verification %K automated compositional finite_state machine_learning safety verification %P 534--547 %T Automated Assume-Guarantee Reasoning for Simulation Conformance %U http://dx.doi.org/10.1007/11513988_51 %X 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. ER -

@article{sagar2005automated, 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. ER -}, added-at = {2010-01-27T11:36:16.000+0100}, author = {Chaki, Sagar and Clarke, Edmund and Sinha, Nishant and Thati, Prasanna}, biburl = {https://www.bibsonomy.org/bibtex/2c06e70986cd92776608a36b4c36e7031/giuliano.losa}, description = {Automated Assume-Guarantee Reasoning for Simulation Conformance}, interhash = {bb9e68a36c4f96748f23200ea772679d}, intrahash = {c06e70986cd92776608a36b4c36e7031}, journal = {Computer Aided Verification}, keywords = {automated compositional finite_state machine_learning safety verification}, pages = {534--547}, timestamp = {2010-01-27T12:29:44.000+0100}, title = {Automated Assume-Guarantee Reasoning for Simulation Conformance}, url = {http://dx.doi.org/10.1007/11513988_51}, year = 2005 }