Advertisement

State Space Reduction Using Partial τ-Confluence

  • Jan Friso Groote
  • Jaco van de Pol
Conference paper
Part of the Lecture Notes in Computer Science book series (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.

Keywords

State Space Transition System Label Transition System Candidate Transition Maximal Class 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    A.V. Aho, J.E. Hopcroft and J.D. Ullman. Data structures and algorithms. Addison-Wesley. 1983.Google Scholar
  2. 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.CrossRefGoogle Scholar
  3. 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. 4.
    D. Dill, C.N. Ip and U. Stern. Murphi description language and verifier. http://sprout.stanford.edu/dill/murphi.html, 1992-2000.
  5. 5.
    H. Garavel and R. Mateescu. The Caesar/Aldebaran development package. http://www.inrialpes.fr/vasy/cadp/, 1996-2000.
  6. 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.CrossRefMathSciNetGoogle Scholar
  7. 7.
    P. Godefroid and P. Wolper. A partial approach to model checking. Information and Computation, 110(2):305–326, 1994.zbMATHCrossRefMathSciNetGoogle Scholar
  8. 8.
    J.F. Groote and B. Lisser. The CRL toolset. http://www.cwi.nl/~mcrl, 1999–2000.
  9. 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. 10.
    J.F. Groote and M.P.A. Sellink. Confluence for process verification. In Theoretical Computer Science B, 170(1-2):47–81, 1996.zbMATHMathSciNetGoogle Scholar
  11. 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. 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.zbMATHCrossRefMathSciNetGoogle Scholar
  13. 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. 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. 15.
    S.P. Luttik. Description and formal specification of the link layer of P1394. Technical Report SEN-R9706, CWI, Amsterdam, 1997.Google Scholar
  16. 16.
    R. Milner. Communication and Concurrency. Prentice Hall International. 1989.Google Scholar
  17. 17.
    U. Nestmann and M. Steffen. Typing confluence. In: Proceedings of FMICS’97, pages 77–101. CNR Pisa, 1997.Google Scholar
  18. 18.
    R. Paige and R. Tarjan. Three partition refinement algorithms. SIAM Journal on Computing, 16(6):973–989, 1987.zbMATHCrossRefMathSciNetGoogle Scholar
  19. 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. 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.zbMATHCrossRefGoogle Scholar
  21. 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

Copyright information

© Springer-Verlag Berlin Heidelberg 2000

Authors and Affiliations

  • Jan Friso Groote
    • 1
    • 2
  • Jaco van de Pol
    • 1
  1. 1.CWIGB AmsterdamThe Netherlands
  2. 2.Department of Mathematics and Computing ScienceEindhoven University of TechnologyMB EindhovenThe Netherlands

Personalised recommendations