A Parallel Relation-Based Algorithm for Symbolic Bisimulation Minimization

  • Richard Huybers
  • Alfons LaarmanEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11388)


Symbolic computation using BDDs and bisimulation minimization are alternative ways to cope with the state space explosion in model checking. The combination of both techniques opens up many parameters that can be tweaked for further optimization. Most importantly, the bisimulation can either be represented as equivalence classes or as a relation. While recent work argues that storing partitions is more efficient, we show that the relation-based approach is preferable. We do so by deriving a relation-based minimization algorithm based on new coarse-grained BDD operations. The implementation demonstrates that the relational approach uses fewer memory and performs better.


Bisimulation minimization Symbolic model checking BDDs Decision diagrams Parallel computing 


  1. 1.
    Baier, C., Katoen, J.: Principles of Model Checking. MIT Press, Cambridge (2008)zbMATHGoogle Scholar
  2. 2.
    Blom, S., Orzan, S.: Distributed branching bisimulation reduction of state spaces. Electron. Notes Theor. Comput. Sci. 89(1), 99–113 (2003)CrossRefGoogle Scholar
  3. 3.
    Bouali, A., de Simone, R.: Symbolic bisimulation minimisation. In: von Bochmann, G., Probst, D.K. (eds.) CAV 1992. LNCS, vol. 663, pp. 96–108. Springer, Heidelberg (1993). Scholar
  4. 4.
    Brace, K.S., Rudell, R.L., Bryant, R.E.: Efficient implementation of a BDD package. In: 27th ACM/IEEE Design Automation Conference, pp. 40–45 (1990)Google Scholar
  5. 5.
    Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput. C–35(8), 677–691 (1986)CrossRefGoogle Scholar
  6. 6.
    Burch, J., Clarke, E., McMillan, K., Dill, D., Hwang, L.: Symbolic model checking: 1020 states and beyond. Inf. Comput. 98(2), 142–170 (1992)CrossRefGoogle Scholar
  7. 7.
    Ciardo, G., Lüttgen, G., Siminiceanu, R.: Saturation: an efficient iteration strategy for symbolic state—Space generation. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 328–342. Springer, Heidelberg (2001). Scholar
  8. 8.
    Dalsgaard, A.E., Enevoldsen, S., Larsen, K.G., Srba, J.: Distributed computation of fixed points on dependency graphs. In: Fränzle, M., Kapur, D., Zhan, N. (eds.) SETTA 2016. LNCS, vol. 9984, pp. 197–212. Springer, Cham (2016). Scholar
  9. 9.
    De Nicola, R., Vaandrager, F.: Three logics for branching bisimulation. J. ACM (JACM) 42(2), 458–487 (1995)MathSciNetCrossRefGoogle Scholar
  10. 10.
    van Dijk, T.: Sylvan: multi-core decision diagrams. Ph.D. thesis, University of Twente (2016).
  11. 11.
    van Dijk, T., van de Pol, J.: Multi-core symbolic bisimulation minimisation. Int. J. Softw. Tools Technol. Transf. 20(2), 157–177 (2018)CrossRefGoogle Scholar
  12. 12.
    van Dijk, T., van de Pol, J.C.: Lace: non-blocking split deque for work-stealing. In: Lopes, L., et al. (eds.) Euro-Par 2014. LNCS, vol. 8806, pp. 206–217. Springer, Cham (2014). Scholar
  13. 13.
    Fisler, K., Vardi, M.Y.: Bisimulation and model checking. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 338–342. Springer, Heidelberg (1999). Scholar
  14. 14.
    Fisler, K., Vardi, M.Y.: Bisimulation minimization in an automata-theoretic verification framework. In: Gopalakrishnan, G., Windley, P. (eds.) FMCAD 1998. LNCS, vol. 1522, pp. 115–132. Springer, Heidelberg (1998). Scholar
  15. 15.
    Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. J. ACM (JACM) 32(1), 137–161 (1985)MathSciNetCrossRefGoogle Scholar
  16. 16.
    Huth, M., Ryan, M.: Verification by model checking, chap. Logic in Computer Science, p. 241. Cambridge University Press, Cambridge (2004)CrossRefGoogle Scholar
  17. 17.
    Liu, X., Smolka, S.A.: Simple linear-time algorithms for minimal fixed points. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 53–66. Springer, Heidelberg (1998). Scholar
  18. 18.
    Milner, R.: Communication and Concurrency. Prentice Hall, Upper Saddle River (1989)zbMATHGoogle Scholar
  19. 19.
    Mumme, M., Ciardo, G.: An efficient fully symbolic bisimulation algorithm for non-deterministic systems. IJFCS 24(02), 263–282 (2013)MathSciNetzbMATHGoogle Scholar
  20. 20.
    Paige, R., Tarjan, R.E.: Three partition refinement algorithms. SIAM J. Comput. 16(6), 973–989 (1987). Scholar
  21. 21.
    Park, D.: Concurrency and automata on infinite sequences. In: Deussen, P. (ed.) GI-TCS 1981. LNCS, vol. 104, pp. 167–183. Springer, Heidelberg (1981). Scholar
  22. 22.
    Shannon, C.E.: A symbolic analysis of relay and switching circuits. Electr. Eng. 57(12), 713–723 (1938). Scholar
  23. 23.
    Solé, M., Pastor, E.: Traversal techniques for concurrent systems. In: Aagaard, M.D., O’Leary, J.W. (eds.) FMCAD 2002. LNCS, vol. 2517, pp. 220–237. Springer, Heidelberg (2002). Scholar
  24. 24.
    Van Dijk, T., Laarman, A., Van De Pol, J.: Multi-core BDD operations for symbolic reachability. Electron. Notes Theor. Comput. Sci. 296, 127–143 (2013)CrossRefGoogle Scholar
  25. 25.
    Wimmer, R., Herbstritt, M., Hermanns, H., Strampp, K., Becker, B.: Sigref – a symbolic bisimulation tool box. In: Graf, S., Zhang, W. (eds.) ATVA 2006. LNCS, vol. 4218, pp. 477–492. Springer, Heidelberg (2006). Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.LIACSLeiden UniversityLeidenThe Netherlands

Personalised recommendations