Anzeige
Erschienen in:
2014 | OriginalPaper | Buchkapitel
Predicate Abstraction of Rewrite Theories
verfasst von : Kyungmin Bae, José Meseguer
Erschienen in: Rewriting and Typed Lambda Calculi
Verlag: Springer International Publishing
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
For an infinite-state concurrent system
$\mathcal{S}$
with a set
AP
of state predicates, its
predicate abstraction
defines a finite-state system whose states are subsets of
AP
, and its transitions
s
→
s
′ are witnessed by concrete transitions between states in
$\mathcal{S}$
satisfying the respective sets of predicates
s
and
s
′. Since it is not always possible to find such witnesses, an over-approximation adding extra transitions is often used. For systems
$\mathcal{S}$
described by formal specifications, predicate abstractions are typically built using various automated deduction techniques. This paper presents a new method—based on rewriting, semantic unification, and variant narrowing—to automatically generate a predicate abstraction when the formal specification of
$\mathcal{S}$
is given by a conditional rewrite theory. The method is illustrated with concrete examples showing that it naturally supports abstraction refinement and is quite accurate, i.e., it can produce abstractions not needing over-approximations.