Form Methods Syst Des (2008) 32: 267–284 DOI 10.1007/s10703-007-0042-5 Three optimizations for Assume–Guarantee reasoning with L∗

Abstract The learning-based automated Assume–Guarantee reasoning paradigm has been applied in the last few years for the compositional verification of concurrent systems. Specif-ically, L ∗ has been used for learning the assumption, based on strings derived from coun-terexamples, which are given to it by a model-checker that attempts to verify the Assume– Guarantee rules. We suggest three optimizations to this paradigm. First, we derive from each counterexample multiple strings to L∗, rather than a single one as in previous approaches. This small improvement saves candidate queries and hence model-checking runs. Second, we observe that in existing instances of this paradigm, the learning algorithm is coupled weakly with the teacher. Thus, the learner completely ignores the details of the internal structure of the system and specification being verified, which are available already to the teacher. We suggest an optimization that uses this information in order to avoid many un-necessary membership queries (it reduces the number of such queries by more than an order of magnitude). Finally, we develop a method for minimizing the alphabet used by the as-sumption, which reduces the size of the assumption and the number of queries required to construct it. We present these three optimizations in the context of verifying trace contain-ment for concurrent systems composed of finite state machines. We have implemented our approach in the COMFORT tool, and experimented with real-life examples. Our results ex-hibit an average speedup of between 4 to 11 times, depending on the Assume–Guarantee rule used and the set of activated optimizations