Mapping tile logic into rewriting logic

José Meseguer, Ugo Montanari

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Rewriting logic extends to concurrent systems with state changes the body of theory developed within the algebraic semantics approach. It is both a foundational tool and the kernel language of several implementation efforts (Cafe, ELAN, Mande). Tile logic extends (unconditional) rewriting logic since it takes into account state changes with side effects and synchronization. It is especially useful for defining compositional models of computation of reactive systems, coordination languages, mobile calculi, and causal and located concurrent systems. In this paper, the two logics are defined and compared using a recently developed algebraic specification methodology, membership equational logic. Given a theory T, the rewriting logic of T is the free monoidal S-category, and the tile logic of T is the free monoidal double category, both generated by T. An extended version of monoidal 2-categories, called g VH-categories, is also defined, able to include in an appropriate sense the structure of monoidal double categories. We show that 2VH-categories correspond to an extended version of rewriting logic, which is able to embed tile logic, and which can be implemented in the basic version of rewriting logic using suitable internal strategies. These strategies can be significantly simpler when the theory is uniforra. A uniform theory is provided in the paper for CCS, and it is conjectured that uniform theories exist for most process algebras.

Original languageEnglish (US)
Title of host publicationRecent Trends in Algebraic Development Techniques - 12th International Workshop, WADT 1997, Selected Papers
EditorsFrancesco Parisi Presicce
PublisherSpringer-Verlag
Pages62-91
Number of pages30
ISBN (Print)3540642994, 9783540642992
DOIs
StatePublished - Jan 1 1998
Externally publishedYes
Event12th International Workshop on Algebraic Development Techniques, WADT 1997 - Tarquinia, Italy
Duration: Jun 3 1997Jun 7 1997

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume1376
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other12th International Workshop on Algebraic Development Techniques, WADT 1997
CountryItaly
CityTarquinia
Period6/3/976/7/97

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Mapping tile logic into rewriting logic'. Together they form a unique fingerprint.

  • Cite this

    Meseguer, J., & Montanari, U. (1998). Mapping tile logic into rewriting logic. In F. P. Presicce (Ed.), Recent Trends in Algebraic Development Techniques - 12th International Workshop, WADT 1997, Selected Papers (pp. 62-91). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1376). Springer-Verlag. https://doi.org/10.1007/3-540-64299-4_27