An assume-guarantee verification method has been recognized as a promising approach to verify
component-based software by model checking. This method is not only fitted to component-based software
but also has a potential to solve the state space explosion problem in model checking. The method allows us
to decompose a verification target into components so that we can model check each of them separately. In
this method, assumptions are seen as the environments needed for the components to satisfy a property and
for the rest of the system to be satisfied. The number of states of the assumptions should be minimized
because the computational cost of model checking is influenced by that number. Thus, we propose a method
for generating minimal assumptions for the assumeguarantee verification of component-based software. The
key idea of this method is finding the minimal assumptions in the search spaces of the candidate
assumptions. The minimal assumptions generated by the proposed method can be used to recheck the whole
system at much lower computational cost. We have implemented a tool for generating the minimal
assumptions. Experimental results are also presented and discussed. Copyright ?? 2010 The Institute of
Electronics, Information and Communication Engineers.
