Skip to main content
SpringerLink
Log in
Book cover

Annual Symposium on Theoretical Aspects of Computer Science

STACS 2001: STACS 2001 pp 39–50Cite as

2-Nested Simulation Is Not Finitely Equationally Axiomatizable

  • Conference paper
  • First Online:

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

Abstract

2-nested simulation was introduced by Groote and Vaan- drager [10] as the coarsest equivalence included in completed trace equiv- alence for which the tyft/tyxt format is a congruence format. In the linear time-branching time spectrum of van Glabbeek [8], 2-nested simulation is one of the few equivalences for which no finite equational axiomati- zation is presented. In this paper we prove that such an axiomatization does not exist for 2-nested simulation.

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. L. Aceto, Z. Ésik, and A. Ingólfsdóttir, On the two-variable fragment of the equational theory of the max-sum algebra of the natural numbers, in Proceedings of the 17th STACS, H. Reichel and S. Tison, eds., vol. 1770 of Lecture Notes in Computer Science, Springer-Verlag, Feb. 2000, pp. 267–278.

    Google Scholar 

  2. L. Aceto, Z. Ésik, and A. Ingólfsdóttir, The max-plus algebra of the natural numbers has no finite equational basis, research report, BRICS, Department of Computer Science, Aalborg University, October 1999. Pp. 25. To appear in Theoretical Computer Science.

    Google Scholar 

  3. L. Aceto, W. Fokkink, and A. Ingólfsdóttir,A menagerie of non-finitely based process semantics over BPA * from ready simulation to completed traces, Mathematical Structures in Computer Science, 8 (1998), pp. 193–230.

    Article  MATH  Google Scholar 

  4. J. Baeten and J. Klop, eds., Proceedings CONCUR 90, Amsterdam, vol. 458 of Lecture Notes in Computer Science, Springer-Verlag, 1990.

    Google Scholar 

  5. J. Bergstra and J. W. Klop, Fixed point semantics in process algebras, Report IW 206, Mathematisch Centrum, Amsterdam, 1982.

    Google Scholar 

  6. J. H. Conway, Regular Algebra and Finite Machines, Mathematics Series (R. Brown and J. De Wet eds.), Chapman and Hall, London, United Kingdom, 1971.

    Google Scholar 

  7. J. L. Gischer, The equational theory of pomsets, Theoretical Comput. Sci., 61 (1988), pp. 199–224.

    Article  MathSciNet  MATH  Google Scholar 

  8. R. van Glabbeek, The linear time-branching time spectrum, in Baeten and Klop [4], pp. 278–297.

    Google Scholar 

  9. J. F. Groote, A new strategy for proving ωcompleteness with applications in process algebra, in Baeten and Klop [4], pp. 314–331.

    Google Scholar 

  10. J. F. Groote and F. Vaandrager, Structured operational semantics and bisimulation as a congruence, Information and Computation, 100 (1992), pp. 202–260.

    Article  MATH  MathSciNet  Google Scholar 

  11. R. Keller, Formal verification of parallel programs, Comm. ACM, 19 (1976), pp. 371–384.

    MATH  Google Scholar 

  12. H. Lin, An interactive proof tool for process algebras, in 9th Annual Symposium on Theoretical Aspects of Computer Science, vol. 577 of Lecture Notes in Computer Science, Cachan, France, 13-15 Feb. 1992, Springer, pp. 617–618.

    Google Scholar 

  13. R. Milner, An algebraic definition of simulation between programs, in Proceedings 2nd Joint Conference on Artificial Intelligence, William Kaufmann, 1971, pp. 481–489.

    Google Scholar 

  14. —, Communication and Concurrency, Prentice-Hall International, Englewood Cliffs, 1989.

    Google Scholar 

  15. W. Mitchell and D. Carlisle, Modal observation equivalence of processes, Technical Report UMCS–96–1–1, Manchester University, Computer Science, 1996.

    Google Scholar 

  16. F. Moller, The importance of the left merge operator in process algebras, in Proceedings 17th ICALP, Warwick, M. Paterson, ed., vol. 443 of Lecture Notes in Computer Science, Springer-Verlag, July 1990, pp. 752–764.

    Google Scholar 

  17. —, The nonexistence of finite axiomatisations for CCS congruences, in Proceedings 5th Annual Symposium on Logic in Computer Science, Philadelphia, USA, IEEE Computer Society Press, 1990, pp. 142–153.

    Google Scholar 

  18. G. Plotkin, A structural approach to operational semantics, Report DAIMI FN-19, Computer Science Department, Aarhus University, 1981.

    Google Scholar 

  19. V. Redko, On defining relations for the algebra of regular events, Ukrainskii Matematicheskii Zhurnal, 16 (1964), pp. 120–126. In Russian.

    MathSciNet  Google Scholar 

  20. P. Sewell, Nonaxiomatisability of equivalences over finite state processes, Annals of Pure and Applied Logic, 90 (1997), pp. 163–191.

    Article  MATH  MathSciNet  Google Scholar 

  21. S.K. Shukla, D.J. Rosenkrantz, H.B. Hunt iii, and R. E. Stearns, A HORNSAT based approach to the polynomial time decidability of simulation relations for finite state processes, in DIMACS Workshop on Satisfiability Problem: Theory and Applications, D. Du, J. Gu, and P. M. Pardalos, eds., vol. 35 of DIMACS Series in Discrete Mathematics and Computer cience, 1996, pp. 603–642.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. BRICS(Basic Research in Computer Science) Centre of the Danish National Research Foundation Department of Computer Science, Aalborg University, Fr. Bajersvej 7E, 9220, Aalborg Ø, Denmark

    Luca Aceto & Anna Ingólfsdóttir

  2. Department of Software Engineering, CWI, Kruislaan 413, 1098 SJ, Amsterdam, The Netherlands

    Wan Fokkink

Authors
  1. Luca Aceto
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Wan Fokkink
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Anna Ingólfsdóttir
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. I3S & INRIA Sophia Antipolis INRIA, CNRS, 2004 Route des Lucioles, 06902, Sophia-Antipolis, France

    Afonso Ferreira

  2. Institut für Theoretische Informatik, Fakultät Informatik, TU Dresden, 01062, Dresden, Germany

    Horst Reichel

Rights and permissions

Reprints and permissions

Copyright information

© 2001 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Aceto, L., Fokkink, W., Ingólfsdóttir, A. (2001). 2-Nested Simulation Is Not Finitely Equationally Axiomatizable. In: Ferreira, A., Reichel, H. (eds) STACS 2001. STACS 2001. Lecture Notes in Computer Science, vol 2010. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44693-1_4

Download citation

  • DOI: https://doi.org/10.1007/3-540-44693-1_4

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

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

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation