Optimization techniques for BDD-based bisimulation computation

ABSTRACT

In this paper we report on optimizations for a BDD-based algorithm for the computation of bisimulations. The underlying algorithmic principle is an iterative refinement of a partition of the state space. The proposed optimizations demonstrate that both, taking into account the algorithmic structure of theproblem and the exploitation of the BDD-based representation, are essential to finally obtain an efficient symbolic algorithm for real-world problems. The contributions of this paper are (1) block forwarding to update block refinement as soon as possible, (2) split-driven refinement that over-approximates the set of blocks that must definitely be refined, and (3) block ordering to fix the order of the blocks for the refinement in a clever way. We provide substantial experimental results on examples from different applications and compare them to alternative approaches when possible. The experiments clearly show that the proposed optimization techniques result in a significant performance speed-up compared to the basic algorithm as well as to alternative approaches.

REFERENCES

• 1: ARP 4761. Guidelines and Methods for Conducting the Safety Assessment Process on Civil Airborne Systems and Equipment. Aerospace Recommended Practice, Society of Automotive Engineers, Detroit, USA, 1996.
• 2: S. Blom and S. Orzan. Distributed branching bisimulation reduction of state spaces. In Proc. of PDMC'03, volume 89 of ENTCS, 2003.
• 3: Eckard Bode , Marc Herbstritt , Holger Hermanns , Sven Johr , Thomas Peikenkamp , Reza Pulungan , Ralf Wimmer , Bernd Becker, Compositional Performability Evaluation for STATEMATE, Proceedings of the 3rd international conference on the Quantitative Evaluation of Systems, p.167-178, September 11-14, 2006 [doi>10.1109/QEST.2006.10]
• 4: Amar Bouali , Robert de Simone, Symbolic Bisimulation Minimisation, Proceedings of the Fourth International Workshop on Computer Aided Verification, p.96-108, June 29-July 01, 1992
• 5: M C Browne , E M Clarke , D L Dill , B Mishra, Automatic verification of sequential circuits using temporal logic, IEEE Transactions on Computers, v.35 n.12, p.1035-1044, Dec. 1986 [doi>10.1109/TC.1986.1676711]
• 6: Randal E. Bryant, Graph-based algorithms for Boolean function manipulation, IEEE Transactions on Computers, v.35 n.8, p.677-691, Aug. 1986 [doi>10.1109/TC.1986.1676819]
• 7: J.R. Burch, E.M. Clarke, and D.E. Long. Symbolic model checking with partitioned transition relations. In Proc. of VLSI'91, pages 49--58, 1991.
• 8: Gianfranco Ciardo , Marco Tilgner, ON THE USE OF KRONECKER OPERATORS FOR THE SOLUTION OF GENERALIZED STOCHASTIC PETRI NETS, Institute for Computer Applications in Science and Engineering (ICASE), 1996
• 9: ERTMS. Project Website, May 16, 2006. http://ertms.uic.asso.fr/etcs.html.
• 10: Jean-Claude Fernandez , Alain Kerbrat , Laurent Mounier, Symbolic Equivalence Checking, Proceedings of the 5th International Conference on Computer Aided Verification, p.85-96, June 28-July 01, 1993
• 11: Kathi Fisler , Moshe Y. Vardi, Bisimulation and Model Checking, Proceedings of the 10th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, p.338-341, September 27-29, 1999
• 12: Jan Friso Groote , Frits W. Vaandrager, An Efficient Algorithm for Branching Bisimulation and Stuttering Equivalence, Proceedings of the 17th International Colloquium on Automata, Languages and Programming, p.626-638, July 16-20, 1990
• 13: David Harel , Michal Politi, Modeling Reactive Systems with Statecharts: The Statemate Approach, McGraw-Hill, Inc., New York, NY, 1998
• 14: M. Herbstritt, R. Wimmer, T. Peikenkamp, E. Böde, M. Adelaide, S. Johr, H. Hermanns, and B. Becker. Analysis of Large Safety-Critical Systems: A quantitative Approach. Reports of SFB/TR 14 AVACS 8, Feb 2006.
• 15: H. Hermanns. Interactive Markov Chains: The Quest for Quantified Quality, volume 2428 of LNCS. Springer, 2002.
• 16: Joost-Pieter Katoen , Marta Z. Kwiatkowska , Gethin Norman , David Parker, Faster and Symbolic CTMC Model Checking, Proceedings of the Joint International Workshop on Process Algebra and Probabilistic Methods, Performance Modeling and Verification, p.23-38, September 12-14, 2001
• 17: M. Kuntz, M. Siegle, and E. Werner. Symbolic Performance and Dependability Evaluation with the Tool CASPA. In FORTE Workshops, volume 3236 of LNCS, pages 293--307. Springer, 2004.
• 18: Yusuke Matsunaga , Patrick C. McGeer , Robert K. Brayton, On computing the transitive closure of a state transition relation, Proceedings of the 30th international conference on Design automation, p.260-265, June 14-18, 1993, Dallas, Texas, United States [doi>10.1145/157485.164884]
• 19: R. Milner, Communication and concurrency, Prentice-Hall, Inc., Upper Saddle River, NJ, 1989
• 20: Rocco De Nicola , Frits Vaandrager, Three logics for branching bisimulation, Journal of the ACM (JACM), v.42 n.2, p.458-487, March 1995 [doi>10.1145/201019.201032]
• 21: F. Somenzi. CUDD: CU Decision Diagram Package Release 2.4.1. University of Colorado at Boulder, 2005.
• 22: Rob J. van Glabbeek, The Linear Time - Branching Time Spectrum II, Proceedings of the 4th International Conference on Concurrency Theory, p.66-81, August 23-26, 1993
• 23: Rob J. van Glabbeek , W. Peter Weijland, Branching time and abstraction in bisimulation semantics, Journal of the ACM (JACM), v.43 n.3, p.555-600, May 1996 [doi>10.1145/233551.233556]
• 24: R. Wimmer, M. Herbstritt, and B. Becker. Minimization of Large State Spaces using Symbolic Branching Bisimulation. In Proc. of DDECS'06. IEEE, 2006.
• 25: R. Wimmer, M. Herbstritt, H. Hermanns, K. Strampp, and B. Becker. Sigref -- A Symbolic Bisimulation Tool Box. In Proc. of 4th ATVA, volume 4218 of LNCS, pages 477--492. Springer, 2006.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.1 Models of Computation
          Subjects: Automata (e.g., finite, push-down, resource-bounded)

General Terms:
Algorithms, Verification

Keywords:
binary decision diagrams, bisimulation, state space explosion, state space reduction, symbolic methods