Skip to main content
SpringerLink
Log in

Bisimulation and Other Undecidable Equivalences for Lossy Channel Systems

  • Conference paper
  • First Online:
Theoretical Aspects of Computer Software (TACS 2001)

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

Included in the following conference series:

Abstract

Lossy channel systems are systems of finite state automata that communicate via unreliable unbounded fifo channels. Today the main open question in the theory of lossy channel systems is whether bisimulation is decidable.

We show that bisimulation, simulation, and in fact all relations between bisimulation and trace inclusion are undecidable for lossy channel systems (and for lossy vector addition systems).

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. P.A. Abdulla, A. Annichini, and A. Bouajjani. Symbolic verification of lossy channel systems: Application to the bounded retransmission protocol. In Proc. 5th Int. Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS’99),A msterdam,The Netherlands,March 1999, volume 1579 of Lecture Notes in Computer Science, pages 208–222. Springer, 1999.

    Google Scholar 

  2. P.A. Abdulla, A. Bouajjani, and B. Jonsson. On-the-fly analysis of systems with unbounded, lossy FIFO channels. In Proc. 10th Int. Conf. Computer Aided Verification (CAV’98),V ancouver,BC,Canada,June-July 1998, volume 1427 of Lecture Notes in Computer Science, pages 305–318. Springer, 1998.

    Google Scholar 

  3. P.A. Abdulla, C. Baier, S. Purushothaman Iyer, and B. Jonsson. Reasoning about probabilistic lossy channel systems. In Proc. 11th Int. Conf. Concurrency Theory (CONCUR’2000),University Park,PA,USA, Aug. 2000, volume 1877 of Lecture Notes in Computer Science, pages 320–333. Springer, 2000.

    Google Scholar 

  4. P.A. Abdulla and B. Jonsson. Undecidable verification problems for programs with unreliable channels. Information and Computation, 130(1):71–90, 1996.

    Article  MATH  MathSciNet  Google Scholar 

  5. P.A. Abdulla and B. Jonsson. Verifying programs with unreliable channels. Information and Computation, 127(2):91–101, 1996.

    Article  MATH  MathSciNet  Google Scholar 

  6. P.A. Abdulla and M. Kindahl. Decidability of simulation and bisimulation between lossy channel systems and finite state systems. In Proc. 6th Int. Conf. Theory of Concurrency (CONCUR’95),Philadelphia, P A,USA,A ug. 1995, volume 962 of Lecture Notes in Computer Science, pages 333–347. Springer, 1995. Long version available at http://www.docs.uu.se/docs/avds/.

    Google Scholar 

  7. P.A. Abdulla, M. Kindahl, and D. Peled. An improved search strategy for lossy channel systems. In Proc. Joint Int. Conf. Formal Description Techniques and Protocol Specification,Testing,and Verification (FORTE/PSTV’97),Osaka,Jap an,Nov. 1997, pages 251–264. Chapman & Hall, 1997.

    Google Scholar 

  8. O. Bukart, D. Caucal, F. Moller, and B. Steffen. Verification on infinite structures. In J.A. Bergstra, A. Ponse, and S.A. Smolka, editors, Handbook of Process Algebra, chapter 9, pages 545–623. Elsevier Science, 2001.

    Google Scholar 

  9. A. Bouajjani and R. Mayr. Model checking lossy vector addition systems. In Proc. 16th Ann. Symp. Theoretical Aspects of Computer Science (STACS’99),T rier,Germany,Mar. 1999, volume 1563 of Lecture Notes in Computer Science, pages 323–333. Springer, 1999.

    Google Scholar 

  10. G. von Bochmann. Finite state description of communication protocols. Computer Networks and ISDN Systems, 2:361–372, 1978.

    Google Scholar 

  11. D. Brand and P. Zafiropulo. On communicating finite-state machines. Research Report RZ 1053, IBM Zurich Research Lab., June 1981. A short version appears in J.ACM 30(2):323–342, 1983.

    MathSciNet  Google Scholar 

  12. G. Cécé and A. Finkel. Programs with quasi-stable channels are effectively recognizable. In Proc. 9th Int. Conf. Computer Aided Verification (CAV’97),Haifa,Isr ael,June 1997, volume 1254 of Lecture Notes in Computer Science, pages 304–315. Springer, 1997.

    Google Scholar 

  13. G. Cécé, A. Finkel, and S. Purushothaman Iyer. Unreliable channels are easier to verify than perfect channels. Information and Computation, 124(1):20–31, 1995.

    Article  Google Scholar 

  14. A. Finkel. Decidability of the termination problem for completely specificied protocols. Distributed Computing, 7(3):129–135, 1994.

    Article  Google Scholar 

  15. R.J. van Glabbeek. The linear time-branching time spectrum I. In J.A. Bergstra, A. Ponse, and S.A. Smolka, editors, Handbook of Process Algebra, chapter 1, pages 3–99. Elsevier Science, 2001.

    Google Scholar 

  16. R.J. van Glabbeek and F.W. Vaandrager. Modular specification of process algebras. Theoretical Computer Science, 113(2):293–348, 1993.

    Article  MATH  MathSciNet  Google Scholar 

  17. Y. Hirshfeld and M. Jerrum. Bisimulation equivalence is decidable for normed process algebra. In Proc. 26th Int. Coll. Automata,L anguages, and Programming (ICALP’99),Pr ague,Cze ch Republic,July 1999, volume 1644 of Lecture Notes in Computer Science, pages 412–421. Springer, 1999.

    Google Scholar 

  18. P. Jančar. Undecidability of bisimilarity for Petri nets and some related problems. Theoretical Computer Science, 148(2):281–301, 1995.

    Article  MathSciNet  MATH  Google Scholar 

  19. P. Jančar. Decidability of bisimilarity for one-counter processes. Information and Computation, 158(1):1–17, 2000.

    Article  MathSciNet  MATH  Google Scholar 

  20. T. Jéron and C. Jard. Testing for unboundedness of fifo channels. Theoretical Computer Science, 113(1):93–117, 1993.

    Article  MATH  MathSciNet  Google Scholar 

  21. P. Jančar, A. Kučera, and R. Mayr. Deciding bisimulation-like equivalences with finite-state processes. Theoretical Computer Science, 258(1-2):409–433, 2001.

    Article  MathSciNet  MATH  Google Scholar 

  22. P. Jančar and F. Moller. Techniques for decidability and undecidability of bisimilarity. In Proc. 10th Int. Conf. Concurrency Theory (CONCUR’99), Eindhoven,The Netherlands, Aug. 1999, volume 1664 of Lecture Notes in Computer Science, pages 30–45. Springer, 1999.

    Google Scholar 

  23. R. Mayr. Lossy counter machines. Tech. Report TUM-I9830, Institut fur Informatik, TUM, Munich, Germany, October 1998.

    Google Scholar 

  24. R. Mayr. Undecidable problems in unreliable computations. In Proc. 4th Latin American Symposium on Theoretical Informatics (LATIN’2000), Punta del Este,Uruguay,Apr. 2000, volume 1776 of Lecture Notes in Computer Science, pages 377–386. Springer, 2000.

    Google Scholar 

  25. F. Moller. Infinite results. In Proc. 7th Int. Conf. Concurrency Theory (CONCUR’96),Pisa,Italy, Aug. 1996, volume 1119 of Lecture Notes in Computer Science, pages 195–216. Springer, 1996.

    Google Scholar 

  26. Wuxu Peng and S. Purushothaman Iyer. Data flow analysis of communicating finite state machines. ACM Transactions on Programming Languages and Systems, 13(3):399–442, 1991.

    Article  Google Scholar 

  27. Ph. Schnoebelen. Verifying lossy channel systems has nonprimitive recursive complexity. In preparation, 2001.

    Google Scholar 

  28. J.C. Shepherdson and H.E. Sturgis. Computability of recursive functions. Journal of the ACM, 10(2):217–255, 1963.

    Article  MATH  MathSciNet  Google Scholar 

  29. P. Zafiropulo, C. West, H. Rudin, D. Cowan, and D. Brand. Towards analysing and synthesizing protocols. IEEE Transactions on Communication, 28(4):651–661, 1980.

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Lab. Spécification & Vérification, ENS de Cachan & CNRS UMR 8643, 61, av. Pdt. Wilson, 94235, Cachan Cedex, France

    Ph. Schnoebelen

Authors
  1. Ph. Schnoebelen
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, Tokyo Institute of Technology Graduate School of Information Science and Engineering, 2-12-1 Oo-okayama, Meguro-ku, Tokyo, 152-8552, Japan

    Naoki Kobayashi

  2. Department of Computer and Information Science, University of Pennsylvania, 200 S. 33rd St., Philadelphia, PA, 19104, USA

    Benjamin C. Pierce

Rights and permissions

Reprints and permissions

Copyright information

© 2001 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Schnoebelen, P. (2001). Bisimulation and Other Undecidable Equivalences for Lossy Channel Systems. In: Kobayashi, N., Pierce, B.C. (eds) Theoretical Aspects of Computer Software. TACS 2001. Lecture Notes in Computer Science, vol 2215. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45500-0_19

Download citation

  • DOI: https://doi.org/10.1007/3-540-45500-0_19

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-42736-0

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation