## An Assume-Guarantee Rule for Checking Simulation

*
Thomas A. Henzinger, Shaz Qadeer, Sriram K. Rajamani, and
Serdar Tasiran*

The simulation preorder on state transition systems is widely accepted
as a useful notion of refinement, both in its own right and as an
efficiently checkable sufficient condition for trace containment. For
composite systems, due to the exponential explosion of the state
space, there is a need for decomposing a simulation check of the form
*P < Q*, denoting "*P* is simulated by *Q*," into
simpler simulation checks on the components of *P* and *Q*.
We present an assume-guarantee rule that enables such a decomposition.
To the best of our knowledge, this is the first assume-guarantee rule
that applies to a refinement relation different from trace
containment. Our rule is circular, and its soundness proof requires
induction on trace trees. The proof is constructive: given simulation
relations that witness the simulation preorder between corresponding
components of *P* and *Q*, we provide a procedure for
constructing a witness relation for *P < Q*. We also extend our
assume-guarantee rule to account for fairness constraints on
transition systems.

*ACM Transactions on Programming Languages and Systems* 24:51-64, 2002.
A preliminary version appeared in the
*Proceedings of the
Second International Conference on Formal Methods in Computer-Aided Design*
(FMCAD),
Lecture Notes in Computer Science 1522,
Springer, 1998, pp. 421-432.

Download inofficial, sometimes updated
PostScript /
PDF document.
© 1998 Springer,
2002 ACM.