Algebraic Simulations

A fruitful approach to the study of state-based systems consists in their mathematical formalization by means of models like Kripke structures. They allow verification of their associated properties using simulations that relate one Kripke structure to another, for example, to simpler abstractions, or to a more complex implementation. This work tries to advance two main goals along those lines: the first, to generalize the notion of simulation between Kripke structures as much as possible, and the second, to provide general representability results showing that Kripke structures and generalized simulations can be represented in rewriting logic, an executable logical framework with good properties for representing many concurrent systems. The reason for trying to advance the first goal is that simulations are essential for compositional reasoning. A cornerstone in such reasoning is the result that simulations reflect temporal logic properties, that is, if a Kripke structure B simulates another A, and B satisfies a temporal logic formula in a suitable class of formulas, then A does so too. Since results of this kind are very powerful, there are strong reasons to generalize them. Advancing the second goal yields three important benefits: (i) executability, (ii) ease of specification, and (iii) ease of proof. The point about (i) and (ii) is that rewriting logic is a very flexible framework, so that concurrent systems can usually be specified quite easily and at a very high level; furthermore, such specifications can be used directly to execute a system, or to reason about it, which is point (iii)