### 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 language | English (US) |
---|---|

Pages (from-to) | 103-143 |

Number of pages | 41 |

Journal | Journal of Logic and Algebraic Programming |

Volume | 79 |

Issue number | 2 |

DOIs | |

State | Published - 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

*Journal of Logic and Algebraic Programming*,

*79*(2), 103-143. https://doi.org/10.1016/j.jlap.2009.07.003