Skip to main content

Bisimilarity Congruences for Open Terms and Term Graphs via Tile Logic

  • Conference paper
  • First Online:
CONCUR 2000 — Concurrency Theory (CONCUR 2000)

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

Included in the following conference series:

Abstract

The definition of sos formats ensuring that bisimilarity on closed terms is a congruence has received much attention in the last two decades. For dealing with open terms, the congruence is usually lifted from closed terms by instantiating the free variables in all possible ways; the only alternatives considered in the literature are Larsen and Xinxin’s context systems and Rensink’s conditional transition systems. We propose an approach based on tile logic, where closed and open terms are managed uniformly, and study the ‘bisimilarity as congruence’ property for several tile formats, accomplishing different concepts of open system.

Research supported by CNR Integrated Project Progettazione e Verifica di Sistemi Eterogenei, Esprit WG CONFER2 and COORDINA, MURST project TOSCA, and CICYT project Desarrollo Formal de Sistemas Distribuidos (TIC97-0669-C03-01).

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

Access this chapter

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.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. B. Bloom, S. Istrail, and A. R. Meyer. Bisimulation can’t be traced. Journal of the ACM, 42(1):232–268, 1995.

    Article  MATH  MathSciNet  Google Scholar 

  2. R. Bruni, Tile Logic for Synchronized Rewriting of Concurrent Systems, Ph.D. Thesis TD-1/99, Computer Science Department, University of Pisa, 1999.

    Google Scholar 

  3. R. Bruni, D. de Frutos-Escrig, N. Martí-Oliet, and U. Montanari. Tile bisimilarity congruences for open terms and term graphs. Technical Report TR-00-06, Computer Science Department, University of Pisa, 2000.

    Google Scholar 

  4. R. Bruni, J. Meseguer, and U. Montanari. Process and term tile logic. Technical Report SRI-CSL-98-06, SRI International, 1998.

    Google Scholar 

  5. R. Bruni, U. Montanari, and V. Sassone. Open ended systems, dynamic bisimulation and tile logic. In Proc. IFIP-TCS 2000, LNCS. Springer, 2000. To appear.

    Google Scholar 

  6. A. Corradini and F. Gadducci. An algebraic presentation of term graphs, via gs-monoidal categories. Applied Categorical Structures, 7(4):299–331, 1999.

    Article  MATH  MathSciNet  Google Scholar 

  7. A. Corradini and U. Montanari. An algebraic semantics for structured transition systems and its application to logic programs. Th. Comput. Sci., 103:51–106, 1992.

    Article  MATH  MathSciNet  Google Scholar 

  8. R. De Simone. Higher level synchronizing devices in MEIJE-SCCS. Theoret. Comput. Sci., 37:245–267, 1985.

    Article  MATH  MathSciNet  Google Scholar 

  9. M. C. van Eekele, M. J. Plasmeijer, and M. R. Sleep, editors. Term Graph Rewriting: Theory and Practice, Wiley, London, 1993.

    Google Scholar 

  10. F. Gadducci and U. Montanari. Rewriting rules and CCS. in Proceeding WRLA’ 96, vol. 4 of Elect. Notes in Th. Comput. Sci., Elsevier Science, 1996.

    Google Scholar 

  11. F. Gadducci and U. Montanari. The tile model. In Proof, Language and Interaction: Essays in Honour of Robin Milner. MIT Press, 1999. To appear.

    Google Scholar 

  12. J. F. Groote and F. Vaandrager. Structured operational semantics and bisimulation as a congruence. Information and Computation, 100:202–260, 1992.

    Article  MATH  MathSciNet  Google Scholar 

  13. F. W. Lawvere. Functorial semantics of algebraic theories. Proc. National Academy of Science, 50:869–872, 1963.

    Article  MATH  MathSciNet  Google Scholar 

  14. K. G. Larsen and L. Xinxin. Compositionality through an operational semantics of contexts. In Proc. ICALP’90, vol. 443 of LNCS, pages 526–539, Springer, 1990.

    Google Scholar 

  15. J. Meseguer. Conditional rewriting logic as a unified model of concurrency. Theoret. Comput. Sci., 96:73–155, 1992.

    Article  MATH  MathSciNet  Google Scholar 

  16. J. Meseguer and U. Montanari. Mapping tile logic into rewriting logic. In Proc. WADT’97, vol. 1376 of LNCS, pages 62–91. Springer, 1998.

    Google Scholar 

  17. R. Milner. A Calculus of Communicating Systems, vol. 92 of LNCS Springer, 1980.

    MATH  Google Scholar 

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

    Google Scholar 

  19. A. Rensink. Bisimilarity of open terms. Inform. and Comput. 156:345–385, 2000.

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2000 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Bruni, R., de Frutos-Escrig, D., Martí-Oliet, N., Montanari, U. (2000). Bisimilarity Congruences for Open Terms and Term Graphs via Tile Logic. In: Palamidessi, C. (eds) CONCUR 2000 — Concurrency Theory. CONCUR 2000. Lecture Notes in Computer Science, vol 1877. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44618-4_20

Download citation

  • DOI: https://doi.org/10.1007/3-540-44618-4_20

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-67897-7

  • Online ISBN: 978-3-540-44618-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics