Algebraic simulations

José Meseguer, Miguel Palomino, Narciso Martí-Oliet

Research output: Contribution to journalArticle

Abstract

Rewriting logic is a flexible and general logic to specify concurrent systems. To prove properties about concurrent systems in temporal logic, it is very useful to use simulations that relate the transitions and atomic predicates of a system to those of a potentially much simpler one; then, if the simpler system satisfies a property φ in a suitable temporal logic we are guaranteed that the more complex system does too. In this paper, the suitability of rewriting logic as a formal framework not only to specify concurrent systems but also to specify simulations is explored in depth. For this, increasingly more general notions of simulation (allowing stuttering) are first defined for Kripke structures, and suitable temporal logics allowing properties to be reflected back by such simulations are characterized. The paper then proves various representability results à la Bergstra and Tucker, showing that recursive Kripke structures and recursive simulation maps (resp. r.eṡimulation relations) can always be specified in a finitary way in rewriting logic. Using simulations typically requires both model checking and theorem proving, since their correctness requires discharging proof obligations. In this regard, rewriting logic, by containing equational logic as a sublogic and having equationally-based inductive theorem proving at its disposal, is shown to be particularly well-suited for verifying the correctness of simulations.

Original languageEnglish (US)
Pages (from-to)103-143
Number of pages41
JournalJournal of Logic and Algebraic Programming
Volume79
Issue number2
DOIs
StatePublished - Feb 1 2010

Keywords

  • Kripke structures
  • Model checking
  • Representability results
  • Rewriting logic
  • Stuttering simulations

ASJC Scopus subject areas

  • Software
  • Theoretical Computer Science
  • Logic
  • Computational Theory and Mathematics

Fingerprint Dive into the research topics of 'Algebraic simulations'. Together they form a unique fingerprint.

  • Cite this