Skip to main content
SpringerLink
Log in

Sigref – A Symbolic Bisimulation Tool Box

  • Conference paper
Automated Technology for Verification and Analysis (ATVA 2006)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 4218))

Abstract

We present a uniform signature-based approach to compute the most popular bisimulations. Our approach is implemented symbolically using BDDs, which enables the handling of very large transition systems. Signatures for the bisimulations are built up from a few generic building blocks, which naturally correspond to efficient BDD operations. Thus, the definition of an appropriate signature is the key for a rapid development of algorithms for other types of bisimulation.

We provide experimental evidence of the viability of this approach by presenting computational results for many bisimulations on real-world instances. The experiments show cases where our framework can handle state spaces efficiently that are far too large to handle for any tool that requires an explicit state space description.

This work was partly supported by the German Research Council (DFG) as part of the Transregional Collaborative Research Center “Automatic Verification and Analysis of Complex Systems” (SFB/TR 14 AVACS). See www.avacs.org for more information.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Wimmer, R., Herbstritt, M., Becker, B.: Minimization of Large State Spaces using Symbolic Branching Bisimulation. In: Proc. of IEEE Workshop on Design & Diagnostics of Electronic Circuits & Systems (DDECS), pp. 9–14 (2006)

    Google Scholar 

  2. Chehaibar, G., et al.: Specification and Verification of the PowerScaleTM Bus Arbitration Protocol: An Industrial Experiment with LOTOS. In: Proc. of FORTE, vol. 69, pp. 435–450 (1996)

    Google Scholar 

  3. Giannakopoulou, D.: Model Checking for Concurrent Software Architectures. PhD thesis, Imperial College, University of London (1999)

    Google Scholar 

  4. Graf, S., Steffen, B., Luttgen, G.: Compositional minimisation of finite state systems using interface specifications. Formal Asp. of Comp. 8(5), 607–616 (1996)

    Article  MATH  Google Scholar 

  5. Kanellakis, P., Smolka, S.: CCS expressions, finite state processes, and three problems of equivalence. Information and Computation 86(1), 43–68 (1990)

    Article  MATH  MathSciNet  Google Scholar 

  6. Paige, R., Tarjan, R.E.: Three partition refinement algorithms. SIAM Jour. on Computing 16(6), 973–989 (1987)

    Article  MATH  MathSciNet  Google Scholar 

  7. Burch, J., et al.: Symbolic Model Checking: 1020 States and Beyond. Information and Computation 98(2), 142–170 (1992)

    Article  MATH  MathSciNet  Google Scholar 

  8. Bouajjani, A., Fernandez, J.C., Halbwachs, N.: Minimal model generation. In: Clarke, E., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol. 531, pp. 197–203. Springer, Heidelberg (1991)

    Chapter  Google Scholar 

  9. Bouajjani, A., Fernandez, J.C., Halbwachs, N., Ratel, C., Raymond, P.: Minimal state graph generation. Science of Computer Programming 18, 247–269 (1992)

    Article  MATH  MathSciNet  Google Scholar 

  10. Bouali, A., de Simone, R.: Symbolic Bisimulation Minimisation. In: Probst, D.K., von Bochmann, G. (eds.) CAV 1992. LNCS, vol. 663, pp. 96–108. Springer, Heidelberg (1993)

    Google Scholar 

  11. Blom, S., Orzan, S.: Distributed Branching Bisimulation Reduction of State Spaces. ENTCS 89(1), 113–990 (2003)

    Google Scholar 

  12. Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)

    MATH  Google Scholar 

  13. Milner, R.: A Calculus of Communication Systems. LNCS, vol. 92. Springer, Heidelberg (1980)

    Google Scholar 

  14. Milner, R.: Lectures on a Calculus for Communicating Systems. In: Brookes, S.D., Winskel, G., Roscoe, A.W. (eds.) Seminar on Concurrency. LNCS, vol. 197, pp. 197–220. Springer, Heidelberg (1985)

    Google Scholar 

  15. van Glabbeek, R., Weijland, W.: Branching Time and Abstraction in Bisimulation Semantics. Journal of the ACM 43(3), 555–600 (1996)

    Article  MathSciNet  MATH  Google Scholar 

  16. Baeten, J., van Glabbeek, R.: Another Look at Abstraction in Process Algebra. In: Ottmann, T. (ed.) ICALP 1987. LNCS, vol. 267, pp. 84–94. Springer, Heidelberg (1987)

    Google Scholar 

  17. Bergstra, J.A., Ponse, A., van der Zwaag, M.B.: Branching time and orthogonal bisimulation equivalence. Theor. Comp. Sci. 309, 313–355 (2003)

    Article  MATH  Google Scholar 

  18. Milner, R.: A Modal Characterization of Observable Machine-Behaviour. In: Astesiano, E., Böhm, C. (eds.) CAAP 1981. LNCS, vol. 112, pp. 25–34. Springer, Heidelberg (1981)

    Google Scholar 

  19. Montanari, U., Sassone, V.: Dynamic congruence vs. progressing bisimulation for CCS. Fundam. Inform. 16(1), 171–199 (1992)

    MATH  MathSciNet  Google Scholar 

  20. Bouajjani, A., et al.: Safety for Branching Time Semantics. In: Leach Albert, J., Monien, B., Rodríguez-Artalejo, M. (eds.) ICALP 1991. LNCS, vol. 510, pp. 76–92. Springer, Heidelberg (1991)

    Google Scholar 

  21. van Glabbeek, R.J.: The linear time – branching time spectrum II. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 66–81. Springer, Heidelberg (1993)

    Google Scholar 

  22. Hermanns, H., Lohrey, M.: Priority and maximal progress are completely axiomatisable. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 237–252. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  23. Park, D.: Concurrency and automata on infinite sequences. In: Deussen, P. (ed.) GI-TCS 1981. LNCS, vol. 104, pp. 167–183. Springer, Heidelberg (1981)

    Chapter  Google Scholar 

  24. Dovier, A., Gentilini, R., Piazza, C., Policriti, A.: Rank-based symbolic bisimulation (and model checking). ENTCS 67 (2002)

    Google Scholar 

  25. Klarlund, N.: An nlogn algorithm for online BDD refinement. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 107–118. Springer, Heidelberg (1997)

    Google Scholar 

  26. Somenzi, F.: CUDD: CU Decision Diagram Package Release 2.4.1. University of Colorado at Boulder (2005)

    Google Scholar 

  27. Groote, J.F., Vaandrager, F.W.: An Efficient Algorithm for Branching Bisimulation and Stuttering Equivalence. In: Paterson, M. (ed.) ICALP 1990. LNCS, vol. 443, pp. 626–638. Springer, Heidelberg (1990)

    Chapter  Google Scholar 

  28. Bryant, R.: Graph-Based Algorithms for Boolean Function Manipulation. IEEE Trans. on Comp. 35(8), 677–691 (1986)

    Article  MATH  Google Scholar 

  29. Wegener, I.: Branching programs and binary decision diagrams. SIAM Monographs on Discrete Mathematics and Applications. SIAM, Philadelphia (2000)

    Book  MATH  Google Scholar 

  30. Strampp, K.: Symbolische Berechnung von Bisimulationen. Diploma thesis, Albert-Ludwigs-University Freiburg, Germany (2006)

    Google Scholar 

  31. Matsunaga, Y., McGeer, P.C., Brayton, R.K.: On computing the transitive closure of a state transition relation. In: Proc. of DAC, pp. 260–265. ACM Press, New York (1993)

    Google Scholar 

  32. Burch, J.R., et al.: Sequential circuit verification using symbolic model checking. In: Proc. of DAC, pp. 46–51. ACM Press, New York (1990)

    Google Scholar 

  33. Garavel, H., Hermanns, H.: On Combining Functional Verification and Performance Evaluation using CADP. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol. 2391, Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  34. Fernandez, J.C., et al.: CADP: A Protocol Validation and Verification Toolbox. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 437–440. Springer, Heidelberg (1996)

    Google Scholar 

  35. Herbstritt, M., Wimmer, R., Peikenkamp, T., Böde, E., Adelaide, M., Johr, S., Hermanns, H., Becker, B.: Analysis of Large Safety-Critical Systems: A quantitative Approach. Reports of SFB/TR 14 AVACS 8 (2006) ISSN 1860-9821

    Google Scholar 

  36. Ciardo, G., Tilgner, M.: On the use of Kronecker operators for the solution of generalized stochastic Petri nets. Technical Report 96-35, ICASE (1996)

    Google Scholar 

  37. Kuntz, M., Siegle, M., Werner, E.: Symbolic Performance and Dependability Evaluation with the Tool CASPA. In: Núñez, M., Maamar, Z., Pelayo, F.L., Pousttchi, K., Rubio, F. (eds.) FORTE 2004. LNCS, vol. 3236, pp. 293–307. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  38. Harel, D., Politi, M.: Modelling Reactive Systems with Statecharts: The Statemate Approach. McGraw-Hill, New York (1998)

    Google Scholar 

  39. ERTMS: Project (May 16, 2006), Website http://ertms.uic.asso.fr/etcs.html

  40. 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)

    Google Scholar 

  41. Hermanns, H.: Interactive Markov Chains: The Quest for Quantified Quality. In: Hermanns, H. (ed.) Interactive Markov Chains. LNCS, vol. 2428, Springer, Heidelberg (2002)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Albert-Ludwigs-University Freiburg, Germany

    Ralf Wimmer, Marc Herbstritt, Kelley Strampp & Bernd Becker

  2. Saarland University, Saarbrücken, Germany

    Holger Hermanns

Authors
  1. Ralf Wimmer
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Marc Herbstritt
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Holger Hermanns
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Kelley Strampp
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Bernd Becker
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. VERIMAG, 2 Avenue de Vignate, Centre Equitation, 38610, Grenoble-Gières, France

    Susanne Graf

  2. Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China

    Wenhui Zhang

Rights and permissions

Reprints and permissions

Copyright information

© 2006 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Wimmer, R., Herbstritt, M., Hermanns, H., Strampp, K., Becker, B. (2006). Sigref – A Symbolic Bisimulation Tool Box. In: Graf, S., Zhang, W. (eds) Automated Technology for Verification and Analysis. ATVA 2006. Lecture Notes in Computer Science, vol 4218. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11901914_35

Download citation

  • DOI: https://doi.org/10.1007/11901914_35

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-47237-7

  • Online ISBN: 978-3-540-47238-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation