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. E. Böde, M. Herbstritt, H. Hermanns, S. Johr, T. Peikenkamp, R. Pulungan, R. Wimmer, and B. Becker. Compositional perfomability evaluation for statemate. In 3rd International Conference on Quantitative Evaluation of Systems (QEST). IEEE, 2006.]]
4. A. Bouali and R. de Simone. Symbolic bisimulation minimisation. In Proc. of 4th CAV, volume 663 of LNCS, pages 96--108. Springer, 1992.]]
5. M. Browne, E. Clarke, D. Dill, and B. Mishra. Automatic verification of sequential circuits using temporal logic. Trans. on Comp., C-35:1035--1044, 1986.]]
6. R. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Trans. on Comp., 35(8):677--691, 1986.]]
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. G. Ciardo and M. Tilgner. On the use of Kronecker operators for the solution of generalized stochastic Petri nets. Technical Report 96--35, ICASE, 1996.]]
9. ERTMS. Project Website, May 16, 2006. http://ertms.uic.asso.fr/etcs.html.]]
10. J.-C. Fernandez, A. Kerbrat, and L. Mounier. Symbolic equivalence checking. In Proc. of 5th CAV, volume 697 of LNCS, pages 85--96. Springer, 1993.]]
11. K. Fisler and M.Y. Vardi. Bisimulation and model checking. In Procof CHARME, LNCS, pages 338--341, 1999.]]
12. J.F. Groote and F.W. Vaandrager. An efficient algorithm for branching bisimulation and stuttering equivalence. In Proc. of 17th ICALP, volume 443 of LNCS, pages 626--638. Springer, 1990.]]
13. D. Harel and M. Politi. Modelling Reactive Systems with Statecharts: The STATEMATE Approach. McGraw-Hill, 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. J.-P. Katoen et al. Faster and Symbolic CTMC Model Checking. In Procof PAPM-PROBMIV, volume 2165 of LNCS, pages 23--38. Springer, 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. Y. Matsunaga, P.C. McGeer, and R.K. Brayton. On computing the transitive closure of a state transition relation. In Proc. of 30th DAC, pages 260--265. ACM Press, 1993.]]
19. R. Milner. Communication and concurrency. International Series in Computer Science. Prentice Hall, 1989.]]
20. R.D. Nicola and F. Vaandrager. Three logics for branching bisimulation. Journal of the ACM, 42(2):458--487, 1995.]]
21. F. Somenzi. CUDD: CU Decision Diagram Package Release 2.4.1. University of Colorado at Boulder, 2005.]]
22. R.J. van Glabbeek. The linear time -- branching time spectrum II. In Proc. of CONCUR'93, volume 715 of LNCS, pages 66--81. Springer, 1993.]]
23. R.J. van Glabbeek and W.P. Weijland. Branching time and abstraction in bisimulation semantics. Journal of the ACM, 43(3):555--600, 1996.]]
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

• Theory of computation

  • Formal languages and automata theory