Generalization Strategies for the Veri cation of In nite State Systems

Abstract

We present a comparative evaluation of some generalization strategies which are applied by a method for the automated veri cation of in nite state reactive systems. The veri cation method is based on (1) the specialization of the constraint logic program which encodes the system with respect to the initial state and the property to be veri ed, and (2) a bottom-up evaluation of the specialized program. The generalization strategies are used during the program specialization phase for controlling when and how to perform generalization. Selecting a good generalization strategy is not a trivial task because it must guarantee the termination of the specialization phase itself, and it should be a good balance between precision and performance. Indeed, a coarse generalization strategy may prevent one to prove the properties of interest, while an unnecessarily precise strategy may lead to high veri cation times. We perform an experimental evaluation of various generalization strategies on several in nite state systems and properties to be veri ed.

-

One of the most challenging problems in the veri cation of reactive systems, is the extension of the model checking technique (see [ 9 ] for a thorough overview) to in nite state systems. In model checking the evolution over time of an in nite state system is modelled as a binary transition relation over an in nite set of states (such as n-tuples of integers or rationals) and the properties of that evolution are speci ed 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 in nite state systems, the veri cation 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 identi ed (see, for instance, [ 1,14 ]). Other approaches enhance nite 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 in nite state system to a nite 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 xpoint semantics of logic programming languages allows us to easily represent the xpoint semantics of various temporal logics [ 13,27,31 ]. Moreover, constraints over the integers or the rationals can be used for providing nite representations of in nite sets of states [ 13,17 ].

However, for programs which specify in nite 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 in nitely failed derivations. For this reason, instead of using direct program evaluation, many logic programmingbased veri cation 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 veri cation method presented in [ 15 ] and we assess its practical value. That method is applicable to speci cations of CTL properties of in nite state systems encoded as constraint logic programs and it makes use of program specialization.

The speci c contributions of this paper are the following. First, we have reformulated the specialization-based veri cation method of [ 15 ] as a two-phase method. Phase (1): the CLP speci cation is specialized w.r.t. the initial state of the system and the temporal property to be veri ed, 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 veri cation technique.

Then, we have de ned various generalization strategies which can be used during Phase (1) of our veri cation 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 nite 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 veri cation times which are too high. The generalization strategies we consider in this paper have been speci cally 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 in nite state systems and properties taken from the literature. We have performed a comparative evaluation of generalization strategies in terms of e ciency and power, based on the analysis of the experimental results.

Finally, we have compared our MAP implementation with various constraintbased model checkers for in nite 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 in nite state systems can be encoded by using locally strati ed CLP programs. In Section 3 we present our two-phase method for veri cation. In Section 4 we describe various strategies that can be applied during the specialization phase. These strategies di er 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 veri cation systems. 2

Specifying CTL Properties by CLP Programs

We will model an in nite state system as a Kripke structure and we will represent a property to be veri ed 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 j= '. (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 ht1; : : : ; tni, where for i = 1; : : : ; n, the term ti is either a rational number or an element of a nite 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 hX1; : : : ; Xni. (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 de ne a predicate ts such that, for every state X, ts(X; Ys) holds i 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 i t(X; Y ) holds. We refer to [ 16 ] for conditions that guarantee that Ys is a nite list and for an algorithm to construct the clauses de ning ts from the clauses de ning 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 de ning the predicates initial , t, ts, and elem, the satisfaction relation j= can be encoded by a predicate sat de ned 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 (F1; F2)) sat (X; F1); sat (X; F2) 4. sat (X; ex (F )) t(X; Y ); sat (Y; F ) 5. sat (X; eu(F1; F2)) sat (X; F2) 6. sat (X; eu(F1; F2)) sat (X; F1); t(X; Y ); sat (Y; eu(F1; F2)) 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 ([XjXs]; F ) sat (X; F ); sat all (Xs; F ) Let PK denote the constraint logic program consisting of clauses 1{10 together with the clauses de ning the predicates initial , t, ts, and elem.

Now we will present a method for proving that a given CTL formula ' holds. We start by de ning a new predicate prop as follows:

prop def 8X(initial (X) ! sat (X; ')) This de nition 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 PK [ f 1; 2g is locally strati ed and, hence, it has a unique perfect model M (PK [ f 1; 2g) [ 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 2 I, K; s j= ') i prop 2 M (PK [ f 1; 2g).

Example 1. Let us consider the reactive system depicted in Figure 1, where a term of the form s(X1; X2) denotes the pair hX1; X2i of rationals.

X2 := X2 1 ''W s(X1;X2) $$

X2 := X2 +1 X1 &1 & %

X1 %2

Suppose that we want to verify the following property: in every initial state s(X1; X2), where X1 0 and X2 = 0, the CTL formula not (eu(true; negative)) holds, that is, from any initial state it is impossible to reach a state s(X10; X20) where X20 < 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 X1 0; X2 = 0; sat (s(X1; X2); 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 2 M (PK [

One of the most important features of the model checking techniques for nite state systems is the ability to nd 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 ]. 3

Verifying In nite State Systems by Specializing CLP

Programs

In this section we present a method for checking whether or not prop 2 M (PK [ f 1; 2g), where PK [ f 1; 2g is a CLP speci cation of an in nite state system and prop is a predicate encoding the satis ability of a given CTL formula, as indicated in Section 2.

The checking technique based on the bottom-up construction of the perfect model M (PK [ f 1; 2g) is not feasible, in general, because this model may be in nite. 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 2 M (PK [ f 1; 2g). This is due to the limited ability of these proof procedures to cope with in nite failure.

It has been shown in [ 15 ] that program specialization often improves the treatment of in nite failure. In this section we present a reformulation of the method proposed in [ 15 ] by de ning a veri cation algorithm working in two phases: (1) in the rst phase we specialize the program PK [ f 1; 2g w.r.t. the query prop, that is, w.r.t. initial state of the system and the temporal property to be veri ed, 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 e ect of program specialization on the veri cation 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 PK [ f 1; 2g 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 modi es the initial program PK [ f 1; 2g by incorporating into the specialized program Ps the knowledge about the constraints that hold in the initial states. Therefore, the bottom-up construction of the perfect model of Ps may exploit those constraints and terminate more often than the bottom-up construction of the perfect model of the initial program PK [ f 1; 2g. The Veri cation Algorithm Input : The program PK [ f 1; 2g.

Output : An Herbrand interpretation Ms such that prop 2 M (PK [ f 1; 2g) i prop 2 Ms . (Phase 1) Specialize(PK [ f 1; 2g; Ps ); (Phase 2) BottomUp(Ps ; Ms )

The Specialize procedure of Phase (1) implements a program specialization strategy which makes use of the following transformation rules only: de nition introduction, constrained atomic folding, positive unfolding, constrained atomic folding, removal of clauses with unsatis able 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 program PK [ f 1; 2g.

Output : A strati ed program Ps such that prop 2 M (PK [ f 1; 2g) i prop 2 M (Ps).

Ps := f 1g; InDefs := f 2g; Defs := fg; while there exists a clause in InDefs do Unfold ( ; );

Generalize&Fold(Defs; ; NewDefs; ); Ps := Ps [ ;

InDefs := (InDefs f g) [ NewDefs; end-while Defs := Defs [ NewDefs; The Unfold procedure takes as input a clause 2 InDefs of the form H c(X); sat (X; ), and returns as output a set of clauses derived from as follows. The Unfold procedure rst 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(s1; s2), (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 simpli ed by removing: (i) every clause whose body contains an unsatis able 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 de ning the predicates t, ts, sat, and sat all , the Unfold procedure terminates for any ground term denoting a CTL formula occurring in .

The Generalize&Fold procedure takes as input the set of clauses produced by the Unfold procedure and the set Defs of clauses, called de nitions. A de nition 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 de nitions (which are then added to Defs) and, by folding the clauses in using the de nitions in Defs [ NewDefs, derives a new set of clauses, called specialized clauses, which are added to the program Ps. The specialized clauses in are derived as follows. Suppose that : H e; L1; : : : ; Ln is a clause in , where for i = 1; : : : ; n; Li is of the form either sat (X; i) or :sat (X; i). For i = 1; : : : ; n, if there exists a de nition i: newp(X) di(X); sat (X; i) in Defs such that e implies di(X), then is folded using i, that is, sat (X; i) is replaced by newp(X), else a new de nition 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 in nitely many new de nitions 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 Ps of the Specialize procedure is a strati ed program and the procedure BottomUp computes the perfect model Ms of Ps by considering a stratum at a time, starting from the lowest stratum and going up to the highest stratum of Ps (see, for instance, [ 4 ]). Obviously, the model Ms may be in nite and the BottomUp procedure may not terminate. In order to get a terminating procedure, we could compute an approximation of Ms by applying some standard techniques which are used in the static analysis of programs [ 10 ]. Indeed, in order to prove that prop 2 Ms, we could construct a set A Ms such that prop 2 A. Approximations (also called abstractions) are often used for the veri cation of in nite 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 Ms terminates in several signi cant cases. Example 2. Let us consider the reactive system K of Example 1. We want to check whether or not prop 2 M (PK [ f 1; 2g), 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 PK [f 1; 2g, because negprop has an in nitely 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 (PK [ f 1; 2g) 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 veri cation algorithm we overcome those di culties encountered by traditional Prolog systems and XSB by applying the Specialize procedure to the program PK [ f 1; 2g (with a suitable generalization strategy, as illustrated in the next section). By doing so, we derive the following specialized program Ps: prop :negprop negprop X1 0; X2 = 0; new 1(X1; X2) new 1(X1; X2) X1 0; X2 = 0; Y1 = X1; Y2 = 1; new 2(Y1; Y2) new 2(X1; X2) X1 0; X2 0; Y1 = X1; Y2 = X2 + 1; new 2(Y1; Y2) The BottomUp procedure computes the perfect model of Ps, which is Ms = fpropg, in a nite number of steps. Thus, the property not (eu(true; negative)) holds in every initial state of K. 4

Generalization Strategies

The design of a powerful generalization strategy should meet two con icting requirements: (i) the strategy should enforce the termination of the Specialize procedure, and (ii) over-generalization may produce a specialized program Ps with an in nite perfect model which may cause the non-termination of the BottomUp procedure. In this section we present several generalization strategies for coping with those con icting requirements. These strategies combine various by now standard techniques used in the elds 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 veri cation problem, the power and e ectiveness 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 makes use of a tree, called De nition Tree, whose root is labelled by clause 2 (recall that f 2g 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 de nition can be generalized a nite number of times only.

Let C be the set of all constraints and D be a xed interpretation for the constraints in C. We assume that: (i) every constraint in C is either an atomic constraint or a nite 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 j= 8(project (c; X) $ 9Xc). We de ne a partial order v on C as follows: for any two constraints c1 and c2 in C, we have that c1 v c2 i D j= 8 (c1 ! c2). De nition 1 (Well-Quasi Ordering). A well-quasi ordering (wqo, for short) on a set S is a re exive, transitive, binary relation - such that, for every in nite sequence e0; e1; : : : of elements of S, there exist i and j such that i < j and ei - ej . Given e1 and e2 in S, we write e1 e2 if e1 - e2 and e2 - e1. We say that a wqo - is thin i for all e 2 S, the set fe0 2 S j e e0g is nite. De nition 2 (Generalization Operator). Let - be a wqo on C. A generalization operator on C w.r.t. the wqo -, is a binary operator such that, for all constraints c and d in C, we have: (i) d v c d, and (ii) c d - c. (Note that, in general, is not commutative.)

Similarly to the widening operator r used in abstract interpretations [ 10 ], every in nite sequence of constraints constructed by using the generalization operator eventually stabilizes, that is, for every in nite sequence d0; d1; : : : of constraints, in the in nite sequence c0; c1; : : : de ned as follows: c0 = d0 and for any i 0, ci+1 = ci di+1, there exist 0 m < n, such that cm = cn.

Procedure Generalize&Fold

Input : (i) a set Defs of de nitions, and (ii) a set clause by the Unfold procedure.

Output : (i) A set NewDefs of new de nitions, and (ii) a set of clauses obtained from a of folded clauses.

NewDefs := ; ; := ; while in there exists a clause : H or :sat (X; ) do Generalize: Let ep(X) be project (e; X). 1. if in Defs there exists a clause : newp(X)

ep(X) v 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 De nition Tree such that b(X) - ep(X) then NewDefs := NewDefs [ fnewp(X) b(X) ep(X); sat (X; )g 3. else NewDefs := NewDefs [ fnewp(X) ep(X); sat (X; )g Fold: := (

f g) [ fH e; G1; M; G2g, where M is newp(X), if L is sat (X; ), and M is :newp(X), if L is :sat (X; ) end-while e; G1; L; G2, where L is either sat (X; ) d(X); sat (X; ) such that

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 PK [f 1; 2g, for every thin wqo -, for every generalization operator , the Specialize procedure terminates. If Ps is the output program of the Specialize procedure, then prop 2 M (PK) i prop 2 M (Ps). 4.2 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 veri cation experiments.

We will consider the set Link of constraints de ned as follows. The atomic constraints of Link are linear inequations constructed by using the predicate symbols < and , the k distinct variables X1; : : : ; Xk, and the integer coefcients qi's. The constraints in Link are interpreted over the rationals in the usual way. Every constraint c 2 Link is the conjunction a1; : : : ; am of m ( 0) distinct atomic constraints and, for i = 1; : : : ; m, (1) ai is of the form either pi 0 or pi < 0, and (2) pi is a polynomial of the form q0 + q1X1 + : : : qkXk, where the qi's are integer coe cients. An equation r = s is considered as an abbreviation of the conjunction of the two inequations r s and s r.

In every in nite state system we will consider, the state is represented as an n-tuple ht1; : : : ; tni, where k terms, with k n, are rationals and the remaining n k terms are elements of a nite domain. As illustrated in Section 2, the initial states and the elementary properties are speci ed by constraints in Link and the transition relation is speci ed by constraints in Lin2k. (The n k components of a state which are elements of a nite domain, are speci ed by their values.) Well-Quasi Orderings. Now we present three wqo's between the polynomials and between the constraints on Link that we will use in the veri cation examples of the next section. (1) The wqo HomeoCoe , denoted by -HC , compares sequences of absolute values of integer coe cients 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 coe cients p1 =def q0 + q1X1 + : : : + qkXk, and p2 =def r0 + r1X1 + : : : + rkXk, we have that p1 -HC p2 i there exist a permutation h`0; : : : ; `ki of the indexes h0; : : : ; ki such that, for i = 0; : : : ; k; jqij jr`i j. Given two atomic constraints a1 =def p1 < 0 and a2 =def p2 < 0, we have that a1 -HC a2 i p1 -HC p2. Similarly, if we consider a1 =def p1 0 and a2 =def p2 0. Given two constraints c1 =def a1; : : : ; am; and c2 =def b1; : : : ; bn; we have that c1 -HC c2 i there exist m distinct indexes `1; : : : ; `m, with m n, such that ai -HC b`i , for i = 1; : : : ; m. (2) The wqo MaxCoe , denoted by -MC , compares the maximum absolute value of coe cients occurring in polynomials. For any atomic constraint ai of the form p < 0 or p 0, where p is q0 + q1X1 + : : : + qkXk, we have that maxcoe (ai) = max fjq0j; jq1j; : : : ; jqkjg, and for any two atomic constraints a1, a2, we have that a1 -MC a2 i maxcoe (a1) maxcoe (a2). Given two constraints c1 =def a1; : : : ; am; and c2 =def b1; : : : ; bn; we have that c1 -MC c2 i , for i = 1; : : : ; m, there exists j 2 f1; : : : ; ng such that ai -MC bj . (3) The wqo SumCoe , denoted by -SC , compares the sum of the absolute values of the coe cients occurring in polynomials. For any atomic constraint ai of the form p < 0 or p 0, where p is q0 +q1X1 +: : : +qkXk, , we de ne sumcoe (ai) = Pk j=0 jqj j, and for any two atomic constraints a1, a2, we de ne a1 -SC a2 i sumcoe (a1) sumcoe (a2). Given two constraints c1 =def a1; : : : ; am; and c2 =def b1; : : : ; bn; we de ne c1 -SC c2 i , for i = 1; : : : ; m, there exists j 2 f1; : : : ; ng such that ai -SC bj .

Generalization Operators. Now we present some generalization operators on Link which we use in the veri cation examples of the next section. (G1) Given any two constraints c and d, the generalization operator Top, denoted T , returns true. It can be shown that T is indeed a generalization operator w.r.t. the wqo's HomeoCoe , MaxCoe , and SumCoe . (G2) Given any two constraints c =def a1; : : : ; am, and d, the generalization operator Widen, denoted W , returns the conjunction ai1; : : : ; air; where fai1; : : : ; airg = fah j 1 h m and d v ahg (see [ 10 ] for a similar operator for static program analysis). It can be shown that W is, indeed, a generalization operator w.r.t. the wqo's HomeoCoe , MaxCoe , and SumCoe . (G3) Given any two constraints c =def a1; : : : ; am, and d =def b1; : : : ; bn, the generalization operator WidenPlus, denoted WP , returns the conjunction ai1; : : : ; air; bj1; : : : ; bjs, where: (i) fai1; : : : ; airg = fah j 1 h m and d v ahg, and (ii) fbj1; : : : ; bjsg = fbk j 1 k n and bk - cg. It can be shown that WP is, indeed, a generalization operator w.r.t. the wqo's MaxCoe , and SumCoe . However, in general, WP is not a generalization operator w.r.t. HomeoCoe , 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 de ned 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 v ordering) such that c v h and d v h.

Given any two constraints c and d, a wqo -, and a generalization operator , we de ne the generalization operator CH as follows: c CH d =def c ch(c; d). From the de nitions of and ch one can easily derive that the operator CH is indeed a generalization operator for c and d, that is, (i) d v c CH d, and (ii) c CH d - c. (G4) Given any two constraints c and d, we de ne 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 de ne 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. 5

Experimental Evaluation

In this section we report the results of the experiments we have performed on several examples of veri cation of in nite state reactive systems.

We have implemented the veri cation 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 veri ed 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 veri ed safety in the case of two processes; (iii) Peterson [ 29 ]: we have considered a counting abstraction [ 11 ] of this protocol and we have veri ed safety in the case of N processes; and (iv) Ticket [ 3 ]: we have considered the case of two processes and we have veri ed safety and liveness.

We have also veri ed safety properties of the following cache coherence protocols: (v) Berkeley RISC, (vi) DEC Fire y, (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 veri cation method to counting abstractions of the protocols.

We have also veri ed 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 Bu er : we have considered protocols for two producers and two consumers which communicate via a bounded and an unbounded bu er, 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) O ce Light Control [ 7 ], which is a protocol for controlling how o ce lights are switched on or o , 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 in nite state system).

Table 1 shows the results of running the MAP system on the above examples by choosing di erent 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 MaxCoe &CHWiden, MaxCoe &CHWidenPlus, MaxCoe &Top, and MaxCoe &Widen have been omitted because they give results which are very similar to those obtained by using SumCoe , instead of MaxCoe . HomeoCoe &CHWidenPlus and HomeoCoe &WidenPlus have been omitted because, as already mentioned in Section 4, these combinations do not satisfy the conditions given in De nition 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 SumCoe &WidenPlus (23 properties proved out of 23) closely followed by MaxCoe &WidenPlus and SumCoe &CHWidenPlus (22 properties proved out of 23). The veri cation times for SumCoe &CHWidenPlus are de nitely worse than the ones for the other two combinations: indeed, on average, for each proved property, SumCoe &CHWidenPlus takes 2990 milliseconds, while MaxCoe &WidenPlus and SumCoe &WidenPlus take 730 milliseconds and 820 milliseconds, respectively. This is due to the fact that SumCoe & CHWidenPlus introduces more de nitions 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 de nitions.) Table 1 also shows that by using the Top and the Widen generalization operators the specialization time is quite good, but the precision of veri cation is low. In other terms, the Top and Widen operators determine an over-generalization. In contrast, SumCoe &WidenPlus and MaxCoe &WidenPlus ensure a good balance between time and precision.

In conclusion, the specialization strategy which uses the generalization strategy SumCoe &WidenPlus outperforms the others, closely followed by the specialization strategy which uses MaxCoe &WidenPlus. In particular, the generalization strategies based either on the homeomorphic embedding (that is, HomeoCoe ) 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 veri cation method with other constraint-based model checking tools for in nite state systems, we have run the veri cation 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 veri cation 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 SumCoe &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, nally, 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 veri cation times are a ected by an uneven behavior on some speci c examples. For instance, in the Bounded and Unbounded Bu er examples the Bakery 2 (safety) Bakery 2 (liveness) Bakery 3 (safety) MutAst Peterson N Ticket (safety) Ticket (liveness) Berkeley RISC DEC Fire y IEEE Futurebus+ Illinois University MESI 100

80 MOESI 980

950 Synapse N+1 30

20 Xerox PARC Dragon 1230

1180 Barber Bounded Bu er Unbounded Bu er CSM Insertion Sort Selection Sort O ce Light Control Reset Petri Nets MAP system has higher veri cation times with respect to the other systems, because these examples can be easily veri ed by backward reachability, thereby making the MAP specialization phase redundant. On the opposite side, MAP is much more e cient than the other systems in the Peterson and CSM examples, where the specialization phase de nitely pays o . 6

Conclusions

In this paper we have proposed some improvements of the method presented in [ 15 ] for verifying in nite state reactive systems. First, we have reformulated the veri cation method as a two-phase method: (1) in the rst phase a CLP speci cation of the reactive system is specialized w.r.t. the initial state and the temporal property to be veri ed 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 di erent 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, de ned 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 in nite state systems taken from the literature and we have compared the results in terms of e ciency 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 e ciency 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 in nite 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 veri cation system (with the best performing strategies) is competitive with respect to the other tools.

Our approach is closely related to other veri cation methods for in nite 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 in nite sets of states. The specialization-based veri cation 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 de nite 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 veri cation times are reported. Thus, it is hard to make a comparison in terms of e ectiveness 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. EXAMPLE Bakery 2 (safety) Bakery 2 (liveness) Bakery 3 (safety) MutAst Peterson N Ticket (safety) Ticket (livenes) Berkeley RISC DEC Fire y IEEE Futurebus+ Illinois University MESI MOESI Synapse N+1 Xerox PARC Dragon Barber Bounded Bu er Unbonded Bu er CSM Insertion Sort Selection Sort O ce Light Control Reset Petri Nets

MAP ALV SC &WidenPlus default A

DMC HyTech

F L noAbs Abs Fw Bw

Another approach based on program transformation for verifying parameterized (and, hence, in nite 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 veri cation 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 speci c 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 e ciency and precision, of program specialization and static analysis techniques for the veri cation of in nite state systems is an interesting direction for future research. A Kripke structure [ 9 ] is a 4-tuple hS; I; R; Li, where: (1) S is a set of states, (2) I S is a set of initial states, (3) R S S is a transition relation from states to states, and (4) L: S ! P(Elem) is a labeling function that assigns to each state s 2 S a subset L(s) of Elem; that is, a set of elementary properties that hold in s. In particular, there exist the elementary properties true, false, and initial and we have that, for all s 2 S, (i) true 2 L(s), (ii) false 62 L(s), and (iii) initial 2 L(s) i s 2 I. We assume that R is a total relation, that is, for every state s 2 S there exists at least one state s0 2 S, called a successor state of s, such that s R s0.

A computation path in a Kripke structure K is an in nite sequence of states s0 s1 : : : such that si R si+1 for every i 0.

The Computation Tree Logic (CTL, for short) [ 9 ] is a propositional temporal logic interpreted over a given Kripke structure. A CTL formula ' has the following syntax:

' ::= e j not (') j and ('1; '2) j ex (') j eu('1; '2) j af (') where e belongs to the set Elem of the elementary properties. Note that the set fex ; eu; af g of operators is su cient to express all CTL properties, because the other CTL operators introduced in [ 9 ] can be de ned in terms of ex ; eu, and af . In particular, the operator ef is de ned as eu(true; ').

The operators ex ; eu, and af have the following semantics. The property ex (') holds in a state s if there exists a successor s0 of s such that ' holds in s0. The property eu('1; '2) holds in a state s if there exists a computation path starting from s such that '1 holds in all states of a nite pre x of and '2 holds on the rest of the path. The property af (') holds in a state s if on every computation path starting from s there exists a state s0 where ' holds.

Formally, the semantics of CTL formulas is given by de ning the satisfaction relation K; s j= ', which tells us when a formula ' holds in a state s of the Kripke structure K.

De nition 3 (Satisfaction Relation for a Kripke Structure). Given a Kripke structure K = hS; I; R; Li, a state s 2 S, and a formula ', we inductively de ne the relation K; s j= ' as follows: K; s j= e i e is an elementary property belonging to L(s) K; s j= not (') i it is not the case that K; s j= ' K; s j= and ('1; '2) i K; s j= '1 and K; s j= '2 K; s j= ex (') i there exists a computation path s0 s1 : : : in K such that s = s0 and K; s1 j= ' K; s j= eu('1; '2) i there exists a computation path s0 s1 : : : in K such that (i) s = s0 and (ii) for some n 0 we have that:

K; sn j= '2 and K; sj j= '1 for all j 2 f0; : : : ; n 1g K; s j= af (') i for all computation paths s0 s1 : : : in K, if s = s0 then there exists n 0 such that K; sn j= '.

References

1. P. A. Abdulla , K. Cerans , B. Jonsson , and Y.-K. Tsay . General decidability theorems for in nite-state systems . Proc. LICS'96 , pages 313 { 321 . IEEE Press, 1996 .

2. P. A. Abdulla , G. Delzanno, N. Ben Henda , and A. Rezine . Monotonic abstraction (On e cient veri cation of parameterized systems) . International Journal of Foundations of Computer Science , 20 ( 5 ): 779 { 801 , 2009 .

3. G. R. Andrews . Concurrent Programming: Principles and Practice. AddisonWesley , 1991 .

4. K. R. Apt and R. N. Bol . Logic programming and negation: A survey . Journal of Logic Programming , 19 , 20 :9{ 71 , 1994 .

5. G. Banda and J. P. Gallagher . Constraint-based abstraction of a model checker for in nite state systems . Proc. WLP 2009 . Potsdam, Germany, 2009 .

6. T. Bultan . BDD vs. constraint-based model checking: An experimental evaluation for asynchronous concurrent systems . Proc. TACAS 2000 , LNCS 1785 , pages 441 { 455 . Springer, 2000 .

7. T. Bultan and T. Yavuz-Kahveci. Action Language Veri er . Proc. ASE 2001 , pages 382 { 386 . IEEE Press, 2001 .

8. W. Chen and D. S. Warren . Tabled evaluation with delaying for general logic programs . JACM , 43 ( 1 ), 1996 .

9. E. M. Clarke , O. Grumberg , and D. Peled . Model Checking. MIT Press, 1999 .

10. P. Cousot and N. Halbwachs . Automatic discovery of linear restraints among variables of a program . Proc. POPL'78 , pages 84 { 96 . ACM Press, 1978 .

11. G. Delzanno. Constraint-based veri cation of parameterized cache coherence protocols . Formal Methods in System Design , 23 ( 3 ): 257 { 301 , 2003 .

12. G. Delzanno, J. Esparza , and A. Podelski . Constraint-based analysis of broadcast protocols . Proc. CSL '99, LNCS 1683 , pages 50 { 66 . Springer, 1999 .

13. G. Delzanno and A. Podelski . Constraint-based deductive model checking . International Journal on Software Tools for Technology Transfer , 3 ( 3 ): 250 { 270 , 2001 .

14. J. Esparza . Decidability of model checking for in nite-state concurrent systems . Acta Informatica , 34 ( 2 ): 85 { 107 , 1997 .

15. F. Fioravanti , A. Pettorossi , and M. Proietti . Verifying CTL properties of in nite state systems by specializing constraint logic programs . Proc. VCL'01, Tech. Rep. DSSE-TR-2001-3 , pages 85 { 96 . University of Southampton, UK, 2001 .

16. F. Fioravanti , A. Pettorossi , and M. Proietti . Verifying in nite state systems by specializing constraint logic programs . Report 657 , IASI-CNR , Roma, Italy, 2007 .

17. L. Fribourg and H. Olsen . Proving safety properties of in nite state systems by compilation into Presburger arithmetic . Proc. CONCUR'97, LNCS 1243 , pages 96 { 107 . Springer, 1997 .

18. J. Handy . The Cache Memory Book . Morgan Kaufman, 1998 . Second Edition .

19. T. A. Henzinger , P.-H. Ho , and H. Wong-Toi . HYTECH: A model checker for hybrid systems . International Journal on Software Tools for Technology Transfer , 1 ( 1 -2): 110 { 122 , 1997 .

20. L. Lamport . A new solution of Dijkstra's concurrent programming problem . Communications of the ACM , 17 ( 8 ): 453 { 455 , 1974 .

21. D. Lesens and H. Sa di. Abstraction of parameterized networks . Electronic Notes of Theoretical Computer Science , 9 : 41 , 1997 .

22. M. Leuschel . Improving homeomorphic embedding for online termination . Proc. LOPSTR'98, LNCS 1559 , pages 199 { 218 . Springer, 1999 .

23. M. Leuschel and H. Lehmann . Coverability of reset Petri nets and other wellstructured transition systems by partial deduction . Proc. CL 2000 , LNAI 1861 , pages 101 { 115 . Springer, 2000 .

24. M. Leuschel , B. Martens , and D. De Schreye. Controlling generalization and polyvariance in partial deduction of normal logic programs . ACM Transactions on Programming Languages and Systems , 20 ( 1 ): 208 { 258 , 1998 .

25. M. Leuschel and T. Massart . In nite state model checking by abstract interpretation and program specialization . Proc. LOPSTR'99 , LNCS 1817 , pages 63 { 82 . Springer, 2000 .

26. The MAP Transformation System . www.iasi.cnr.it/ proietti/system.html, 2010 .

27. U. Nilsson and J. Lu bcke. Constraint logic programming for local and symbolic model-checking . Proc. CL 2000 , LNAI 1861 , pages 384 { 398 . Springer, 2000 .

28. J. C. Peralta and J. P. Gallagher . Convex hull abstractions in specialization of clp programs . Proc. LOPSTR 2002 , LNCS 2664 , pages 90 { 108 , 2003 .

29. G. L. Peterson . Myths about the mutual exclusion problem . Information Processing Letters , 12 ( 3 ): 115 { 116 , 1981 .

30. A. Pnueli and E. Shahar . A platform for combining deductive with algorithmic veri cation . Proc. CAV'96, LNCS 1102 , pages 184 { 195 . Springer, 1996 .

31. Y. S. Ramakrishna , C. R. Ramakrishnan , I. V. Ramakrishnan , S. A. Smolka , T. Swift , and D. S. Warren . E cient model checking using tabled resolution . Proc.CAV'97, LNCS 1254 , pages 143 { 154 . Springer, 1997 .

32. A. Roychoudhury , K. Narayan Kumar , C. R. Ramakrishnan , I. V. Ramakrishnan , and S. A. Smolka . Veri cation of parameterized systems using logic program transformations . Proc. TACAS 2000 , LNCS 1785 , pages 172 { 187 . Springer, 2000 .

33. H. B. Sipma , T. E. Uribe , and Z. Manna . Deductive model checking . Formal Methods in System Design , 15 : 49 { 74 , 1999 .

34. M. H. S rensen and R. Glu ck. An algorithm of generalization in positive supercompilation . Proc. ILPS'95 , pages 465 { 479 . MIT Press, 1995 .

35. L. D. Zuck and A. Pnueli . Model checking and abstraction to the aid of parameterized systems (A survey) . Computer Languages, Systems & Structures , 30 ( 3-4 ): 139 { 169 , 2004 .