Abstract
Bisimulation is a seemingly attractive state-space minimization technique because it can be computed automatically and yields the smallest model preserving all µcalculus formulas. It is considered impractical for symbolic model checking, however, because the required BDDs are prohibitively large for most designs. We revisit bisimulation minimization, this time in an automata-theoretic framework. Bisimulation has potential in this framework because after intersecting the design with the negation of the property, minimization can ignore most of the atomic propositions. We compute bisimulation using an algorithm due to Lee and Yannakakis that represents bisimulation relations by their equivalence classes and only explores reachable classes. This greatly improves on the time and memory usage of naÏve algorithms.We demonstrate that bisimulation is practical for many designs within the automata-theoretic framework. In most cases, however, the cost of performing this reduction still outweighs that of conventional model checking.
Supported in part by NSF grants CDA-9625898, CCR-9628400 and CCR-9700061, and by a grant from the Intel Corporation.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
R. Alur, C. Courcoubetis, D. Dill, N. Halbwachs, and H. Wong-Toi. An implementation of three algorithms for timing verification based on automata emptiness. In Proc. of the IEEE Real-Time Systems Symposium, pages 157–166, 1992.
A. Aziz, V. Singhal, G.M. Swamy, and R.K. Brayton. Minimizing interacting finite state machines: A compositional approach to language containment. In Proc. of the International Conference on Computer Design (ICCD), 1994.
R. I. Bahar et al. Algebraic decision diagrams and their applications. In Proc. of the International Conference on Computer-Aided Design, pages 188–191, 1993.
I. Beer, S. Ben-David, D. Geist, R. Gewirtzman, and M. Yoeli. Methodology and system for practical formal verification of reactive hardware. In Proc. 6th Conference on Computer Aided Verification, volume 818 of Lecture Notes in Computer Science, pages 182–193, Stanford, June1994.
A. Bouajjani, J.-C. Fernandez, N. Halbwachs, P. Raymond, and C. Ratel. Minimal state graph generation. Science of Computer Programming, 18:247–269, 1992.
A. Bouali. XEVE, an ESTEREL verification environment. In Proc. of the International Conference on Computer-Aided Verification (CAV), pages 500–504, 1998.
A. Bouali and R. de Simone. Symbolic bisimulation minimization. In Proc. of the International Conference on Computer-Aided Verification (CAV), pages 96–108, 1992.
Y. Choueka. Theories of automata on Ω-tapes: A simplified approach. Journal of Computer and System Sciences, 8:117–141, 1974.
E.M. Clarke, R. Enders, T. Filkorn, and S. Jha. Exploiting symmetry in temporal logic model checking. Formal Methods in System Design, 9(1/2):77–104, August 1996.
E.M. Clarke, O. Grumberg, and D.E. Long. Model-checking and abstraction. In Proc. of the 19th ACM Symposium on Principles of Programming Languages, pages 343–354, 1992.
E.M. Clarke and R.P. Kurshan. Computer aided verification. IEEE Spectrum, 33:61–67, 1986.
C. Courcoubetis, M.Y. Vardi, P. Wolper, and M. Yannakakis. Memory efficient algorithms for the verification of temporal properties. Formal Methods in System Design, 1:275–288, 1992.
The CUDD package. Available from http://vlsi.colorado.edu/~fabio/.
D. Dams. Abstract Interpretation and Partition Refinement for Model Checking. PhD thesis, Technische Universiteit Eindhoven, 1996.
D. Dams, O. Grumberg, and R. Gerth. Generation of reduced models for checking fragments of CTL. In Proc. 5th Int.l Conference on Computer-Aided Verification, pages 479–490, 1993.
D. Dams, O. Grumberg, and R. Gerth. Abstract interpretation of reactive systems. ACM Transactions on Programming Languages and Systems (TOPLAS), 19(2), March 1997.
K. Fisler and M.Y. Vardi. Bisimulation minimization in an automata-theoretic verification framework (extended version). Technical report, Rice University, Department of Computer Science, 1998.
J.F. Groote and F. Vaandrager. An efficient algorithm for branching bisimulation and stuttering equivalence. In Proc. of the International Conference on Automata, Languages, and Programming, pages 626–638, 1990.
The VIS Group. VIS: A system for verification and synthesis. In R. Alur and T. Henzinger, editors, In the Proc. of the 8th International Conference on Computer Aided Verification, pages 428–432. Springer Verlag, July 1996.
O. Grumberg and D.E. Long. Model checking and modular verification. ACM Trans. on Programming Languages and Systems, 16(3):843–871, 1994.
V. Gyuris and A. P. Sistla. On-the-fly model checking under fairness that exploits symmetry. In Proc. of International Conference on Computer-Aided Verification (CAV), pages 232–243, 1997.
R. Hardin, R.P. Kurshan, S. Shukla, and M.Y. Vardi. A new heuristic for bad cycle detection using BDDs. In Proc. of the International Conference on Computer-Aided Verification, 1997.
M. Hennessy and R. Milner. Algebraic laws for nondeterminism and concurrency. Journal of ACM, 32:137–161, 1985.
T.A. Henzinger, O. Kupferman, and S. Rajamani. Fair simulation. In Proc. 8th Conference on Concurrency Theory, volume 1243 of Lecture Notes in Computer Science, pages 273–287, Warsaw, July 1997. Springer-Verlag.
C. N. Ip and D. L. Dill. Better verification through symmetry. Formal Methods in System Design, 9(1/2):41–76, August 1996.
A. Kick. Formula dependent model reduction through elimination of invisible transitions for checking fragments of CTL. Technical Report 1995–27, UniversitÄt Karlsruhe, 1995.
O. Kupferman and M.Y. Vardi. On the complexity of branching modular model checking. In Proc. 6th Conference on Concurrency Theory, volume 962 of Lecture Notes in Computer Science, pages 408–422, August 1995. Springer-Verlag.
R.P. Kurshan. Computer Aided Verification of Coordinating Processes. Princeton Univ. Press, 1994.
D. Lee and M. Yannakakis. Online minimization of transition systems. In Proc. 24th ACM Symposium on Theory of Computing, pages 264–274, May 1992.
David E. Long. Model-checking, Abstraction, and Compositional Verification. PhD thesis, Carnegie-Mellon University, 1993.
R. Milner. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer Verlag, Berlin, 1980.
S. Minato. Binary decision diagrams and applications for VLSI CAD. Kluwer Academic Publishers, 1996.
M.Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proc. First Symposium on Logic in Computer Science, pages 322–331, Cambridge, June 1986.
P. Wolper. Expressing interesting properties of programs in propositional temporal logic. In Proc. 13th ACM Symp. on Principles of Programming, pages 184–192, St. Petersburgh, January 1986.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Fisler, K., Vardi, M.Y. (1998). Bisimulation Minimization in an Automata-Theoretic Verification Framework. In: Gopalakrishnan, G., Windley, P. (eds) Formal Methods in Computer-Aided Design. FMCAD 1998. Lecture Notes in Computer Science, vol 1522. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-49519-3_9
Download citation
DOI: https://doi.org/10.1007/3-540-49519-3_9
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65191-8
Online ISBN: 978-3-540-49519-2
eBook Packages: Springer Book Archive