Checking chase termination: Cyclicity analysis and rewriting techniques

The aim of this paper is to present more general criteria and techniques for chase termination. We first present extensions of the well-known stratification criterion and introduce a new criterion, called local stratification, which generalizes both super-weak acyclicity and stratification -based criteria (including the class of constraints which are inductively restricted). Next, the paper presents a rewriting algorithm transforming the original set of constraints Σ into an "equivalent" set Σ^α and verifying the structural properties for chase termination on Σ^α. The rewriting of constraints allows us to recognize larger classes of constraints for which chase termination is guaranteed. In particular, we show that if Σ satisfies chase termination conditions Τ, then the rewritten set Σ^α satisfies Τ as well, but the vice versa is not true, that is there are significant classes of constraints for which Σ^α satisfies Τ and Σ does not. A more general rewriting algorithm producing as output an equivalent set of dependencies and a Boolean value stating whether a sort of cyclicity has been detected is also proposed. The new rewriting technique and the checking of acyclicity allow us to introduce the class of acyclic constraints, which generalizes local stratification and guarantees that all chase sequences are finite with a length polynomial in the size of the input database.