Normalization of Linear Horn Clauses - Formal Methods: Foundations and Applications - page 242

Normalization of Linear Horn Clauses

Thomas Martin Gawlitza 1 , Helmut Seidl 2 , and Kumar Neeraj Verma 2

1 CNRS/VERIMAG
[e-mail]
2 Institut fur Informatik, TU Munchen, Germany
{ seidl,verma } @in.tum.de

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

1 Introduction

Horn clauses are a convenient formalism for expressing analyses of concurrent
programs. Horn clauses have, e.g., successfully been applied to the analysis of cryp-
tographic protocols [1] based on the Dolev-Yao model [4]. This model represents mes-
sages as first-order terms, where an all-powerful adversary can intercept all messages
sent during the protocol's execution, delete or replace them with other messages, and
generate new messages. Horn clauses provide a convenient mechanism for describing
an over-approximation of the set of messages that can be learned by the adversary after
arbitrary number of executions of such a protocol between different sets of participants.
Nielson et al. [12] introduced the class

H 1 of Horn clauses in order to model reach-
ability in the spi-calculus. They showed that finite sets of H 1 Horn clauses can be con-

verted into equivalent tree automata in exponential time. Finite sets of H 1 Horn clauses

thus define regular tree languages. Moreover, they showed that the satisfiability problem
for finite sets of

H 1 Horn clauses is DEXPTIME-hard. Independent of this work Wei-
denbach [13] showed earlier that the satisfiability problem for finite sets of

H 1 Horn
clauses is decidable. The sort resolution procedure of Weidenbach [13] has a double
exponential worst-case time-complexity and is therefore not optimal [7]. Based on the
work of Nielson et al. [12], Goubault-Larrecq [7] showed how to check satisfiability
of finite sets of

H 1 Horn clauses in exponential time by using ordered resolution with

VERIMAG is a joint laboratory of CNRS, Universite Joseph Fourier and Grenoble INP.