Automated assume-guarantee reasoning for simulation conformance. (English) Zbl 1081.68612

Chaki, Sagar; Clarke, Edmund; Sinha, Nishant; Thati, Prasanna

Etessami, Kousha (ed.) et al., Computer aided verification. 17th international conference, CAV 2005, Edinburgh, Scotland, UK, July 6–10, 2005. Proceedings. Berlin: Springer (ISBN 3-540-27231-3/pbk). Lecture Notes in Computer Science 3576, 534-547 (2005).

Summary: 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.
For the entire collection see [Zbl 1078.68004].

MSC:

68Q60	Specification and verification (program logics, model checking, etc.)
68Q32	Computational learning theory
68Q45	Formal languages and automata

Software:

ComFoRT