Normalization of Linear Horn Clauses

Abstract

Nielson et al. [12] exhibit a rich class of Horn clauses which they call ${\cal H}_1$. Least models of finite sets of ${\cal H}_1$ Horn clauses are regular tree languages. Nielson et al. [12] describe a normalization procedure for computing least models of finite sets of ${\cal H}_1$ Horn clauses in the form of tree automata. In the present paper, we simplify and extend this normalization procedure to a semi-procedure that deals with finite sets of linear Horn clauses. The extended semi-procedure does not terminate in general but does so on useful subclasses of finite sets of linear Horn clauses. The extension in particular coincides with the normalization procedure of Nielson et al. [12] for sets of ${\cal H}_1$ Horn clauses. In order to demonstrate the usefulness of the extension, we show how backward reachability analysis for constrained dynamic pushdown networks (see Bouajjani et al. [3]) can be encoded into a class of finite sets of linear Horn clauses for which our normalization procedure terminates after at most exponentially many steps.