Talk "Equational abstractions in rewriting logic and Maude"

by Narciso Martí-Oliet

Tue, 02 September 2014 at 09:00 am in Sinaia, Romania

Joint work with: J. Meseguer, M. Palomino, and F. Durán

Abstract: Maude is a high-level language and high-performance system supporting both equational and rewriting computation for a wide range of applications. Maude also provides a model checker for linear temporal logic. This procedure can be used to prove properties when the set of states reachable from an initial state in a system is finite; when this is not the case, it may be possible to use an equational abstraction technique for reducing the size of the state space. Abstraction reduces the problem of whether an infinite state system satisfies a temporal logic property to model checking that property on a finite state abstract version. The most common abstractions are quotients of the original system. We present a simple method of defining quotient abstractions by means of equations collapsing the set of states. Our method yields the minimal quotient system together with a set of proof obligations that guarantee its executability and can be discharged with tools such as those available in the Maude formal environment. The proposed method will be illustrated in a couple of detailed examples.