Equational abstractions

José Meseguer, Miguel Palomino, Narciso Martí-Oliet

Research output: Contribution to journalArticlepeer-review


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.

Original languageEnglish (US)
Pages (from-to)239-264
Number of pages26
JournalTheoretical Computer Science
Issue number2-3
StatePublished - Aug 28 2008


  • Abstractions
  • Algebraic specification
  • LTL
  • Maude
  • Model checking
  • Rewriting logic

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Equational abstractions'. Together they form a unique fingerprint.

Cite this