Skip to main content
SpringerLink
Log in
Book cover

International Conference on Concurrency Theory

CONCUR 2007: CONCUR 2007 – Concurrency Theory pp 120–135Cite as

Equivalence Checking for Infinite Systems Using Parameterized Boolean Equation Systems

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 4703))

Abstract

In this paper, we provide a transformation from the branching bisimulation problem for infinite, concurrent, data-intensive systems in linear process format, into solving Parameterized Boolean Equation Systems. We prove correctness, and illustrate the approach with an unbounded queue example. We also provide some adaptations to obtain similar transformations for weak bisimulation and simulation equivalence.

This is a preview of subscription content, 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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  2. Andersen, H.R.: Model checking and boolean graphs. Theoretical Computer Science 126(1), 3–30 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  3. Andersen, H.R., Vergauwen, B.: Efficient checking of behavioural relations and modal assertions using fixed-point inversion. In: Wolper, P. (ed.) CAV 1995. LNCS, vol. 939, pp. 142–154. Springer, Heidelberg (1995)

    Google Scholar 

  4. Basten, T.: Branching bisimilarity is an equivalence indeed! Information Processing Letters 58, 141–147 (1996)

    Article  MATH  MathSciNet  Google Scholar 

  5. Bolognesi, T., Brinksma, E.: Introduction to the ISO specification language LOTOS. Computer Networks 14, 25–59 (1987)

    Google Scholar 

  6. Chandy, K.M., Misra, J.: Parallel Program Design: A Foundation. Addison-Wesley, Reading (1988)

    MATH  Google Scholar 

  7. Chen, T., Ploeger, B., van de Pol, J., Willemse, T.A.C.: Equivalence checking for infinite systems using parameterized boolean equation systems. CS-Report 07-14, Technische Universiteit Eindhoven (2007)

    Google Scholar 

  8. Cleaveland, R., Steffen, B.: Computing behavioural relations, logically. In: Leach Albert, J., Monien, B., Rodríguez-Artalejo, M. (eds.) Automata, Languages and Programming. LNCS, vol. 510, pp. 127–138. Springer, Heidelberg (1991)

    Google Scholar 

  9. Fokkink, W., Pang, J., van de Pol, J.: Cones and foci: A mechanical framework for protocol verification. Formal Methods in System Design 29(1), 1–31 (2006)

    Article  MATH  Google Scholar 

  10. van Glabbeek, R.: The Linear Time - Branching Time Spectrum II. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 66–81. Springer, Heidelberg (1993)

    Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  12. Groote, J.F., Mateescu, R.: Verification of temporal properties of processes in a setting with data. In: Haeberer, A.M. (ed.) AMAST 1998. LNCS, vol. 1548, pp. 74–90. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  13. Groote, J.F., van de Pol, J.: A bounded retransmission protocol for large data packets. In: Nivat, M., Wirsing, M. (eds.) AMAST 1996. LNCS, vol. 1101, pp. 536–550. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

  14. Groote, J.F., Reniers, M.: Algebraic process verification. In: Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.) Handbook of Process Algebra, pp. 1151–1208. Elsevier, Amsterdam (2001)

    Chapter  Google Scholar 

  15. Groote, J.F., Vaandrager, F.W.: An efficient algorithm for branching bisimulation and stuttering equivalence. In: Paterson, M.S. (ed.) Automata, Languages and Programming. LNCS, vol. 443, pp. 626–638. Springer, Heidelberg (1990)

    Chapter  Google Scholar 

  16. Groote, J.F., Willemse, T.A.C.: Model-checking processes with data. Science of Computer Programming 56(3), 251–273 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  17. Groote, J.F., Willemse, T.A.C.: Parameterised boolean equation systems. Theoretical Computer Science 343(3), 332–369 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  18. Kwak, H., Choi, J., Lee, I., Philippou, A.: Symbolic weak bisimulation for value-passing calculi. Technical Report, MS-CIS-98-22, Department of Computer and Information Science, University of Pennsylvania (1998)

    Google Scholar 

  19. Lin, H.: Symbolic transition graph with assignment. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol. 1119, pp. 50–65. Springer, Heidelberg (1996)

    Google Scholar 

  20. Lynch, N., Tuttle, M.: An introduction to input/output automata. CWI Quarterly 2(3), 219–246 (1989)

    MATH  MathSciNet  Google Scholar 

  21. Mader, A.: Verification of modal properties using boolean equation systems. PhD Thesis, VERSAL 8, Bertz Verlag, Berlin (1997)

    Google Scholar 

  22. Mateescu, R.: A generic on-the-fly solver for alternation-free boolean equation systems. In: Garavel, H., Hatcliff, J. (eds.) ETAPS 2003 and TACAS 2003. LNCS, vol. 2619, pp. 81–96. Springer, Heidelberg (2003)

    Google Scholar 

  23. Milner, R.: A Calculus of Communicating Systems. Springer, Heidelberg (1980)

    MATH  Google Scholar 

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

    MATH  Google Scholar 

  25. Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes (Part I/II). Information and Computation 100(1), 1–77 (1992)

    Article  MATH  MathSciNet  Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

  27. Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics 5(2), 285–309 (1955)

    MATH  MathSciNet  Google Scholar 

  28. Zhang, D., Cleaveland, R.: Fast generic model-checking for data-based systems. In: Wang, F. (ed.) FORTE 2005. LNCS, vol. 3731, pp. 83–97. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. CWI, Department of Software Engineering, P.O. Box 94079, 1090 GB Amsterdam, The Netherlands

    Taolue Chen & Jaco van de Pol

  2. Eindhoven University of Technology, Design and Analysis of Systems Group, P.O. Box 513, 5600 MB Eindhoven, The Netherlands

    Bas Ploeger, Jaco van de Pol & Tim A. C. Willemse

Authors
  1. Taolue Chen
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Bas Ploeger
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Jaco van de Pol
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Tim A. C. Willemse
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Luís Caires Vasco T. Vasconcelos

Rights and permissions

Reprints and permissions

Copyright information

© 2007 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Chen, T., Ploeger, B., van de Pol, J., Willemse, T.A.C. (2007). Equivalence Checking for Infinite Systems Using Parameterized Boolean Equation Systems. In: Caires, L., Vasconcelos, V.T. (eds) CONCUR 2007 – Concurrency Theory. CONCUR 2007. Lecture Notes in Computer Science, vol 4703. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-74407-8_9

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-74407-8_9

  • Publisher Name: Springer, Berlin, Heidelberg

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

  • Online ISBN: 978-3-540-74407-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation