TY - JOUR

T1 - Algebraic simulations

AU - Meseguer, José

AU - Palomino, Miguel

AU - Martí-Oliet, Narciso

N1 - Funding Information:
Research supported by ONR Grant N00014-02-1-0715, NSF Grant CCR-0234524, by DARPA through Air Force Research Laboratory Contract F30602-02-C-0130, by the Spanish projects MIDAS TIC2003-01000 and DESAFIOS TIN2006-15660-C02-01, and by Comunidad de Madrid program PROMESAS S-0505/TIC/0407. *Corresponding author. E-mail addresses: meseguer@cs.uiuc.edu (J. Meseguer), miguelpt@sip.ucm.es (M. Palomino), narciso@sip.ucm.es (N. Martí-Oliet).

PY - 2010/2

Y1 - 2010/2

N2 - 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.

AB - 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.

KW - Kripke structures

KW - Model checking

KW - Representability results

KW - Rewriting logic

KW - Stuttering simulations

UR - http://www.scopus.com/inward/record.url?scp=72049113846&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=72049113846&partnerID=8YFLogxK

U2 - 10.1016/j.jlap.2009.07.003

DO - 10.1016/j.jlap.2009.07.003

M3 - Article

AN - SCOPUS:72049113846

VL - 79

SP - 103

EP - 143

JO - Journal of Logic Programming

JF - Journal of Logic Programming

SN - 1567-8326

IS - 2

ER -