Algebraic Simulations

Meseguer, José; Palomino, Miguel; Marti-Oliet, Narciso

Permalink

https://hdl.handle.net/2142/11382 Copy

Description

Title

Algebraic Simulations

Author(s)

• Meseguer, José
• Palomino, Miguel
• Marti-Oliet, Narciso

Issue Date

2007-08

Keyword(s)

computer science

Abstract

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

Type of Resource

text

Permalink

http://hdl.handle.net/2142/11382

Copyright and License Information

You are granted permission for the non-commercial reproduction, distribution, display, and performance of this technical report in any format, BUT this permission is only for a period of 45 (forty-five) days from the most recent time that you verified that this technical report is still available from the University of Illinois at Urbana-Champaign Computer Science Department under terms that include this permission. All other rights are reserved by the author(s).

Owning Collections