Predicate abstraction of rewrite theories

For an infinite-state concurrent system 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 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 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 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.