TY - GEN

T1 - Normalization of linear horn clauses

AU - Gawlitza, Thomas Martin

AU - Seidl, Helmut

AU - Verma, Kumar Neeraj

PY - 2011

Y1 - 2011

N2 - Nielson et al. [12] exhibit a rich class of Horn clauses which they call . Least models of finite sets of Horn clauses are regular tree languages. Nielson et al. [12] describe a normalization procedure for computing least models of finite sets of 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 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.

AB - Nielson et al. [12] exhibit a rich class of Horn clauses which they call . Least models of finite sets of Horn clauses are regular tree languages. Nielson et al. [12] describe a normalization procedure for computing least models of finite sets of 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 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.

UR - http://www.scopus.com/inward/record.url?scp=79953062763&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-19829-8_16

DO - 10.1007/978-3-642-19829-8_16

M3 - Conference contribution

AN - SCOPUS:79953062763

SN - 9783642198281

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 242

EP - 257

BT - Formal Methods

T2 - 13th Brazilian Symposium on Formal Methods, SBMF 2010

Y2 - 8 November 2010 through 11 November 2010

ER -