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

Systematically we do this as follows. We consider the constraint Φ to be given by the
finite word automaton A =( Q, P ,δ,Φ,F ),where Q is the set of states, the set of

control states P is the alphabet, δ

Q is the transition relation, the constraint
Φ is identified as the initial state, and F is the set of accepting states. The set S Constr ( A )
is the smallest set of Horn clauses that fulfills the following properties:

⊆ Q × P ×

S Constr ( A ),if Φ ∈ 1. Q Φ ([]) ⇐ ∈ F .

2. Q Φ 1 ( x N :: x L ) ⇐ P ( x N ,p,x 1 ,x 2 ) ∧ Q Φ 2 ( x L ) ∈ S Constr ( A ),if( Φ 1 ,p,Φ 2 ) ∈ δ .

If we denote a finite word-automaton accepting Φ by A Φ , then the set S Constr ( A Φ ) con-

tains the Horn clauses that define the predicate Q Φ . We collect all Horn clauses which
are necessary to describe all constraints in the set S CDPN ( M ), i.e., S CDPN ( M ) is the
union of all S Constr ( A Φ ),where Φ is a constraint that appears in M . Finally we collect
all Horn clauses from the sets S CDPN ( M ) and S CDPN ( M ) in the set S CDPN ( M ),i.e.
we set S CDPN ( M ):= S CDPN ( M ) ∪

S CDPN ( M ).
Example 5. For a CDPN M that consists of the transition rules P ∗ : pa

→ pqa ,

P ∗ : qa → #,and# ∗ : pa → #,weget

S CDPN ( M )= { P ( x N ,p,x S ,x N :: x L ) ∧ P ( x N ,q,a 0 , []) , P ( x N ,p,ax S ,x L ) ⇐

P ( x N ,q,ax S ,x L ) ⇐ P ( x N , # ,x S ,x L ) ,

P ( x N ,p,ax S ,x L ) ⇐ P ( x N , # ,x S ,x L ) ∧ Q # ∗ ( x L ) }

S CDPN ( M )= {

Q # ∗ ([]) ⇐ , Q # ∗ ( x N :: x L ) ⇐ P ( x N , # ,x 1 ,x 2 ) ∧ Q # ∗ ( x L ) }

For obvious reasons it is not necessary to define the predicate Q P ∗ .

For the remainder of the section let C ⊆ Proc be a regular set of configurations and

S C be a set of normal Horn clauses that fulfills properties 2 and 3 of lemma 3 such that
L 1 ( S C ) ∪ S CDPN ( M ) represents the

pre ∗ M -image of C precisely under the assumption that all constraints are stable:
Lemma 4. pre ∗ M ( L i ( S C )) ⊆L i ( S C ∪

... ∪L N ( S C )= C holds for some N ∈ N . S C ∪

S CDPN ( M )) for all i . Equality holds, whenever

all constraints are stable.

The set S C ∪ S CDPN ( M ) of Horn clauses only consists of linear Horn clauses. Actually,

our normalization semi-procedure computes the least model of S C ∪

S CDPN ( M ) in

at most exponentially many steps. We emphasize that the set S C ∪

S CDPN ( M )

of

H 1 Horn
clauses by instantiation. This is impossible, because the third argument and the fourth
argument of the predicate P are not always finite, i.e., the sets

linear Horn clauses cannot be transformed into an equivalent finite set of

{t 3 | ( t 1 ,t 2 ,t 3 ,t 4 ) ∈

H S C ∪S CDPN ( M ) ( P ) } and { t 4 | ( t 1 ,t 2 ,t 3 ,t 4 ) ∈H S C ∪S CDPN ( M ) ( P ) } can be infinite.

The first argument of P can be instantiated, since it is finite.

4Con lu ion

We extended the normalization procedure of Nielson et al. [12] for H 1 Horn clauses

to a normalization semi-procedure for linear Horn clauses. As a nontrivial application,