The temporal logic of rewriting: A gentle introduction

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.