Equational Abstractions
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.
Document Details
- Document Type
- Technical Report
- Publication Date
- Jan 01, 2007
- Accession Number
- ADA482411
Entities
People
- José Meseguer
- Miguel Palomino
- Narciso Martí-oliet
Organizations
- University of Illinois Urbana–Champaign