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.