Advertisement

Bisimulation and Other Undecidable Equivalences for Lossy Channel Systems

  • Ph. Schnoebelen
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2215)

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

Keywords

Channel System Label Transition System Behavioral Equivalence Counter Machine Extended Rule 
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. [AAB99]
    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. [ABJ98]
    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. [ABPJ00]
    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. [AJ96a]
    P.A. Abdulla and B. Jonsson. Undecidable verification problems for programs with unreliable channels. Information and Computation, 130(1):71–90, 1996.zbMATHCrossRefMathSciNetGoogle Scholar
  5. [AJ96b]
    P.A. Abdulla and B. Jonsson. Verifying programs with unreliable channels. Information and Computation, 127(2):91–101, 1996.zbMATHCrossRefMathSciNetGoogle Scholar
  6. [AK95]
    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. [AKP97]
    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. [BCMS01]
    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. [BM99]
    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. [Boc78]
    G. von Bochmann. Finite state description of communication protocols. Computer Networks and ISDN Systems, 2:361–372, 1978.Google Scholar
  11. [BZ81]
    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.MathSciNetGoogle Scholar
  12. [CF97]
    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. [CFP95]
    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.CrossRefGoogle Scholar
  14. [Fin94]
    A. Finkel. Decidability of the termination problem for completely specificied protocols. Distributed Computing, 7(3):129–135, 1994.CrossRefGoogle Scholar
  15. [Gla01]
    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. [GV93]
    R.J. van Glabbeek and F.W. Vaandrager. Modular specification of process algebras. Theoretical Computer Science, 113(2):293–348, 1993.zbMATHCrossRefMathSciNetGoogle Scholar
  17. [HJ99]
    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. [Jan95]
    P. Jančar. Undecidability of bisimilarity for Petri nets and some related problems. Theoretical Computer Science, 148(2):281–301, 1995.CrossRefMathSciNetzbMATHGoogle Scholar
  19. [Jan00]
    P. Jančar. Decidability of bisimilarity for one-counter processes. Information and Computation, 158(1):1–17, 2000.CrossRefMathSciNetzbMATHGoogle Scholar
  20. [JJ93]
    T. Jéron and C. Jard. Testing for unboundedness of fifo channels. Theoretical Computer Science, 113(1):93–117, 1993.zbMATHCrossRefMathSciNetGoogle Scholar
  21. [JKM01]
    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.CrossRefMathSciNetzbMATHGoogle Scholar
  22. [JM99]
    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. [May98]
    R. Mayr. Lossy counter machines. Tech. Report TUM-I9830, Institut fur Informatik, TUM, Munich, Germany, October 1998.Google Scholar
  24. [May00]
    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. [Mol96]
    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. [PP91]
    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.CrossRefGoogle Scholar
  27. [Sch01]
    Ph. Schnoebelen. Verifying lossy channel systems has nonprimitive recursive complexity. In preparation, 2001.Google Scholar
  28. [SS63]
    J.C. Shepherdson and H.E. Sturgis. Computability of recursive functions. Journal of the ACM, 10(2):217–255, 1963.zbMATHCrossRefMathSciNetGoogle Scholar
  29. [ZWR+80]
    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.CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Ph. Schnoebelen
    • 1
  1. 1.Lab. Spécification & VérificationENS de Cachan & CNRS UMR 8643Cachan CedexFrance

Personalised recommendations