Affordable Access

Publisher Website

Equational abstractions

Authors
Journal
Theoretical Computer Science
0304-3975
Publisher
Elsevier
Publication Date
Volume
403
Identifiers
DOI: 10.1016/j.tcs.2008.04.040
Keywords
  • Rewriting Logic
  • Maude
  • Algebraic Specification
  • Model Checking
  • Ltl
  • Abstractions
Disciplines
  • Mathematics

Abstract

Abstract 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 in the Maude formal environment.

There are no comments yet on this publication. Be the first to share your thoughts.

Statistics

Seen <100 times
0 Comments

More articles like this

Equational Abstractions for Model Checking Erlang...

on Electronic Notes in Theoretica... Jan 01, 2005

Equational Abstractions for Reducing the State Spa...

on Electronic Notes in Theoretica... Jan 01, 2009

About the implementability and the power of equati...

on Theoretical Computer Science Jan 01, 1981

<abstractions>

Oct 02, 2003
More articles like this..