Equational abstractions

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

Full description

Saved in:
Bibliographic Details
Published in:Theoretical computer science 2008-08, Vol.403 (2), p.239-264
Main Authors: Meseguer, José, Palomino, Miguel, Martí-Oliet, Narciso
Format: Article
Language:English
Subjects:
Abstractions
Algebraic specification
Algorithmics. Computability. Computer arithmetics
Applied sciences
Computer science
control theory
systems
Exact sciences and technology
General logic
Logic and foundations
LTL
Mathematical logic, foundations, set theory
Mathematics
Maude
Miscellaneous
Model checking
Rewriting logic
Sciences and techniques of general use
Theoretical computing
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:0304-3975
1879-2294
DOI:10.1016/j.tcs.2008.04.040