Bisimulation and Model Checking
State space minimization techniques are crucial for combating state explosion. A variety of verification tools use bisimulation minimization to check equivalence between systems, to minimize components before composition, or to reduce a state space prior to model checking. This paper explores the third use in the context of verifying invariant properties. We consider three bisimulation minimization algorithms. From each, we produce an on-the-fly model checker for invariant properties and compare this model checker to a conventional one based on backwards reachability. Our comparisons, both theoretical and experimental, lead us to conclude that bisimulation minimization does not appear to be viable in the context of invariance verification because performing the minimization requires as many, if not more, computational resources as model checking the unminimized system through backwards reachability.
- 1.Bouajjani, A., J.C. Fernandez and N. Halbwachs. Minimal model generation. In Proc. Intl. Conference on Computer-Aided Verification (CAV), pages 197–203. Springer-Verlag, 1990.Google Scholar
- 2.Fisler, K. and M. Y. Vardi. Bisimulation minimization in an automata-theoretic verification framework. In Proc. Intl. Conference on Formal Methods in Computer-Aided Design (FMCAD), pages 115–132. Springer-Verlag, 1998.Google Scholar
- 3.Fisler, K. and M.Y. Vardi. Bisimulation and model checking (extended version). Technical report TR99-339, Rice University, Department of Computer Science, 1999. Available at http://www.cs.rice.edu/CS/Verification/.
- 5.Lee, D. and M. Yannakakis. Online minimization of transition systems. In Proc. 24th ACM Symposium on Theory of Computing, pages 264–274, Victoria, May 1992.Google Scholar
- 8.The VIS Group. VIS: A system for verification and synthesis. In Proc. of the 8th Intl. Conference on Computer Aided Verification (CAV), pages 428–432. Springer Verlag, July 1996.Google Scholar