Skip to main content
SpringerLink
Log in

State Space Reduction Using Partial τ-Confluence

  • Conference paper
  • First Online:
Mathematical Foundations of Computer Science 2000 (MFCS 2000)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1893))

Abstract

We present an efficient algorithm to determine the maximal class of confluent τ-transitions in a labelled transition system. Confluent τ-transitions are inert with respect to branching bisimulation. This allows to use τ-priorisation, which means that in a state with a confluent outgoing τ-transition all other transitions can be removed, maintaining branching bisimulation. In combination with the removal of τ-loops, and the compression of τ-sequences this yields an efficient algorithm to reduce the size of large state spaces.

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 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.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. A.V. Aho, J.E. Hopcroft and J.D. Ullman. Data structures and algorithms. Addison-Wesley. 1983.

    Google Scholar 

  2. M.A. Bezem and J.F. Groote. A correctness proof of a one bit sliding window protocol in μCRL. The Computer Journal, 37(4): 289–307, 1994.

    Article  Google Scholar 

  3. M. Cherif and H. Garavel and H. Hermanns. The bcg_min user manual, version 1.1. http://www.inrialpes.fr/vasy/cadp/man/bcg_min.html, 1999.

  4. D. Dill, C.N. Ip and U. Stern. Murphi description language and verifier. http://sprout.stanford.edu/dill/murphi.html, 1992-2000.

  5. H. Garavel and R. Mateescu. The Caesar/Aldebaran development package. http://www.inrialpes.fr/vasy/cadp/, 1996-2000.

  6. R.J. van Glabbeek and W.P. Weijland. Branching time and abstraction in bisimulation semantics. In Journal of the ACM, 43(3):555–600, 1996.

    Article  MathSciNet  Google Scholar 

  7. P. Godefroid and P. Wolper. A partial approach to model checking. Information and Computation, 110(2):305–326, 1994.

    Article  MATH  MathSciNet  Google Scholar 

  8. J.F. Groote and B. Lisser. The CRL toolset. http://www.cwi.nl/~mcrl, 1999–2000.

  9. J.F. Groote and J.C. van de Pol. State space reduction using partial τ-confluence. Technical Report CWI-SEN-R0008, March 2000. Available via http://www.cwi.nl/_vdpol/papers/.

  10. J.F. Groote and M.P.A. Sellink. Confluence for process verification. In Theoretical Computer Science B, 170(1-2):47–81, 1996.

    MATH  MathSciNet  Google Scholar 

  11. J.F. Groote and F.W. Vaandrager. An efficient algorithm for branching bisimulation and stuttering equivalence. In Proc. 17th ICALP, LNCS 443, 626–638. Springer-Verlag, 1990.

    Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

  13. N. Kobayashi, B.C. Pierce, and D.N. Turner. Linearity and the τ-calculus. In: Proceedings of the 23rd POPL, pages 358–371. ACM press, January1996.

    Google Scholar 

  14. X. Liu and D. Walker. Confluence of processes and systems of objects. In Proceedings of TAPSOFT’95, pages 217–231, LNCS 915, 1995.

    Google Scholar 

  15. S.P. Luttik. Description and formal specification of the link layer of P1394. Technical Report SEN-R9706, CWI, Amsterdam, 1997.

    Google Scholar 

  16. R. Milner. Communication and Concurrency. Prentice Hall International. 1989.

    Google Scholar 

  17. U. Nestmann and M. Steffen. Typing confluence. In: Proceedings of FMICS’97, pages 77–101. CNR Pisa, 1997.

    Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

  19. A. Philippou and D. Walker. On confluence in the pi-calculus. 24th Int. Coll. on Automata, Languages and Programming, LNCS1256, Springer-Verlag, 1997.

    Google Scholar 

  20. M. Sighireanu and R. Mateescu. Verification of the link layer protocol of the IEEE-1394 serial bus (firewire): an experiment with E-LOTOS. In Journal on Software Tools for Technology Transfer (STTT), 2(1):68–88, 1998.

    Article  MATH  Google Scholar 

  21. A. Valmari. A stubborn attack on state explosion. In Proc. of Computer Aided Verification, LNCS 531, pages 25–42, Springer-Verlag, 1990.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. CWI, P.O.-box 94.079, 1090, GB Amsterdam, The Netherlands

    Jan Friso Groote & Jaco van de Pol

  2. Department of Mathematics and Computing Science, Eindhoven University of Technology, P.O. Box 513, 5600, MB Eindhoven, The Netherlands

    Jan Friso Groote

Authors
  1. Jan Friso Groote
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jaco van de Pol
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, University of Aarhus, Ny Munkegade, Bldg. 540, 8000, Aarhus C, Denmark

    Mogens Nielsen

  2. Department of Computer Sciene, Comenius University, 84248, Bratislava, Slovakia

    Branislav Rovan

Rights and permissions

Reprints and permissions

Copyright information

© 2000 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Groote, J.F., van de Pol, J. (2000). State Space Reduction Using Partial τ-Confluence. In: Nielsen, M., Rovan, B. (eds) Mathematical Foundations of Computer Science 2000. MFCS 2000. Lecture Notes in Computer Science, vol 1893. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44612-5_34

Download citation

  • DOI: https://doi.org/10.1007/3-540-44612-5_34

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-67901-1

  • Online ISBN: 978-3-540-44612-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation