Skip to main content
SpringerLink
Log in
SpringerLink
Log in

Deciding bisimulation equivalences for a class of non-finite-state programs

  • Contributed Papers
  • Conference paper
  • First Online:
STACS 89 (STACS 1989)

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

Included in the following conference series:

Abstract

Traditionally, many automatic program verification techniques are applicable only to finite-state programs. In this paper we show how to extend some verification techniques to infinite-state programs that may read, store, and write data but not perform any other computations. We present algorithms for deciding strong equivalence and observation equivalence, defined by bisimulations (as in CCS), between such programs. These algorithms have major applications in verification of communication protocols. The equivalence problems are shown to be NP-hard in the size of the programs.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. S. Abramsky. Observation equivalence as a testing equivalence. Theoretical Computer Science, 53(2,3):225–241, 1987.

    Google Scholar 

  2. S. Brookes, C.A.R. Hoare, and W. Roscoe. A theory of communicating sequential processes. J. ACM, 31(3):560–599, 1984.

    Google Scholar 

  3. B. Bloom, S. Istrail, and A. Meyer. Bisimulation can't be traced: preliminary report. In Proc. 15th ACM PoPL, pages 229–239, 1988.

    Google Scholar 

  4. D. Brand and W. H. Joyner. Verification of protocols using symbolic execution. Computer Networks, 2(4–5):351–360, 1978.

    Google Scholar 

  5. D. Brand and W. H. Joyner. Verification of HDLC. IEEE Transactions on Communications, COM-30(5):1136–1142, 1982.

    Google Scholar 

  6. J. Bergstra and J. Klop. Verification of an Alternating Bit Protocol by means of Process Algebra. Technical Report, Centrum voor Wiskunde en Informatica, 1984.

    Google Scholar 

  7. E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite-state concurrent systems using temporal logics specification: a practical approach. In Proc. 10th ACM PoPL, pages 117–126, Austin, Texas, 1983.

    Google Scholar 

  8. T. W. Doeppner and A. Giacalone. A formal description of the UNIX operating system. In Proc. 2nd ACM PoDC, pages 241–253, 1983.

    Google Scholar 

  9. N. D. Jones and S. S. Muchnick. Even simple programs are hard to analyse. J. ACM, 24(2):338–350, April 1977.

    Google Scholar 

  10. B. Jonsson and J. Parrow. Deciding bisimulation equivalences for a class of non-finite-state programs. SICS Technical Report, In preparation.

    Google Scholar 

  11. C. Koomen. Algebraic specification and verification of protocols. Science of Computer Programming, 5(1):1–36, 1985.

    Google Scholar 

  12. P. C. Kanellakis and S. A. Smolka. CCS expressions, finite state processes, and three problems of equivalence. In Proc. 2nd ACM PoDC, pages 228–240, Montreal, Canada, 1983.

    Google Scholar 

  13. K. G. Larsen and R. Milner. Verifying a protocol using relativized bisimulation. In Proc. ICALP '87, LNCS 267, Springer Verlag, 1987.

    Google Scholar 

  14. R. Milner. A Calculus of Communicating Systems. Volume 92 of Lecture Notes of Computer Science, Springer Verlag, 1980.

    Google Scholar 

  15. R. Milner. Calculi for synchrony and asynchrony. Theoretical Computer Science, 25:267–310, 1983.

    Google Scholar 

  16. R. de Nicola and M. Hennessy. Testing equivalences for processes. Theoretical Computer Science, 34:83–133, 1984.

    Google Scholar 

  17. J. Parrow. Verifying a CSMA/CD-Protocol with CCS. Technical Report ECS-LFCS-87-18, Laboratory for Foundations of Computer Science, Department of Computer Science, University of Edinburgh, 1987. To appear in Protocol Specification, Testing, and Verification VIII (1988).

    Google Scholar 

  18. S.A. Smolka, A.J. Frank, and S.K. Debray. Testing protocol robustness the CCS way. In Protocol Specification, Testing, and Verification IV (1984), pages 93–108, 1985. North-Holland.

    Google Scholar 

  19. D. Vergamini. Verification by means of Observation Equivalence on Automata. Technical Report 501, INRIA, Sophia Antipolis, 1986.

    Google Scholar 

  20. M. Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proc. IEEE Symp. on Logic in Computer Science, pages 332–344, June 1986.

    Google Scholar 

  21. P. Wolper. Expressing interesting properties of programs in propositional temporal logic (extended abstract). In Proc. 13th ACM PoPL, pages 184–193, Jan. 1986.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Swedish Institute of Computer Science, Stockholm

    Bengt Jonsson & Joachim Parrow

  2. SICS, Box 1263, S-164 28, Kista, Sweden

    Bengt Jonsson & Joachim Parrow

Authors
  1. Bengt Jonsson
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Joachim Parrow
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

B. Monien R. Cori

Rights and permissions

Reprints and permissions

Copyright information

© 1989 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Jonsson, B., Parrow, J. (1989). Deciding bisimulation equivalences for a class of non-finite-state programs. In: Monien, B., Cori, R. (eds) STACS 89. STACS 1989. Lecture Notes in Computer Science, vol 349. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0029004

Download citation

  • DOI: https://doi.org/10.1007/BFb0029004

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-50840-3

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation