Linking Theorem Proving and Model-Checking with Well-Founded Bisimulation
Panagiotis Manolios, Kedar Namjoshi, and Robert Sumners.
Technical Report TR-99-02, University of Texas at Austin, Department of Computer Sciences,
Austin, TX, January 1999. (Superseded by the CAV article).
We present an approach to verification that combines the strengths of model-checking and theorem proving. We use theorem proving to show a bisimulation up to stuttering on a---potentially infinite-state---system. Our characterization of stuttering bisimulation allows us to do such proofs by reasoning only about single steps of the system. We present an on-the-fly method that extracts the quotient induced by the bisimulation, for finite quotients. If our specification is a temporal logic formula, we model-check the quotient. If our specification is a simpler system, we use an equivalence checker to show that the quotient is stuttering bisimilar to the simpler system. We lift the results obtained on the quotient to the original system by showing that the original system is a branching-time refinement of the extracted quotient.
We demonstrate our methodology by verifying the alternating bit
protocol. This protocol cannot be directly model-checked because it
has an infinite-state space; however, using the theorem prover ACL2,
we show that the protocol is stuttering bisimilar to a small
finite-state system, which we model-check. We also show that the
alternating bit protocol is a refinement of a non-lossy system.
Gzipped Postscript (86K)
Compressed Postscript (116K)