IMDEA Software

Iniciativa IMDEA

Inicio > Eventos > Charlas Invitadas > 2008 > The Temporal Logic of Rewriting
Esta página aún no ha sido traducida. A continuación se muestra la página en inglés.

Jose Meseguer

miércoles 2 de abril de 2008

11:00am Amphitheatre H-1002

Jose Meseguer, Profesor, University of Illinois at Urbana-Champaign

The Temporal Logic of Rewriting


This talk presents the temporal logic of rewriting TLR*. Syntactically, TLR* is a very simple extension of CTL* which just adds action atoms, in the form of spatial action patterns, to CTL*. 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 CTL*, or purely action-based logics like A-CTL*.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 TLR* 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 TLR* properties with CTL* model checkers.