Accession Number:

ADA482411

Title:

Equational Abstractions

Descriptive Note:

Corporate Author:

ILLINOIS UNIV AT URBANA-CHAMPAIGN DEPT OF COMPUTER SCIENCE

Report Date:

2007-01-01

Pagination or Media Count:

37.0

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.

Subject Categories:

  • Theoretical Mathematics
  • Computer Hardware

Distribution Statement:

APPROVED FOR PUBLIC RELEASE