Introduction

One of the most challenging problems in the verification of reactive systems, is the extension of the model checking technique (see [9] for a thorough overview) to infinite state systems. In model checking the evolution over time of an infinite state system is modelled as a binary transition relation over an infinite set of states (such as n-tuples of integers or rationals) and the properties of that evolution are specified by means of propositional temporal formulas. In particular, in this paper we consider the Computation Tree Logic (CTL, for short), which is a branching time propositional temporal logic by which one can specify, among others, the so-called safety and liveness properties [9].

Unfortunately, when considering infinite state systems, the verification of CTL formulas is an undecidable problem, in general. In order to cope with this limitation, various decidable subclasses of systems and formulas have been identified (see, for instance, [1,14]). Other approaches enhance finite state model checking by using more general deductive techniques (see, for instance, [30,33]) or using abstractions, that is, mappings by which one can reduce an infinite state system to a finite state system, preserving the property of interest (see, for instance, [2,35]).

Also logic programming and constraint logic programming have been proposed as frameworks for specifying and verifying properties of reactive systems. Indeed, the fixpoint semantics of logic programming languages allows us to easily represent the fixpoint semantics of various temporal logics [13,27,31]. Moreover, constraints over the integers or the rationals can be used for providing finite representations of infinite sets of states [13,17].

However, for programs which specify infinite state systems, the proof procedures normally used in constraint logic programming (CLP), such as the extension to CLP of SLDNF resolution or tabled resolution [8], very often diverge when trying to check some given temporal properties. This is due to the limited ability of these proof procedures to cope with infinitely failed derivations. For this reason, instead of using direct program evaluation, many logic programmingbased verification methods make use of reasoning techniques such as: (i) static analysis [5,13] or (ii) program transformation [15,23,25,28,32].

In this paper we further develop the verification method presented in [15] and we assess its practical value. That method is applicable to specifications of CTL properties of infinite state systems encoded as constraint logic programs and it makes use of program specialization.

The specific contributions of this paper are the following. First, we have reformulated the specialization-based verification method of [15] as a two-phase method. Phase (1): the CLP specification is specialized w.r.t. the initial state of the system and the temporal property to be verified, and Phase (2): a bottom-up evaluation of the specialized program is performed. By doing so we are able to better evaluate the role of program specialization in the verification technique.

Then, we have defined various generalization strategies which can be used during Phase (1) of our verification method, for controlling when and how to perform generalization. Selecting a good generalization strategy is not a trivial task: it must guarantee the termination of the specialization phase itself, by introducing a finite number of specialization sub-problems, and it should provide a good balance between precision and performance. Indeed, the use of a too coarse generalization strategy may prevent one to prove the properties of interest, while an unnecessarily precise strategy may lead to verification times which are too high. The generalization strategies we consider in this paper have been specifically designed for CLP programs using the constraint domain of linear inequations over rationals.

We have implemented these strategies on the MAP transformation system [26], and we have applied them to several infinite state systems and properties taken from the literature. We have performed a comparative evaluation of generalization strategies in terms of efficiency and power, based on the analysis of the experimental results.

Finally, we have compared our MAP implementation with various constraintbased model checkers for infinite state systems and, in particular, with ALV [7], DMC [13], and HyTech [19].

The paper is organized as follows. In Section 2 we recall how CTL properties of infinite state systems can be encoded by using locally stratified CLP programs. In Section 3 we present our two-phase method for verification. In Section 4 we describe various strategies that can be applied during the specialization phase. These strategies differ for the generalization techniques used for ensuring the termination of the program specialization phase. In Section 5 we report on some experiments we have performed by using a prototype implementation of the MAP transformation system. Finally, we compare the results we have obtained using the MAP system with the results we have obtained using other verification systems.

Specifying CTL Properties by CLP Programs

We will model an infinite state system as a Kripke structure and we will represent a property to be verified as a formula of the Computation Tree Logic (CTL, for short). The fact that a CTL formula ϕ holds in a state s of a Kripke structure K will be denoted by K,s |= ϕ. (The reader who is not familiar with these notions may refer to the Appendix or to [9].) A Kripke structure can be encoded as a constraint logic program as indicated in the following four points [15,25,27]. (1) The set S of states is given as a set of n-tuples of the form t 1 , . . . , t n , where for i = 1, . . . , n, the term t i is either a rational number or an element of a finite domain. For reasons of simplicity, when denoting a state we will feel free to use a single variable X, instead of an n-tuple of variables of the form X 1 , . . . , X n .

(2) The set I of initial states is given as a set of clauses of the form: initial (X) ← c(X), where c(X) is a constraint. (3) The transition relation R is given as a set of clauses of the form:

t(X, Y ) ← c(X, Y ) where c(X, Y ) is a constraint. Y is called a successor state of X. We also define a predicate ts such that, for every state X, ts(X, Ys) holds iff Ys is a list of all the successor states of X, that is, for every state X, the state Y belongs to the list Ys iff t(X, Y ) holds. We refer to [16] for conditions that guarantee that Ys is a finite list and for an algorithm to construct the clauses defining ts from the clauses defining t. (4) The elementary properties which are associated with each state X by the labeling function L, are given by a set of clauses of the form: elem(X, e) ← c(X) where e is a constant, that is, the name of an elementary property, and c(X) is a constraint.

Given a Kripke structure K encoded by the clauses defining the predicates initial , t, ts, and elem, the satisfaction relation |= can be encoded by a predicate sat defined by the following clauses [15,25,27]

: 1. sat(X, F ) ← elem(X, F ) 2. sat(X, not(F )) ← ¬sat(X, F ) 3. sat(X, and (F 1 , F 2 )) ← sat(X, F 1 ), sat(X, F 2 ) 4. sat(X, ex (F )) ← t(X, Y ), sat(Y, F ) 5. sat(X, eu(F 1 , F 2 )) ← sat(X, F 2 ) 6. sat(X, eu(F 1 , F 2 )) ← sat(X, F 1 ), t(X, Y ), sat(Y, eu(F 1 , F 2 )) 7.

sat(X, af (F )) ← sat(X, F ) 8. sat(X, af (F )) ← ts(X, Ys), sat all (Ys, af (F )) 9. sat all ([ ], F ) ← 10. sat all ([X|Xs], F ) ← sat(X, F ), sat all (Xs, F ) Let P K denote the constraint logic program consisting of clauses 1-10 together with the clauses defining the predicates initial , t, ts, and elem. Now we will present a method for proving that a given CTL formula ϕ holds. We start by defining a new predicate prop as follows:

prop ≡ def ∀X(initial (X) → sat(X, ϕ)) This definition can be encoded by the following two clauses:

γ 1 : prop ← ¬negprop γ 2 : negprop ← initial (X), sat(X, not(ϕ))

The correctness of this encoding is stated by the following Theorem 1 and it is a consequence of the fact that program P K ∪ {γ 1 , γ 2 } is locally stratified and, hence, it has a unique perfect model M (P K ∪ {γ 1 , γ 2 }) [4]. The proof proceeds by structural induction on the CTL formula ϕ and is omitted for lack of space (see [16] for details).

Theorem 1 (Correctness of Encoding). Let K be a Kripke structure, let I be the set of initial states of K, and let ϕ be a CTL formula. Then, (for all states s ∈ I, K, s |= ϕ) iff prop ∈ M (P K ∪ {γ 1 , γ 2 }).

Example 1. Let us consider the reactive system depicted in Figure 1, where a term of the form s(X 1 , X 2 ) denotes the pair X 1 , X 2 of rationals. The Kripke structure K which models that system, is defined as follows. The initial states are given by the clause:

&% '$ ' & W X1 ≥ 1 X2 := X2 −1 s(X1,X2) $ % X1 ≤ 2 X2 := X2 +111. initial (s(X 1 , X 2 )) ← X 1 ≤ 0, X 2 = 0 The transition relation R is given by the clauses: 12. t(s(X 1 , X 2 ), s(Y 1 , Y 2 )) ← X 1 ≥ 1, Y 1 = X 1 , Y 2 = X 2 −1 13. t(s(X 1 , X 2 ), s(Y 1 , Y 2 )) ← X 1 ≤ 2, Y 1 = X 1 , Y 2 = X 2 +1

The elementary property negative is given by the clause:

14. elem(s(X 1 , X 2 ), negative) ← X 2 < 0 Let P K denote the program consisting of clauses 1-14. We omit the clauses defining the predicate ts, which are not needed in this example.

Suppose that we want to verify the following property: in every initial state s(X 1 , X 2 ), where X 1 ≤ 0 and X 2 = 0, the CTL formula not(eu(true, negative)) holds, that is, from any initial state it is impossible to reach a state s(X 1 , X 2 ) where X 2 < 0. By using the fact that not(not(ϕ)) is equivalent to ϕ, this property is encoded by the following two clauses:

γ 1 : prop ← ¬negprop γ 2 : negprop ← X 1 ≤ 0, X 2 = 0, sat(s(X 1 , X 2 )

, eu(true, negative)) Thus, by Theorem 1, in order to verify that in every initial state of K the CTL formula not(eu(true, negative)) holds, we need to show that prop ∈ M (P K ∪ {γ 1 , γ 2 }).

One of the most important features of the model checking techniques for finite state systems is the ability to find witnesses and counterexamples [9]. Our encoding of the Kripke structure can easily be extended to handle the generation of witnesses of formulas of the form eu(ϕ 1 , ϕ 2 ) and counterexamples of formulas of the form af (ϕ). For details, the interested reader may refer to Section 7 of [16].

Verifying Infinite State Systems by Specializing CLP Programs

In this section we present a method for checking whether or not prop ∈ M (P K ∪ {γ 1 , γ 2 }), where P K ∪ {γ 1 , γ 2 } is a CLP specification of an infinite state system and prop is a predicate encoding the satisfiability of a given CTL formula, as indicated in Section 2.

The checking technique based on the bottom-up construction of the perfect model M (P K ∪ {γ 1 , γ 2 }) is not feasible, in general, because this model may be infinite. Moreover, the proof procedures normally used in constraint logic programming, such as the extension of SLDNF resolution and tabled resolution to CLP, very often diverge when trying to check whether or not prop ∈ M (P K ∪ {γ 1 , γ 2 }). This is due to the limited ability of these proof procedures to cope with infinite failure.

It has been shown in [15] that program specialization often improves the treatment of infinite failure. In this section we present a reformulation of the method proposed in [15] by defining a verification algorithm working in two phases: (1) in the first phase we specialize the program P K ∪ {γ 1 , γ 2 } w.r.t. the query prop, that is, w.r.t. initial state of the system and the temporal property to be verified, and (2) in the second phase we construct the perfect model of the specialized program by a bottom-up evaluation. This separation into two phases allows the assessment of the effect of program specialization on the verification process as indicated in Section 5.

It is often the case that the specialization phase improves the termination of the construction of the perfect model. Indeed, in many cases the bottomup construction of the perfect model of the program P K ∪ {γ 1 , γ 2 } does not terminate because it does not take into account the information about the query to be evaluated and, in particular, about the initial states of the system. The specialization phase modifies the initial program P K ∪ {γ 1 , γ 2 } by incorporating into the specialized program P s the knowledge about the constraints that hold in the initial states. Therefore, the bottom-up construction of the perfect model of P s may exploit those constraints and terminate more often than the bottom-up construction of the perfect model of the initial program

P K ∪ {γ 1 , γ 2 }.

The Verification Algorithm Input:

The program P K ∪ {γ 1 , γ 2 }. Output: An Herbrand interpretation M s such that prop ∈ M (P K ∪ {γ 1 , γ 2 }) iff prop ∈ M s . (Phase 1) Specialize(P K ∪ {γ 1 , γ 2 }, P s ); (Phase 2) BottomUp(P s , M s )

The Specialize procedure of Phase (1) implements a program specialization strategy which makes use of the following transformation rules only: definition introduction, constrained atomic folding, positive unfolding, constrained atomic folding, removal of clauses with unsatisfiable body, and removal of subsumed clauses. Thus, Phase (1) is simpler than the specialization strategy presented in [15] which uses some extra rules such as negative unfolding, removal of useless clauses, and contextual constraint replacement.

Procedure Specialize Input: The Unfold procedure takes as input a clause γ ∈ InDefs of the form H ← c(X), sat(X, ψ), and returns as output a set Γ of clauses derived from γ as follows. The Unfold procedure first unfolds once γ w.r.t. sat(X, ψ) and then applies zero or more times the unfolding as long as in the body of a clause derived from γ there is an atom of one of the following forms: (i) t(s 1 , s 2 ), (ii) ts(s, ss), (iii) sat(s, e), where e is an elementary property, (iv) sat(s, not(ψ 1 )), (v) sat(s, and (ψ 1 , ψ 2 )), (vi) sat(s, ex (ψ 1 )), and (vii) sat all (ss, ψ 1 ), where ss is a non-variable list. Then the set of clauses derived from γ by applying the unfolding rule is simplified by removing: (i) every clause whose body contains an unsatisfiable constraint, and (ii) every clause which is subsumed a clause of the form H ← c, where c is a constraint. Due to the structure of the clauses defining the predicates t, ts, sat, and sat all , the Unfold procedure terminates for any ground term denoting a CTL formula ψ occurring in γ.

The program P K ∪ {γ 1 , γ 2 }. Output: A stratified program P s such that prop ∈ M (P K ∪ {γ 1 , γ 2 }) iff prop ∈ M (P s ).

The Generalize&Fold procedure takes as input the set Γ of clauses produced by the Unfold procedure and the set Defs of clauses, called definitions. A definition in Defs is a clause of the form newp(X) ← d(X), sat(X, ψ) which can be used for folding. The Generalize&Fold procedure introduces a set NewDefs of new definitions (which are then added to Defs) and, by folding the clauses in Γ using the definitions in Defs ∪ NewDefs, derives a new set Φ of clauses, called specialized clauses, which are added to the program P s . The specialized clauses in Φ are derived as follows. Suppose that η: H ← e, L 1 , . . . , L n is a clause in Γ , where for i = 1, . . . , n, L i is of the form either sat(X, ψ i ) or ¬sat(X, ψ i ). For i = 1, . . . , n, if there exists a definition δ i : newp(X) ← d i (X), sat(X, ψ i ) in Defs such that e implies d i (X), then γ is folded using δ i , that is, sat(X, ψ i ) is replaced by newp(X), else a new definition ν i : newp(X) ← g(X), sat(X, ψ i ), such that e implies g(X), is added to NewDefs and γ is folded using ν i . More details on the Generalize&Fold procedure will be given in the next section.

An uncontrolled application of the Generalize&Fold procedure may lead to the introduction of infinitely many new definitions and, therefore, it may determine the non-termination of the Specialize procedure. In order to guarantee termination, we will extend to constraint logic programs some techniques which have been proposed for controlling generalization in positive supercompilation [34] and partial deduction [22,24].

The output program P s of the Specialize procedure is a stratified program and the procedure BottomUp computes the perfect model M s of P s by considering a stratum at a time, starting from the lowest stratum and going up to the highest stratum of P s (see, for instance, [4]). Obviously, the model M s may be infinite and the BottomUp procedure may not terminate. In order to get a terminating procedure, we could compute an approximation of M s by applying some standard techniques which are used in the static analysis of programs [10]. Indeed, in order to prove that prop ∈ M s , we could construct a set A ⊆ M s such that prop ∈ A. Approximations (also called abstractions) are often used for the verification of infinite state systems (see, for instance, [2,5,13,35]). In this paper, however, we will not study these techniques based on approximations and we will focus our attention on the design of the Specialize procedure only. In Section 5 we show that the construction of the model M s terminates in several significant cases.

Example 2. Let us consider the reactive system K of Example 1. We want to check whether or not prop ∈ M (P K ∪ {γ 1 , γ 2 }), where prop expresses the fact that not(eu(true, negative)) holds in every initial state. Now we have that: (i) by using a traditional Prolog system, the evaluation of the query prop does not terminate in the program P K ∪{γ 1 , γ 2 }, because negprop has an infinitely failed SLD tree, (ii) by using the XSB logic programming system which uses tabled resolution, the query prop does not terminate, and (iii) the bottom-up construction of M (P K ∪ {γ 1 , γ 2 }) does not terminate (even if we restrict the program to clauses 1, 2, 5, 6, 11-14, which are the clauses actually needed for evaluating the query prop).

In our verification algorithm we overcome those difficulties encountered by traditional Prolog systems and XSB by applying the Specialize procedure to the program P K ∪ {γ 1 , γ 2 } (with a suitable generalization strategy, as illustrated in the next section). By doing so, we derive the following specialized program P s :

prop

← ¬negprop negprop ← X 1 ≤ 0, X 2 = 0, new 1(X 1 , X 2 ) new 1(X 1 , X 2 ) ← X 1 ≤ 0, X 2 = 0, Y 1 = X 1 , Y 2 = 1, new 2(Y 1 , Y 2 ) new 2(X 1 , X 2 ) ← X 1 ≤ 0, X 2 ≥ 0, Y 1 = X 1 , Y 2 = X 2 + 1, new 2(Y 1 , Y 2 )

The BottomUp procedure computes the perfect model of P s , which is M s = {prop}, in a finite number of steps. Thus, the property not(eu(true, negative)) holds in every initial state of K.

Generalization Strategies

The design of a powerful generalization strategy should meet two conflicting requirements: (i) the strategy should enforce the termination of the Specialize procedure, and (ii) over-generalization may produce a specialized program P s with an infinite perfect model which may cause the non-termination of the Bot-tomUp procedure. In this section we present several generalization strategies for coping with those conflicting requirements. These strategies combine various by now standard techniques used in the fields of program transformation and static analysis, such as well-quasi orderings, widening, and convex hull operators, and variants thereof. All these strategies guarantee the termination of the Specialize procedure. However, as we deal with an undecidable verification problem, the power and effectiveness of the various generalization strategies can only be assessed by an experimental evaluation, which will be presented in the next section.

The Generalize&Fold Procedure

The Generalize&Fold procedure makes use of a tree, called Definition Tree, whose root is labelled by clause γ 2 (recall that {γ 2 } is the initial value of InDefs) and the non-root nodes are labelled by the clauses in Defs. Since, by construction, the clauses in Defs are all distinct, we will identify each clause with a node of that tree. The children of a clause γ in Defs are the clauses NewDefs derived by applying Unfold (γ, Γ ) followed by Generalize&Fold(Defs, Γ, NewDefs, Φ).

Similarly to [22,24,34], our generalization technique is based on the combined use of well-quasi ordering relations and clause generalization operators. The well-quasi orderings guarantee that generalization is eventually applied, while generalization operators guarantee that each definition can be generalized a finite number of times only.

Let C be the set of all constraints and D be a fixed interpretation for the constraints in C. We assume that: (i) every constraint in C is either an atomic constraint or a finite conjunction of constraints (we will denote conjunction by comma), and (ii) C is closed under projection, where the projection of a constraint c w.r.t. the variable X is a constraint, denoted project(c, X), such that D |= ∀(project(c, X) ↔ ∃Xc). We define a partial order on C as follows: for any two constraints c 1 and c 2 in C, we have that

c 1 c 2 iff D |= ∀ (c 1 → c 2 ).

Definition 1 (Well-Quasi Ordering). A well-quasi ordering (wqo, for short) on a set S is a reflexive, transitive, binary relation such that, for every infinite sequence e 0 , e 1 , . . . of elements of S, there exist i and j such that i < j and e i e j . Given e 1 and e 2 in S, we write e 1 ≈ e 2 if e 1 e 2 and e 2 e 1 . We say that a wqo is thin iff for all e ∈ S, the set {e ∈ S | e ≈ e } is finite. Similarly to the widening operator ∇ used in abstract interpretations [10], every infinite sequence of constraints constructed by using the generalization operator eventually stabilizes, that is, for every infinite sequence d 0 , d 1 , . . . of constraints, in the infinite sequence c 0 , c 1 , . . . defined as follows: c 0 = d 0 and for any i ≥ 0, c i+1 = c i d i+1 , there exist 0 ≤ m < n, such that c m = c n . Procedure Generalize&Fold Input: (i) a set Defs of definitions, and (ii) a set Γ of clauses obtained from a clause γ by the Unfold procedure. Output: (i) A set NewDefs of new definitions, and (ii) a set Φ of folded clauses.

NewDefs := ∅ ; Φ := Γ ; while in Φ there exists a clause η: H ← e, G 1 , L, G 2 , where L is either sat(X, ψ) or ¬sat(X, ψ) do Generalize: Let e p (X) be project(e, X). 1. if in Defs there exists a clause δ: newp(X) ← d(X), sat(X, ψ) such that e p (X) d(X) (modulo variable renaming) then NewDefs := NewDefs 2. elseif there exists a clause α in Defs such that:

(i) α is of the form newq(X) ← b(X), sat(X, ψ), and (ii) α is the most recent ancestor of γ in the Definition Tree such that b(X) e p (X) then NewDefs := NewDefs ∪ {newp(X) ← b(X) e p (X), sat(X, ψ)} 3. else NewDefs := NewDefs ∪ {newp(X) ← e p (X), sat(X, ψ)}

Fold: Φ := (Φ − {η}) ∪ {H ← e, G 1 , M, G 2 }, where M is newp(X), if L is sat(X, ψ),

and

M is ¬newp(X), if L is ¬sat(X, ψ) end-while

The following theorem, whose proof is given in [16], establishes that the Specialize procedure, which uses the Unfold and the Generalize&Fold subprocedures, always terminates and preserves the perfect model semantics.

Theorem 2 (Termination and Correctness of the Specialize Procedure). For every input program P K ∪{γ 1 , γ 2 }, for every thin wqo , for every generalization operator , the Specialize procedure terminates. If P s is the output program of the Specialize procedure, then prop ∈ M (P K ) iff prop ∈ M (P s ).

Well-Quasi Orderings and Generalization Operators on Linear

Constraints In this section we describe the wqo's and the generalization operators we have used in our verification experiments.

We will consider the set Lin k of constraints defined as follows. The atomic constraints of Lin k are linear inequations constructed by using the predicate symbols < and ≤, the k distinct variables X 1 , . . . , X k , and the integer coefficients q i 's. The constraints in Lin k are interpreted over the rationals in the usual way. Every constraint c ∈ Lin k is the conjunction a 1 , . . . , a m of m (≥ 0) distinct atomic constraints and, for i = 1, . . . , m, (1) a i is of the form either p i ≤ 0 or p i < 0, and (2) p i is a polynomial of the form q 0 + q 1 X 1 + . . . q k X k , where the q i 's are integer coefficients. An equation r = s is considered as an abbreviation of the conjunction of the two inequations r ≤ s and s ≤ r.

In every infinite state system we will consider, the state is represented as an n-tuple t 1 , . . . , t n , where k terms, with k ≤ n, are rationals and the remaining n−k terms are elements of a finite domain. As illustrated in Section 2, the initial states and the elementary properties are specified by constraints in Lin k and the transition relation is specified by constraints in Lin 2k . (The n−k components of a state which are elements of a finite domain, are specified by their values.)

Well-Quasi Orderings. Now we present three wqo's between the polynomials and between the constraints on Lin k that we will use in the verification examples of the next section.

(1) The wqo HomeoCoeff, denoted by HC , compares sequences of absolute values of integer coefficients occurring in polynomials. The HC ordering is based on the notion of a homeomorphic embedding (see, for instance, [22,24,34]) and takes into account commutativity and associativity of addition and conjunction. Given two polynomials with integer coefficients p 1 = def q 0 + q 1 X 1 + . . . + q k X k , and p 2 = def r 0 + r 1 X 1 + . . . + r k X k , we have that p 1 HC p 2 iff there exist a permutation 0 , . . . , k of the indexes 0, . . . , k such that, for i = 0, . . . , k, |q i | ≤ |r i |. Given two atomic constraints a 1 = def p 1 < 0 and a 2 = def p 2 < 0, we have that a 1 HC a 2 iff p 1 HC p 2 . Similarly, if we consider a 1 = def p 1 ≤ 0 and a 2 = def p 2 ≤ 0. Given two constraints c 1 = def a 1 , . . . , a m , and c 2 = def b 1 , . . . , b n , we have that c 1 HC c 2 iff there exist m distinct indexes 1 , . . . , m , with m ≤ n, such that a i HC b i , for i = 1, . . . , m.

(2) The wqo MaxCoeff, denoted by MC , compares the maximum absolute value of coefficients occurring in polynomials. For any atomic constraint a i of the form p < 0 or p ≤ 0, where p is q 0 + q 1 X 1 + . . . + q k X k , we have that maxcoeff (a i ) = max {|q 0 |, |q 1 |, . . . , |q k |}, and for any two atomic constraints a 1 , a 2 , we have that a 1 MC a 2 iff maxcoeff (a 1 ) ≤ maxcoeff (a 2 ). Given two constraints c 1 = def a 1 , . . . , a m , and c 2 = def b 1 , . . . , b n , we have that c 1 MC c 2 iff, for i = 1, . . . , m, there exists j ∈ {1, . . . , n} such that a i MC b j .

(3) The wqo SumCoeff, denoted by SC , compares the sum of the absolute values of the coefficients occurring in polynomials. For any atomic constraint a i of the form p < 0 or p ≤ 0, where p is q 0 +q 1 X 1 +. . .+q k X k , , we define sumcoeff (a i ) = It can be shown that WP is, indeed, a generalization operator w.r.t. the wqo's MaxCoeff, and SumCoeff. However, in general, WP is not a generalization operator w.r.t. HomeoCoeff, because the constraint c WP d may contain more atomic constraints than c and, thus, it may not be the case that (c WP d) HC c.

Some additional generalization operators can be defined by combining our three operators T , W , and WP , with the convex hull operator, which is often used in the static analysis of programs [10]. Given two constraints c and d, their convex hull, denoted by ch(c, d), is the least constraint h (w.r.t. the ordering) such that c h and d h.

Given any two constraints c and d, a wqo , and a generalization operator , we define the generalization operator CH as follows:

c CH d = def c ch(c, d).

From the definitions of and ch one can easily derive that the operator CH is indeed a generalization operator for c and d, that is, (i) d c CH d, and (ii) c CH d c. (G4) Given any two constraints c and d, we define the generalization operator CHWiden, denoted CHW , as follows: c CHW d = def c W ch(c, d ). (G5) Given any two constraints c and d, we define the generalization operator CHWidenPlus, denoted CHWP , as follows:

c CHWP d = def c WP ch(c, d ).

Note that if we combine the generalization operator Top and the convex hull operator, we get the Top operator again.

Experimental Evaluation

In this section we report the results of the experiments we have performed on several examples of verification of infinite state reactive systems.

We have implemented the verification algorithm presented in Section 2 by using MAP [26], an experimental system for the transformation of constraint logic programs. The MAP system is implemented in SICStus Prolog 3.12.8 and uses the clpq library to operate on constraints. Now we give a brief description of the experiments we have conducted (see also Tables 1 and 2).

We have considered the following mutual exclusion protocols. (i) Bakery [20]: we have verified safety (that is, mutual exclusion) and liveness (that is, starvation freedom) in the case of two processes, and safety in the case of three processes; (ii) MutAst [21]: we have verified safety in the case of two processes; (iii) Peterson [29]: we have considered a counting abstraction [11] of this protocol and we have verified safety in the case of N processes; and (iv) Ticket [3]: we have considered the case of two processes and we have verified safety and liveness.

We have also verified safety properties of the following cache coherence protocols: (v) Berkeley RISC, (vi) DEC Firefly, (vii) IEEE Futurebus+, (viii) Illinois University, (ix) MESI, (x) MOESI, (xi) Synapse N+1, and (xii) Xerox PARC Dragon. These protocols are used in shared-memory multiprocessing systems for guaranteeing data consistency of the local cache associated with every processor [18]. We have considered parameterized versions of the above protocols, that is, protocols designed for an arbitrary number of processors. Similarly to [11], we have applied our verification method to counting abstractions of the protocols.

We have also verified safety properties of the following systems. (xiii) Barber [6]: we have considered a parameterized version of this protocol with a single barber process and an arbitrary number of customer processes; (xiv) Bounded and Unbounded Buffer : we have considered protocols for two producers and two consumers which communicate via a bounded and an unbounded buffer, respectively (the encodings of these protocols are taken from [13]); (xv) CSM, which is a central server model described in [12]; (xvi) Insertion Sort and Selection Sort: we have considered the problem of checking array bounds of these two sorting algorithms, parameterized w.r.t. the size of the array, as presented in [13]; (xvii) Office Light Control [7], which is a protocol for controlling how office lights are switched on or off, depending on room occupancy; (xviii) Reset Petri Nets, which are Petri Nets augmented with reset arcs: we have considered a reachability problem for a net which is a variant of one presented in [23] (unlike [23], in the net we have considered there is no bound on the number of tokens that can reside in a place and, therefore, our net is an infinite state system).

Table 1 shows the results of running the MAP system on the above examples by choosing different combinations of a wqo W and a generalization operator G introduced in Section 4. In the sequel we will denote that combination by W &G. The combinations MaxCoeff &CHWiden, MaxCoeff &CHWidenPlus, MaxCoeff &Top, and MaxCoeff &Widen have been omitted because they give results which are very similar to those obtained by using SumCoeff, instead of MaxCoeff. HomeoCoeff &CHWidenPlus and HomeoCoeff &WidenPlus have been omitted because, as already mentioned in Section 4, these combinations do not satisfy the conditions given in Definition 2, and thus, they do not guarantee the termination of the specialization strategy.

If we consider precision, that is, the number of properties which have been proved, the best combination is SumCoeff &WidenPlus (23 properties proved out of 23) closely followed by MaxCoeff &WidenPlus and SumCoeff &CHWidenPlus (22 properties proved out of 23). The verification times for SumCoeff &CHWiden-Plus are definitely worse than the ones for the other two combinations: indeed, on average, for each proved property, SumCoeff &CHWidenPlus takes 2990 milliseconds, while MaxCoeff &WidenPlus and SumCoeff &WidenPlus take 730 milliseconds and 820 milliseconds, respectively. This is due to the fact that SumCoeff & CHWidenPlus introduces more definitions than the other two strategies. (For lack of space, we do not report average times for the other generalization strategies, nor we present statistics on the number of generated definitions.) Table 1 also shows that by using the Top and the Widen generalization operators the specialization time is quite good, but the precision of verification is low. In other terms, the Top and Widen operators determine an over-generalization. In contrast, SumCoeff &WidenPlus and MaxCoeff &WidenPlus ensure a good balance between time and precision.

In conclusion, the specialization strategy which uses the generalization strategy SumCoeff &WidenPlus outperforms the others, closely followed by the specialization strategy which uses MaxCoeff &WidenPlus. In particular, the generalization strategies based either on the homeomorphic embedding (that is, Homeo-Coeff ) or the combination of the widening and convex hull operators (that is, Widen and CHWiden) are not the best choices in our examples.

In order to compare our MAP implementation of the verification method with other constraint-based model checking tools for infinite state systems, we have run the verification examples described above on the following systems: (i) ALV [7], which combines BDD-based symbolic manipulation for boolean and enumerated types, with a solver for linear constraints on integers, (ii) DMC [13], which computes (approximated) least and greatest models of CLP(R) programs, and (iii) HyTech [19], a model checker for hybrid systems.

Table 2 reports the results of our experiments obtained by using various options available in those verification systems. All experiments with MAP, ALV, DMC, and HyTech have been conducted on an Intel Core 2 Duo E7300 2.66GHz under the Linux operating system.

In terms of precision, MAP with the SumCoeff &WidenPlus option is the best system (23 properties proved out of 23), followed by DMC with the A option (19 out of 23), ALV with the default option (18 out of 23), and, finally, HyTech with the Bw option (17 out of 23). Among the above mentioned systems and respective options, HyTech (Bw) has the best average running time (70 milliseconds per proved property), followed by MAP and DMC (both 820 milliseconds), and ALV (8480 milliseconds). This is explained by the fact that the HyTech with the Bw option tries to prove a safety property with a very simple strategy, by constructing the reachability set backwards from the property to be proved, while the other systems apply more sophisticated techniques. Note also that the average verification times are affected by an uneven behavior on some specific examples. For instance, in the Bounded and Unbounded Buffer examples the

Conclusions

In this paper we have proposed some improvements of the method presented in [15] for verifying infinite state reactive systems. First, we have reformulated the verification method as a two-phase method: (1) in the first phase a CLP specification of the reactive system is specialized w.r.t. the initial state and the temporal property to be verified and (2) in the second phase the perfect model of the specialized program is constructed in a bottom-up way. For Phase (1) we have considered various specialization strategies which employ different wellquasi orderings and generalization operators to guarantee always terminating transformations. These orderings and generalization operators are either new or adapted from similar notions, such as, convex hull, widening, and homeomorphic embedding, defined in the context of static analysis of programs [10] and program specialization [22,24,34].

We have applied these specialization strategies to several examples of infinite state systems taken from the literature and we have compared the results in terms of efficiency and precision (that is, the number of proved properties). On the basis of our experimental results we have found some strategies that outperform the others in terms of a good balance of efficiency and precision. In particular, the strategies based on the convex hull, widening, and homeomorphic embedding, do not appear to be the best strategies in our examples.

Then, we have applied other model checking tools for infinite state systems (in particular, ALV [7], DMC [13], and HyTech [19]) to the same set of examples. The experimental results show that the specialization-based verification system (with the best performing strategies) is competitive with respect to the other tools.

Our approach is closely related to other verification methods for infinite state systems based on the specialization of (constraint) logic programs [23,25,28]. Unlike the approach proposed in [23,25] we use constraints, which give us very powerful means of dealing with infinite sets of states. The specialization-based verification method presented in [28] consists of one phase only incorporating both top-down query directed specialization and bottom-up answer propagation. This method is restricted to definite constraint logic programs and makes use of a generalization technique which combines widening and convex hull computations for ensuring termination. In [28] only two examples have been presented (the Bakery protocol and a Petri net) and no verification times are reported. Thus, it is hard to make a comparison in terms of effectiveness with respect to the method we have presented here. However, as already mentioned, the generalization techniques based on the widening and the convex hull operators do not turn out to be the best options in our examples.

Another approach based on program transformation for verifying parameterized (and, hence, infinite state) systems has been presented in [32]. This approach is based on unfold/fold transformations which are more general than the ones used in the specialization strategy considered in this paper. However, the strategy for guiding the unfold/fold rules proposed in [32] works in fully automatic mode in a small set of examples only.

Finally, we would like to mention that our verification method can be viewed as complementary with respect to the methods based on static analysis, such as [5,13]. These methods work by constructing approximations of program models (which can be least or greatest models, depending on the specific technique) in a bottom-up way. However, these methods may fail to prove a property simply because they compute a subset (or a superset) of the program model.

One further enhancement of our method could be achieved by replacing the bottom-up, precise computation of the perfect model performed in our Phase (2) by an approximated computation, in the style of [5,13]. Finding the optimal combination, in terms of both efficiency and precision, of program specialization and static analysis techniques for the verification of infinite state systems is an interesting direction for future research.