The temporal logic of rewriting: A gentle introduction

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


This paper presents the temporal logic of rewriting . Syntactically, is a very simple extension of which just adds action atoms, in the form of spatial action patterns, to . Semantically and pragmatically, however, when used together with rewriting logic as a "tandem" of system specification and property specification logics, it has substantially more expressive power than purely state-based logics like , or purely action-based logics like A- . Furthermore, it avoids the system/property mismatch problem experienced in state-based or action-based logics, which makes many useful properties inexpressible in those frameworks without unnatural changes to a system's specification. The advantages in expresiveness of are gained without losing the ability to use existing tools and algorithms to model check its properties: a faithful translation of models and formulas is given that allows verifying properties with model checkers.

Original languageEnglish (US)
Title of host publicationConcurrency, Graphs and Models - Essays Dedicated to Ugo Montanari on the Occasion of His 65th Birthday
Number of pages29
StatePublished - Jul 1 2008

Publication series

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

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'The temporal logic of rewriting: A gentle introduction'. Together they form a unique fingerprint.

Cite this