Parosh Aziz Abdulla

Mohamed Faouzi Atig

Giorgio Delzanno

Andreas Podelski

Push-Down Automata with Gap-Order Constraints

We consider push-down automata with data (PDAD) that operate on variables ranging over the set of natural numbers. The conditions on variables are defined via gap-order constraint. Gap-order constraints allow to compare variables for equality, or to check that the gap between the values of two variables exceeds a given natural number. The messages inside the stack are equipped with values that are natural numbers reflecting their "values". When a message is pushed to the stack, its value may be defined by a variable in the program. When a message is popped, its value may be copied to a variable. Thus, we obtain a system that is infinite in two dimensions, namely we have a stack that may contain an unbounded number of messages each of which is equipped with a natural number. We present an algorithm for solving the control state reachability problem for PDAD based on two steps. We first provide a translation to the corresponding problem for context-free grammars with data (CFGD). Then, we use ideas from the framework of well quasi-orderings in order to obtain an algorithm for solving the reachability problem for CFGDs.

Introduction

Model checking has become one of the main techniques for algorithmic verification of computer systems. The original applications were found in context of finite-state systems, such as hardware circuits, where the behavior of the system can be captured by a finite state machine. In the last two decades, there has also been a large amount of work devoted to extending model checking so that its can handle models with infinite state spaces such as Petri nets, timed automata, push-down systems, counter automata, and channel machines. Recent works have considered systems that are infinite in multiple dimensions. For instance, many classes of timed protocols are parameterized (consist of unbounded numbers of components), and hence they can be naturally modeled by timed Petri nets [START_REF] Abdulla | Better is better than well: On efficient verification of infinite-state systems[END_REF]. Also, many message passing protocols have behaviors that are constrained by timing conditions, giving rise to timed channel systems [START_REF] Abdulla | Timed lossy channel systems[END_REF].

In particular, Push-Down Automata (PDA) have been studied extensively as a model for the analysis of recursive programs (e.g., [START_REF] Bouajjani | Reachability analysis of pushdown automata: Application to model-checking[END_REF][START_REF] Schwoon | Model-Checking Pushdown Systems[END_REF][START_REF] Esparza | Efficient algorithms for model checking pushdown systems[END_REF][START_REF] Esparza | A BDD-based model checker for Büchi programs[END_REF]). The model of PDA has been extended to allow quantitative reasoning with respect to time [START_REF] Abdulla | Dense-timed pushdown automata[END_REF] and probabilities [START_REF] Etessami | Algorithmic verification of recursive probabilistic state machines[END_REF][START_REF] Esparza | Model checking probabilistic pushdown automata[END_REF]. However, all existing models assume finite-state control, which means that variables in the program are assumed to range over finite domains. In this paper, we consider an extension of PDA, which we call PDAD, that strengthens the model in two ways. First, in addition to the stack, a PDAD also operates on a number of variables ranging over the natural numbers. Furthermore, each message inside the stack is equipped with a natural number which represents its "value". Thus, we get a model that is possibly unbounded in two dimensions, namely we have an unbounded number of messages inside the stack each of which has an attribute that is a natural number. The operations allowed on the stack are the standard push and pop operations. However, when pushing a symbol to the stack, its value may be defined to be the value of a program variable. Also, when a message is popped, then its value may be copied to a variable. A PDAD allows comparing the values of variables according to the gap-order constraint system, where two variables may be tested for equality, or for checking that there is a minimal gap (defined by a natural number) between the values of the two variables. Also, a variable may be assigned a new arbitrary value, the value of another variable, or a value that is at least some (given) natural number larger than the value of another variable. In this manner, the model of PDAD subsumes two known models, namely that of PDA (which we get by removing the variables in the program and by neglecting the values of the symbols in the stack), and the model of Integral Relational Automata [START_REF] Čerāns | Deciding properties of integral relational automata[END_REF] (which we get by removing the stack).

In this paper, we show decidability of the control reachability problem for PDAD. Given a control (local) state of the automaton, we check whether the automaton reaches the state from its initial configuration. We solve the problem in two steps. We introduce a class of Context-Free Grammars with Data (CFGD). In a CFGD, each non-terminal has an arity. The grammar generates terms each of which is either a terminal or a nonterminal equipped with a tuple of natural number (as many as its arity). An application of a production rewrites a term to a set of terms. Such an application is constrained by the arguments of the involved non-terminals. The constraints are defined by gap-order conditions. For CFGD, we solve a reachability problem in which we ask whether it is possible to derive a set of terms each of which is a terminal belonging to a given set of terminals. In the first step of our method, we give a reachability analysis algorithm that solves the above mentioned problem for CFGDs.

The algorithm is based on a constraint representation of infinite sets of terms, and it is formulated within the framework of well structured transition systems [START_REF] Abdulla | Well (and Better) Quasi-Ordered Transition Systems[END_REF][START_REF] Abdulla | General decidability theorems for infinitestate systems[END_REF].

The second step of our method translates a given PDAD into a CFGD so as to exploit the corresponding reachability analysis procedure to solve control state reachability for PDADs.

To our knowledge our result yields a new decidable fragment of pushdown automata with data (see Section 10).

Preliminaries

In this section, we introduce some notations and definitions that we will use in the rest of the paper. We use N to denote the set of natural numbers.

We fix a finite set V of variables that range over N. A valuation is a mapping Val : V Ñ N, i.e., it assigns a natural number to each variable. Given a variable x P V , a natural number c P N, and a valuation Val : V Ñ N, we use Val rx Ð cs to denote the valuation Val 1 defined as follows: Val 1 pxq " c, and Val 1 pyq " Valpyq for all y P pV ztxuq.

A renaming is a mapping Ren : V Ñ V , i.e., it renames each variable to another one.

A renaming Ren does not need to be injective, i.e., several variables may be renamed to the same variable by Ren. We say that Ren is a renaming for W if Ren pxq P W for all x P V . For a set A, we use A ˚to denote the set of finite words over A. We use ε to denote the empty word. For words α 1 , α 2 P A ˚, we use α 1 ¨α2 to denote the concatenation of α 1 and α 2 .

A transition system is a tuple xϒ, γ init , ÝÑy where ϒ is a (potentially infinite) set of configurations, γ init P ϒ is the initial configuration, and ÝÑĎ ϒ ˆϒ is the transition relation. As usual, we write γ ÝÑ γ 1 to denote that xγ, γ 1 y PÝÑ, and use Ý Ñ to denote the reflexive transition closure of ÝÑ. For a configuration γ P ϒ and a set Γ Ď ϒ of configurations, we use γ Ý Ñ Γ to denote that γ Ý Ñ γ 1 for some γ 1 P Γ.

Push-Down Automata with Data

In this section, we introduce Push-Down Automata with Data (PDAD) that are extensions of the classical model of Push-Down Automata (PDA). First, we define the model, then we define the operational semantics, i.e., the transition system induced by a PDAD, and finally we introduce the reachability problem. As in the case of a PDA a PDAD operates on an unbounded stack to which it can push (append) messages and from which it can pop (remove) message in last-in-first-out manner. The messages are chosen from a finite alphabet. PDADs extend PDAs in two ways. First, in addition to the stack, the automaton is equipped with a finite set of variables ranging over natural numbers. Second, each message inside the stack is equipped by a natural number that represents its "value". The allowed operations on variables are defined by the gap-order constraint system [START_REF] Čerāns | Deciding properties of integral relational automata[END_REF][START_REF] Revesz | A closed-form evaluation for datalog queries with integer (gap)-order constraints[END_REF]. More precisely, the model allows non-deterministic value assignment, copying the value of one variable to another, and assignment of a value v to some variable such that v is larger of at least a given natural number than the current value of another variable. The transitions may be conditioned by tests that compare the values of two variables for equality, or that give the minimal allowed gap between two variables. A push operation may copy the value of variable to the pushed message, and a pop operation may copy the value of the popped message to a variable.

Model.

A PDAD A is a tuple xQ, q init , A, ∆y where Q is the finite set of states, q init P Q is the initial state, A is the stack alphabet, and ∆ is the transition relation. We remark that the stack alphabet is infinite since it consists of pairs xa, ℓy where a is taken from a finite set and ℓ is a natural number. A transition δ P ∆ is a triple xq 1 , op, q 2 y where q 1 , q 2 P Q are states and op is an operation of one of the following forms: (i) nop is an empty operation that does not change the values of the variables or the content of the stack, (ii) x Ð ˚assigns non-deterministically an arbitrary value in N to the variable x, (iii) y Ð x copies the value of variable x to y, (iv) y Ð pą c xq assigns non-deterministically to y a value that exceeds the current value of x by c (so the new value of y is ą x `c), (v) y " x checks whether the value of y is equal to the value of x, (vi) x ă c y checks whether the gap between the values of y and x is larger than c, (vii) push paq pxq pushes the symbol a P A to the stack and assigns to it the value of x, and (viii) poppaq pxq pops the symbol a P A (if a is the top-most symbol at the stack) and assigns its value to the variable x.

Transition System. A PDAD induces a transition system as follows. A configuration γ is a triple xq, Val, αy where q P Q is a state, Val : V Þ Ñ N is a valuation, and α P pA ˆNq defines the content of the stack (each element of the word is a pair xa, cy where a is the symbol and c is its value).

We define the transition relation ÝÑ:" Y δP∆ δ ÝÑ, where δ ÝÑ describes the effect of the transition δ. For configurations γ " xq, Val, αy, γ 1 " xq 1 , Val 1 , α 1 y, and a transition δ " xq 1 , op, q 2 y P ∆, we write γ δ ÝÑ γ 1 to denote that q " q 1 , q 1 " q 2 , and one of the following conditions is satisfied: We define the initial configuration γ init :" xq init , Val init , εy, where Val init pxq " 0 for all x P V . In other words, we start from a configuration where the automaton is in its initial state, the values of all variables are equal to 0, and the stack is empty (the fact that we choose to initialize the variables to 0 is not crucial for solving the problem).

-op is nop, Val 1 " Val,
For a configuration and a state q P Q, we write γ Ý Ñ q to denote that γ Ý Ñ γ 1 " xq, Val, αy for some Val : V Þ Ñ N and α P pA ˆNq

˚.
In other words, from γ we can reach a configuration whose state is q.

Reachability Problem. In the reachability problem PDAD-REACH, given a PDAD A " xQ, q init , A, ∆y and a state q target P Q, we ask whether γ init Ý Ñ q target .

Context-Free Grammars with Data

In this section, we introduce Context-Free Grammars with Data (CFGD) that are extensions of the classical model of Context-Free Grammars (CFG) in which (terminal and non terminal) symbols are defined by terms with free variables and productions have conditions defined by gap order constraints. We define the model, the operational semantics, and the reachability problem.

Model. A Context-Free Grammars with Data (CFGD) is a tuple G " xS , X init , Py, where S is a finite set of symbols. X init P S is the start (or initial) symbol, and P is the set of productions. Each symbol X has an arity ρ pXq P N that is a natural number. Without loss of generality, we assume that ρ pX init q " 1. A term has the form Xpx 1 , . . . , x n q where X P S , ρ pXq " n and x 1 , . . . x n P V are variables. A ground term has the form Xpc 1 , . . . , c n q where X P S , ρ pXq " n and c 1 , . . . c n P N are natural numbers. For a term σ of the form Xpx 1 , . . . , x n q we define Sym pσq " X and Var pσq " tx 1 , . . . , x n u. We define Sym pσq for a ground term σ similarly. A (ground) sentence α is a finite set tσ 1 , σ 2 , ¨¨¨, σ n u, where each σ i is a (ground) term. We define Sym pαq :" tSym pσ 1 q , . . . , Sym pσ n qu, i.e., it is the set of symbols that occur in α. For a term σ " Xpx 1 , . . . , x n q and a valuation Val, we define Val pσq :" XpValpx 1 q , . . . , Valpx n qq to be the ground term we get by substituting each variable x i in σ by Valpx i q. For a sentence α, we define Val pαq similarly.

A condition θ is a finite conjunction of formulas of the forms: x ă c y or x " y, where

x, y P V and c P N. Here x ă c y stands for x `c ă y. Sometimes, we treat a condition θ as set, and write e.g. px ă c yq P θ to indicate that x ă c y is one of the conjuncts in θ.

For a valuation Val, we use Valpθq to denote the result of substituting each variable x in θ by Val pxq. We use Val |ù θ to denote that Valpθq evaluates to true. We use Var pθq to denote the set of variables that occur in θ.

A production p is of the form σ ❀ α : θ, where σ is a term, α is a non-empty sentence, and θ is a condition. We often use the notation σ ❀ σ 1 ¨¨¨σ n : θ to denote the production σ ❀ tσ 1 , . . . , σ n u : θ (i.e. a sequence in the right-hand side denotes a set of terms). We use N to denote the set of non-terminals consisting of symbols that occur in the left-hand side of a production (we say that they are defined by a production). We use T to denote the set of terminals consisting of symbols that do not occur in the left-hand side of a production. Furthermore, we use A T to denote the set of ground terms with symbols in T .

Transition System. A configuration γ is a ground sentence. We define a transition relation ÝÑ G on the set of configurations by ÝÑ G :" Y pPP p ÝÑ where p ÝÑ represents the effect of applying the production p. More precisely, for a production p P P of the form σ ❀ α : θ, we have γ

1 p ÝÑ γ 2 if there is a valuation Val |ù θ such that γ 1 " α 1 Y tValpσqu and γ 2 " α 1 Y tValpαqu.
For a set S of ground terms, we define Pre pSq to be the set of ground terms σ which can, through the single application of a production, generate a configuration γ Ď S (i.e., σ ÝÑ G γ). Let Pre ˚p¨q denote the transitive closure of Pre p¨q.

We will use the following lemmata later in the paper. Lemma 1. Let α be a ground sentence of G . Then, if for every ground term σ P α, we have σ Ý Ñ G α 2 for some ground sentence α 2 such that Sympα 2 q Ď T , then α Ý Ñ G α 1 for α 1 such that Sympα 1 q Ď T . Lemma 2. Let S be a set of ground terms and σ be a ground term such that σ P Pre ˚pSq. If σ R S then there is a ground term σ 1 P pPre pSq zSq.

Reachability Problem. In the reachability problem CFGD-REACH, we are given a CFGD G " xS , X init , Py and we are asked the question whether X init p0q Ý Ñ G α for some ground sentence α such that Sym pαq Ď T . In other words, we start from a configuration consisting of the start symbol with its parameter is equal to zero, and ask whether the system can reach a configuration where all its ground terms have symbols in T . CFGD vs CFG A Context-Free Grammars (CFG) is defined by production of the form S Ñ w where w is a word defined over terminal and non terminal symbols. We can encode a CFG as a CFGD by associating to each terminal/non terminal symbol X (except the initial) a term Xpa, bq in which pa, bq are used to maintain an order in the right-hand side of a rule. For instance, the production S Ñ SaS is encoded via the CFGD production Spx, yq Ñ tSpx, zq, apz,tq, Spt, yqu : x ă z, z ă t,t ă y.

CFGD vs CMRS CFGD also differ from the CMRS model [START_REF] Abdulla | A classification of the expressive power of wellstructured transition systems[END_REF]. CMRS is obtained by combining multiset rewriting and Gap Order constraints and it is aimed at modeling concurrent processes. CMRS rules have multiple heads and work over multisets of monadic terms (i.e. with a single argument, no nested terms). Differently from CMRS, CFGD productions have a single term in the left-hand side and a set of terms in the righthand side. This implies that multiple occurrences (with the same variables) of a term like ppx, yq are counted only once. Furthermore, non-terminal symbols have arbitrary finite arity.

Symbolic Encoding

In this section, we define the symbolic representation used in the definition of the reachability algorithm (Section 6). The algorithm operates on constraints, where each constraint φ characterizes a (potentially) infinite set φ of ground terms. A constraint φ is of the form σ : θ where σ is a term and θ is a condition. We define Sym pφq " Sympσq and Var pφq " Var pσq Y Var pθq. Definition 3. The constraint φ characterizes a set of ground terms defined by φ " tσ 1 | DVal. pVal |ù θq ^pσ 1 " Valpσqu. For a finite set of constraints Φ, Φ " Ť φPΦ φ .

Without loss of generality, we can assume that Var pθq " Var pσq, and that θ is consistent (constraints with inconsistent conditions characterize empty sets of configurations, and can therefore be safely discarded from the reachability analysis). A term Xpx 1 , . . . , x n q is said to be pure if

x i ‰ x j whenever i ‰ j. A constraint σ : θ is said pure if σ is pure.
We can assume without loss of generality that all constraints are pure. The reason is that if a variable x occurs (say) twice then the two occurrences of x can be replaced by two different variables y 1 and y 2 provided that we add a new conjunct y 1 " y 2 to the condition θ. For constraints φ 1 , φ 2 , we use φ 1 Ď φ 2 to denote that φ 1 subsumes φ 2 , i.e., φ 1 Ě φ 2 . Then, it is easy to see that checking whether φ 1 Ď φ 2 can be reduced to the satisfiability problem for an existential Presburger formula (which is known to be NP-COMPLETE [START_REF] Verma | On the complexity of equational Horn clauses[END_REF] ).

Lemma 4. For constraints φ 1 , φ 2 , the problem of checking whether φ 1 Ď φ 2 is decidable.

The following lemma states that we can transform any constraint φ of the form σ : θ to an equivalent constraint cleanpφq of the form σ : θ 1 such that Var pθ 1 q " Var pσq (i.e., we remove the extra-variables pVar pθq zVar pσqq from θ in order to satisfy the assumption that Var pθq " Var pσq). Lemma 5. [START_REF] Revesz | A closed-form evaluation for datalog queries with integer (gap)-order constraints[END_REF] Given a constraint φ of the form σ : θ, we can construct a constraint cleanpφq of the form σ : θ 1 such that Var pθ 1 q " Var pσq and cleanpφq " φ .

Given two terms σ 1 and σ 2 , we say that σ 1 matches σ 2 iff Sympσ 1 q " Sym pσ 2 q. For matching terms σ 1 " Xpx 1 , . . . , x n q and σ 2 " Xpy 1 , . . . , y n q, where σ 2 is pure, we define Ren σ 2 σ 1 to be a renaming such that Ren σ 2 σ 1 py i q " x i for all i : 1 ď i ď n. Consider a production p " σ ❀ σ 1 ¨¨¨σ n : θ and constraints φ 1 " σ 1 1 : θ 1 , . . . , φ n " σ 1 n : θ n such that σ i and σ 1 i are matching, and such that σ 1 i is pure for all i : 1 ď i ď n. We define p b φ 1 b ¨¨¨b φ n to be the constraint σ : θ ^Ren

σ 1 1 σ 1 pθ 1 q ^¨¨¨^Ren σ 1 n σ n pθ n q.
For a set Φ of constraints, and production p P P, we define Pre p pΦq :" tcleanpφ 1 q| Dφ 1 , . . . , φ n P Φ. φ 1 " p b φ 1 ¨¨¨b φ n u. We define Pre pΦq :" Y pPP Pre p pΦq. Intuitively, Pre pΦq defines a finite set of constraints that characterize the terms which can, through the single application of a production, generate a set of terms each of which belongs to Φ.

Lemma 6.

Ť

φ 1 PPrepΦq φ 1 " Pre p Φ q.
For the set T of terminals, we define Φ T :" tapx 1 , . . . , x n q : true| a P T , ρ paq " nu Notice that Φ T denotes the set of configurations whose symbols are in T .

Reachability Analysis

In this section, we present an algorithm for solving the reachability analysis problem for CFGDs, and prove its partial correctness. The algorithm (Algorithm 1) inputs a CFGD G " xS , X init , Py and answers the question whether we can reach a sentence where all the occurring terms are in A T (i.e. terms with symbols in T ). The algorithm maintains two sets of constraints: a set ToExplore, initialized to Φ T , of constraints that have not yet been analyzed; and a set Explored, initialized to the empty set, of constraints that contain constraints that have already been analyzed. The algorithm preserves the following four invariants:

1. For each σ P ToExplore Y Explored , σ Ý Ñ α for some α s.t. Sympαq Ď T . 2. If X init p0q Ý Ñ α for some α s.t. Sym pαq Ď T , then there is a ground term σ P

ToExplore such that σ R Explored . 3. X init p0q R Explored . 4. Φ T Ď ToExplore Y Explored .
It is easy to see that the third and fourth invariants will be preserved. More precisely, for the third invariant, Explored is initially empty, and the condition at line 5 prevents Algorithm 1: Reachability analysis for a CFGD. This invariant is preserved since each time we remove a constraint from ToExplore (line 4), it is either eventually moved to Explored (line 9), or (in case it is discarded at line 6) there is already a constraint φ 1 P Explored with φ 1 Ě φ . Also, each time we remove a constraint φ 1 from Explored (line 9), we add the constraint φ to Explored where φ Ě φ 1 . Below, we show that the first two invariants are also preserved. Initially, the first invariant holds since pToExplore Y Exploredq " Φ T . The second invariant also holds initially since Explored " H and ToExplore " Φ T ‰ H. Due to the first two invariants, the following two conditions can be checked during each step of the algorithm:

Input: A CFGD G " xS , X init ,
-From the second invariant, if ToExplore becomes empty then the algorithm terminates with a negative answer. -From the first invariant, if a constraint φ is detected such that X init p0q P φ , then the algorithm terminates with a positive answer.

If neither of the two conditions is satisfied, the algorithm proceeds by picking and removing a constraint φ from ToExplore. Two possibilities arise depending on the value of σ:

-If there exists a constraint φ 1 P Explored with φ 1 Ď φ, then we discard φ. The first invariant is preserved since this operation will not add any new elements to ToExplore Y Explored . If X init p0q Ý Ñ α for some α s.t. Sym pαq Ď T , then the second invariant and the fact that φ Ď Explored imply that there is still some σ P ToExplore such that σ R Explored . This means that the second invariant will also be preserved by this step.

-Otherwise, we compute the elements of Pre pExplored Y φq, add them in ToExplore, move φ to Explored, and remove all constraints in Explored that are subsumed by φ. Let Explored old and Explored new be the contents of the set Explored before resp. after performing the operation. Define ToExplore old and ToExplore new analogously. The operation preserves the first invariant as follows. Pick any σ P ToExplore new Y Explored new . If σ P ToExplore old Y Explored old then the result follows by the first invariant. Otherwise we know that σ P Pre pExplored old Y tφuq , i.e., σ ÝÑ G α where α Ď Explored old Y tφu (see Lemma 6). By the induction hypothesis and the first invariant, we know that every ground term σ 1 P α, σ 1 Ý Ñ G α 1 for some α 1 s.t. Sympα 1 q Ď T . Hence α Ý Ñ G α 2 for some α 2 s.t. Sym pα 2 q Ď T (see Lemma 1). In other words, σ ÝÑ G α Ý Ñ G α 2 s.t. Sympα 2 q Ď T . The operation also preserves the second invariant as follows. Assume that X init p0q Ý Ñ G α for some α s.t. Sympαq Ď T . There are two cases. If there is a σ P Φ T such that σ Explored new , then by the fourth invariant σ P ToExplore new and the invariant holds immediately. Otherwise, Φ T Ď Explored new . Since X init p0q Ý Ñ G α we have also that X init p0q P Pre ˚p Explored new q. By the third invariant, we know that X init p0q R Explored new . By Lemma 2 that there is a ground term σ P pPre p Explored new q z Explored new q. Since Explored new " Explored old Y tφu it follows that σ P Pre pExplored old Y tφuq and hence σ P ToExplore new . This give us the following theorem.

Theorem 7. Algorithm 1, under termination assumption, always return the correct answer.

Termination

In this section, we show that Algorithm 1 is guaranteed to terminate. To do that, we first recall some basics of the theory of well and better quasi-orderings. Then, we introduce a new class of constraints that we call flat constraints and show that they are better quasiordered. We show that each condition can be translated into a number of flat constraints.

We use this to show that the set of conditions is well quasi-ordered under set inclusion. This leads to the well quasi-ordering of the set of constraints (of Section 5). Finally, we show the termination of the algorithm.

WQOs and BQOs. A Quasi-Ordering (or a QO for short), is a pair xA, ĺy where ĺ is a reflexive and transitive binary relation on the set A. A QO xA, ĺy is a Well Quasi-Ordering (WQO), if for each infinite sequence a 1 , a 2 , a 3 , . . . of elements of A , there are i ă j such that a i ĺ a j . The following lemma follows from the definition of a WQO.

Lemma 8. For QOs ĺ and ĺ 1 on some set A, if ĺĎĺ 1 and ĺ is a WQO then ĺ 1 is a WQO.

Given a QO xA, ĺy, we define a QO xA ˚, ĺ ˚y on the set of words A ˚such that a 1 a 2 ¨¨¨a m ĺ ˚a1 1 a 1 2 ¨¨¨a 1 n if there is an injection h : t1, . . . , mu Þ Ñ t1, . . . , nu such that i ă j implies hpiq ă hp jq for all i, j : 1 ď i, j ď m, and a i ĺ a 1 hpiq for each i : 1 ď i ď m.

We define the relation ĺ P on the powerset P pAq (finite set of elements in A) of A, so

that A 1 ĺ P A 2 if @a 2 P A 2 .Da 1 P A 1 .a 1 ĺ a 2 .
We define the relation ĺ p on the Cartesian product A 1 ˆ. . . ˆAn of orders xA i , ď i y for i : 1, . . . , n, so that xa 1 , . . . , a n y ĺ p xa 1 1 , . . . , a 1 n y if a i ĺ i a 1 i for i : 1, . . . , n. In the following lemma we state some properties of BQOs4 [START_REF] Abdulla | Better is better than well: On efficient verification of infinite-state systems[END_REF][START_REF] Marcone | Foundations of BQO theory[END_REF].

Lemma 9. -Each BQO is WQO. -If A
-d i " d j if h ψ piq " h ψ p jq. -If h ψ piq " k. and h ψ p jq " k `1 then c k`1 ă d j ´di .
In other words, the variable x i represents d i in ψ. If two variables are mapped to the same set then their values should be identical. Furthermore, the natural numbers c i define the gaps between values of variables belonging to the different sets. For flat constraints

ψ " A 0 c 1 A 1 ¨¨¨c m A m and ψ 1 " A 1 0 c 1 1 A 1 1 ¨¨¨c 1 m A 1
m over V , we write ψ ĺ ψ 1 to denote that (i) A 1 i " A i for all i : 0 ď i ď m, and (ii) c i ď c 1 i for all i : 1 ď i ď m. The following lemma follows from the definitions. Lemma 10. ψ ĺ ψ 1 implies that ψ Ě ψ 1 .

By Lemma 9 it follows that

Lemma 11. ĺ is a BQO on the set of flat constraints.

Proof. We first observe that flat contraints can be viewed as tuples with at most K " |V | partitions and |V | ´1 constants and we can always add finite sequences such as 0H0 . . . 0H to consider K-tuples only. From Lemma 9, we know that xN, ďy and xP pV q , "y are BQOs. Thus, the Cartesian product pP pV q ˆNq K´1 ˆP pV q with ĺ is still a BQO.

Flattening. Consider a condition θ with Var pθq " tx 1 , . . . , x n u (recall the definitions of conditions and constraints from Section 5). We define θ to be the set of vectors v " xd 1 , . . . , d n y P N n , such that there is a valuation Val with Val |ù θ and Val px i q " d i for all i : 1 ď i ď n. Furthermore, for two conditions on the same set of variables we define θ Ď θ 1 iff θ Ě θ 1 . A flattening of θ is a flat constraint ψ over Var pθq, of the form A 0 c 1 A 1 ¨¨¨c m A m where c 1 , . . . , c m ě 0 are minimal natural numbers such that the following conditions are satisfied:

-If px " yq P θ then x, y P A i for some i : 1 ď i ď m.

-If px ă c yq P θ, x P A i , and y P A j then c ď ´řj k"i`1 pc k `1q ´1¯.

Intuitively, variables which are required to be equal by θ, are put in the same X i . Also, variables which are ordered according to θ, are placed sufficiently far apart to cover the corresponding gap. We define F pθq to be the set of flattening of θ. In general conditions induce a partial order between variables. The flattening contains all linearizations with minimal gaps (constants) between variables. Notice that this set is finite. As an example, consider the condition x ă 2 y, x ă 1 z. Since there are no constraints on y and z, we have three different flattening where y ă z or y " z or y ą z, namely txu2tyu0tzu, txu2ty, zu, and txu1tzu0tyu.

We define an ordering ĺ on conditions such that θ ĺ θ 1 if for each ψ 1 P F pθ 1 q there is a ψ P F pθq with ψ ĺ ψ 1 . From Lemma 10 we get the following.

Lemma 12. θ ĺ θ 1 implies that θ Ě θ 1 .
The following lemma follows from Lemma 9 and Lemma 11.

Lemma 13. ĺ is a BQO (and hence WQO) on the set of conditions.

From Lemma 13, Lemma 12, and Lemma 8 we get the following lemma. Lemma 14. The set of conditions is WQO under Ď.

The following lemma then holds.

Lemma 15.

The set of constraints is WQO under Ď.

Proof. Consider an infinite sequence of constraints: φ 1 , φ 2 , φ 3 , . . .. Since the set N Y T is finite, there is an infinite sequence i 1 ă i 2 ă i 3 ă ¨¨¨such that Sym pφ i 1 q " Sym pφ i 2 q " Sym pφ i 3 q " ¨¨¨. If Sym `φi j ˘P T then the result follows immediately (since φ i j " Sym `φi j ˘( for all j ě 1). Otherwise, we can assume, without loss of generality, that φ i j is of the form Xpx 1 , . . . , x n q : θ i j . Notice that each Var `θi j ˘" tx 1 , . . . , x n u is a condition over tx 1 , . . . , x n u. By Lemma 14, there are j ă k such that θ i j Ď θ i k , and hence φ i j Ď φ i k .

Termination. The reason why the algorithm always terminates is that only a finite set of constraints can be added to Explored. This can be explained as follows. By definition, a new element φ is added to Explored only if φ 1 Ď φ, for each φ 1 already added to Explored. This means that the constraints added to Explored form a sequence φ 1 , φ 2 , φ 3 , . . ., such that φ i Ď φ j for all i ă j. By WQO of Ď (Lemma 15) it follows that this sequence is finite. This gives the following theorem. Theorem 16. Algorithm 1 is guaranteed to terminate.

Translation

Reachability with Empty Stacks. We consider a different variant of PDAD-REACH which we call PDAD-REACH-EMPTY. An instance of PDAD-REACH-EMPTY is defined by a PDAD A " xQ, q init , A, ∆y and a state q target P Q, and we are asked whether γ init Ý Ñ γ for some γ of the form xq target , Val, εy, i.e., we ask whether we reach q target at a configuration where the stack is empty. Given an instance of PDAD-REACH, defined by a PDAD A " xQ, q init , A, ∆y and a state q target P Q, we derive an equivalent instance of PDAD-REACH-EMPTY as follows. We construct a new PDAD A 1 from A by adding a new state q new to Q, and adding a transition labeled with nop from q target to q new . For each member a P A of the stack alphabet, we add a self-loop on q new that pops a (with any value). The two problem instances are equivalent as follows. Suppose that q new is reachable with an empty stack in A 1 . Then, the run of A 1 reaching q new must have passed through q target (since q new can only be reached from q target ). This means that q target is reachable in A . On the other hand, suppose that q target is reachable in A . Then, A 1 can simulate the run of A until it reaches q target . From there, it takes the transition to q new , and starts executing the self-loops, popping all the symbols in the stack until the stack becomes empty.

From PDAD to CFGD. Suppose that we are given an instance of PDAP-REACH-EMPTY defined by a PDAD A " xQ, q init , A, ∆y and a state q target P Q. Let tx 1 , . . . , x n u be the set of variables that occur in A . We derive an equivalent instance of CFGD-REACH defined by a CFGD G " xS , X init , Py. The set T of G is defined by the singleton set ttu and we assume that the arity of t is 0 (i.e., ρ ptq " 0). The set of N of G is defined as follows: For each pair of states q 1 , q 2 P Q and symbol a P A Y tKu, with K R A, we have a nonterminal X pq 1 ,a,q 2 q P N with arity 2n `1. The symbol K is used to denote that the stack of A is empty. The set of non-terminal set N contains the initial symbol X init (by definition).

In the following, let ȳ denote a vector xy 1 , . . . , y n y of length n, and define ȳris :" y i for i : 1 ď i ď n. For vectors z " xz 1 , . . . , z n y and ȳ " xy 1 , . . . , y n y, we use z " ȳ (resp. z ‰ j ȳ for some j : 1 ď j ď n) to denote the condition Ź 1ďiďn z i " y i (resp. Ź p1ďiďnq^pi‰ jq z i " y i ). Furthermore, for brevity, we sometimes shorten a conjunction of conditions θ 1 . . . ^θn into a list θ 1 , . . . , θ n .

Intuitively, a non-terminal of the form X pq 1 ,a,q 3 q p ȳ, z, ℓq represents a run of A from a configuration where the state is q 1 , the topmost stack symbol is a and its corresponding value is given by the value ℓ (if a " K then the stack is empty), and the valuation of the shared variables of A is given by the valuation of ȳ, to a configuration with a stack content where a has been popped and where the state is q 3 and the valuation of the shared variables of A is given by the valuation of z.

The set P is derived from ∆, and it contains the productions of Fig. 1. Then the following property holds. Proposition 17. γ init Ý Ñ γ for some γ " xq target , Val, εy iff X init Ý Ñ G α for some sentence α such that Sympαq Ď T .

As an immediate consequence of the above Proposition, Theorem 7, and Theorem 16, we get: Theorem 18. The PDAD-REACH and PDAD-REACH-EMPTY problems are decidable for PDADs.

xq 1 , nop, q 2 y P ∆ q 3 P Q pX pq 1 ,a,q 3 q p ȳ, z, ℓq ❀ X pq 2 ,a,q 3 q p ȳ1 , z1 , ℓ 1 q : ȳ " ȳ1 , z " z1 , ℓ " ℓ 1 q P P xq 1 , x i Ð ˚, q 2 y P ∆ q 3 P Q pX pq 1 ,a,q 3 q p ȳ, z, ℓq ❀ X pq 2 ,a,q 3 q p ȳ1 , z1 , ℓ 1 q : ȳ ‰ i ȳ1 , z " z1 , ℓ " ℓ 1 q P P @ q 1 , x i Ð x j , q 2 D P ∆ q 3 P Q pX pq 1 ,a,q 3 q p ȳ, z, ℓq ❀ X pq 2 ,a,q 3 q p ȳ1 , z1 , ℓ 1 q : ȳ ‰ i ȳ1 , z " z1 , ℓ " ℓ 1 , ȳ1 ris " ȳr jsq P P p @ q 1 , x i Ð `ąc x j ˘, q 2 D P ∆ q 3 P Q X pq 1 ,a,q 3 q p ȳ, z, ℓq ❀ X pq 2 ,a,q 3 q p ȳ1 , z1 , ℓ 1 q : ȳ ‰ i ȳ1 , z " z1 , ℓ " ℓ 1 , ȳr js ă c ȳ1 risq P P @ q 1 , x j " x i , q 2 D P ∆ q 3 P Q pX pq 1 ,a,q 3 q p ȳ, z, ℓq ❀ X pq 2 ,a,q 3 q p ȳ1 , z1 , ℓ 1 q : ȳ " ȳ1 , z " z1 , ℓ " ℓ 1 , ȳris " ȳr jsq P P @ q 1 , x j ă c x i , q 2 D P ∆ q 3 P Q pX pq 1 ,a,q 3 q p ȳ, z, ℓq ❀ X pq 2 ,a,q 3 q p ȳ1 , z1 , ℓ 1 q : ȳ " ȳ1 , z " z1 , ℓ " ℓ 1 , ȳ1 r js ă c ȳrisq P P xq 1 , push pbq px i q , q 2 y P ∆ q 3 , q 4 P Q pX pq 1 ,a,q 3 q p ȳ, z, ℓq ❀ X pq 2 ,b,q 4 q p ȳ1 , ū, ℓ 1 q X pq 4 ,a,q 3 q p ū1 , z1 , ℓ 2 q : ȳ " ȳ1 , ū " ū1 , z " z1 , ℓ " ℓ 2 , ℓ 1 " ȳrisq P P xq 1 , pop px i q paq , q 2 y P ∆ pX pq 1 ,a,q 2 q p ȳ, z, ℓq ❀ t : ȳ ‰ i z, zris " ℓq P P pX init pxq ❀ X pq init ,K,q target q p ȳ, z, ℓq : Ź 1ďiďn ȳris " xq P P pX pq target ,K,q target q p ȳ, z, ℓq ❀ t : ȳ " zq P P Fig. 1. From transitions of pushdown with data to productions.

Extended PDADs

In this section, we present generalizations of the basic PDAD model for which the results presented in this paper still hold. The first extension consists in adding to conditions of the form x " c, x ą c, and x ă c for a variable x and a constant value c ě 0. The resulting formulas corresponds to the original Gap Order Constraints considered in [START_REF] Revesz | A closed-form evaluation for datalog queries with integer (gap)-order constraints[END_REF].

The second extension consists in adding multiple data fields in each element pushed to the stack. For fixed number of data fields k ě 0, the configuration of PDAD k becomes a triple xq, Val, αy where q P Q is a state, Val : V Þ Ñ N is a valuation, and α P `A ˆNk ˘defines the content of the stack (each element of the word is a pair xa, c 1 , . . . , c k y where a is the symbol and c i is its value for the i-th field).

We now consider operations that manipulate the data fields. We first extend the push operation and consider push paq px 1 , . . . , x k q to push the symbol a P A and to assign to the i-th field the value of x i for i : 1, . . . , k. We also consider operation pop paq px 1 , . . . , x k q to pop the symbol a P A from the stack and to assign to x i the value of the i-th field on the top of the stack i : 1, . . . , k. The operational semantics can be naturally extended in order to cope with tuples of values instead of single one.

Finally, we consider operations that test and modify the data fields on the stack. We can use special identifiers topx 1 , . . . ,topx k to denote such data fields and use them in conditions of transitions.

To encode the resulting model into CFGD, we need to introduce non-terminals with extra arguments that represent both the current value and the (guessed) updated value of data fields. More specifically, we need non-terminals of the form X pq 1 ,a,q 2 q p x, ȳ, z, ūq to represent a run of a A k from a configuration where the state is q 1 , the topmost stack symbol is a and its corresponding data field values are given by the vector z, and the valuation of the shared variables of A is given by the valuation of x, to a configuration with the updated data fields ū and where the state is q 2 and the valuation of the shared variables is given by the valuation of ȳ.

We leave a detailed treatment of this extension for future work.

Related Work and Conclusion

Decidability and complexity of reachability problems for pushdown systems with or without data have been extensively studied in the literature. In [START_REF] Bouajjani | Reachability analysis of pushdown automata: Application to model-checking[END_REF] the authors present an algorithm to compute Post ˚and Pre ˚for a pushdown automata and a regular set of its configurations (represented as automata). Symbolic versions of the algorithms have been studied e.g. in [START_REF] Reps | Weighted pushdown systems and their application to interprocedural dataflow analysis[END_REF]. In [START_REF] Atig | Approximating Petri net reachability along context-free traces[END_REF] the authors consider approximated verification methods for subclasses of pushdown systems called finite indices in which it is possible to handle counters without zero test (i.e. transitions of a Petri net). In [START_REF] Abdulla | The minimal Cost reachability problem in priced timed pushdown systems[END_REF][START_REF] Abdulla | Dense-timed pushdown automata[END_REF] the authors present decidability results for timed extensions of pushdown systems. In [START_REF] Cai | Well-structured extensions of pushdown systems[END_REF] the authors present decidability results for pushdown systems with either a well-quasi ordered set of control locations or of data values. In our model we do not consider a well-quasi ordered data domain, but introduce a well-quasi ordered relation over values pushed to and popped from the stack in order to decide reachability. Our extensions of pushdown system with Gap Order is orthogonal to the above mentioned models. Furthermore, it subsumes the model presented in [START_REF] Rot | Pushdown System Representation For Unbounded Object Creation[END_REF], where the authors consider pushdown systems in which messages carry (object) identifiers that can be compared by equality. In addition to equality tests, Gap Order can be used to order messages in the stack. Concerning our proof techniques, the algorithm for solving the CFGD reachability problem is inspired to the seminal results on Datalog and context-free language reachability [START_REF] Yannakakis | Graph-theoretic methods in database theory[END_REF][START_REF] Reps | Program analysis via graph reachability[END_REF] and to the evaluation of Datalog with Gap Order Constraints [START_REF] Revesz | A closed-form evaluation for datalog queries with integer (gap)-order constraints[END_REF]. CLP programs with Gap Order constraints without conjunctions in the body have been used to model transition systems in [START_REF] Fribourg | Symbolic verification with gap-order constraints[END_REF]. The fixpoint semantics of CLP programs has been used to characterize model checking problems in [START_REF] Delzanno | Model checking in CLP[END_REF] and applied to infinite-state systems in [START_REF] Delzanno | Constraint-based analysis of broadcast protocols[END_REF][START_REF] Delzanno | Automatic verification of cache coherence protocols[END_REF][START_REF] Delzanno | Constraint-based verification of client-server protocols[END_REF][START_REF] Delzanno | Constraint-based verification of parameterized cache coherence protocols[END_REF]. In [START_REF] Čerāns | Deciding properties of integral relational automata[END_REF] extended automata with Gap Order conditions over variables are used as an approximated model of counter systems. The model however does not have recursion. The complexity of verification problems (expressed in temporal logic) for transitions systems with Gap Order Constraints has been studied in [START_REF] Bozzelli | Verification of gap-order constraint abstractions of counter systems[END_REF]. Allowing rules with sets of terms in the right-hand side, GFGD are more general than the model in [START_REF] Bozzelli | Verification of gap-order constraint abstractions of counter systems[END_REF]. Multiset rewriting systems with Gap Order Constraints (i.e. systems with an arbitrary number of integral variables) have been introduced in [START_REF] Abdulla | On the coverability problem for constrained multiset rewriting[END_REF] and applied to different types of systems in [START_REF] Abdulla | Parameterized verification of infinite-state processes with global conditions[END_REF] extending the parameterized models described in [START_REF] Abdulla | Approximated parameterized verification of infinite-state processes with global conditions[END_REF][START_REF] Delzanno | A lightweight regular model checking approach for parameterized systems[END_REF]. These systems are a subclass of multiset rewriting with (linear) constraints applied to infinite state verification, e.g., in [START_REF] Delzanno | Automatic verification of time sensitive cryptographic protocols[END_REF].

The evaluation procedure for Datalog with Gap Order Constraints in [START_REF] Revesz | A closed-form evaluation for datalog queries with integer (gap)-order constraints[END_REF] and its termination depend on specific data structures (weighted graphs kept in normal form) used to represent relations between variables that occur in Datalog clauses. In the present paper we formulate an algorithmic solution to CFGD reachability as an instance of the general framework of well-structured transition systems and apply the theory of betterquasi ordering to naturally infer its termination. This approach has the great advantage of capturing the essential ingredients needed for extending the algorithm to other classes of grammars with data. For instance, under some restrictions on the arity of terms, a slightly modified algorithm can be applied to grammars with sets of terms in the left-hand side of a production. A more formal treatment of this kind of generalization together with a deeper investigation of the complexity of the resulting algorithm is part of our future work.

  and α 1 " α. The values of the variables and the stack content are not changed. -op is x Ð ˚, Val 1 " Valrx Ð cs where c P N, and α 1 " α. The value of the variable x is changed non-deterministically to some natural number. The values of the other variables and the stack content are not changed. -op is y Ð x, Val 1 " Val ry Ð Valpxqs, and α 1 " α. The value of the variable x is copied to the variable y. The values of the other variables and the stack content are not changed. -op is y Ð pą c xq, Val 1 " Valry Ð c 1 s, where c 1 ą Val pxq `c, and α 1 " α. The variable y is assigned non-deterministically a value that exceeds the value of x by c. The values of the other variables and the stack content are not changed. -op is y " x, Valpyq " Val pxq, Val 1 " Val, and α 1 " α. The transition is only enabled if the value of y is equal to the value of x. The values of the variables and the stack content are not changed. -op is x ă c y, Val pyq ą Valpxq `c, Val 1 " Val, and α 1 " α. The transition is only enabled if the value of y is larger than the value of x by more than c. The values of the variables and the stack content are not changed. -op is push paq pxq, Val 1 " Val, and α 1 " xa, Valpxqy ¨α. The symbol a is pushed onto the stack with a value equal to that of x. -op is poppxq paq, α " xa, cy ¨α1 for some c P N, and Val 1 " Valrx Ð cs.

	The symbol
	a is popped from the stack (if it is the top-most symbol), and its value is copied to
	the variable x.

  PyOutput: Is there a subset of terminal symbols T Ď T reachable in G ?

1 ToExplore Ð Φ T ; 2 Explored Ð H 3 while ToExplore ‰ H do 4 remove some φ from ToExplore; 5 if X init p0q P φ then return true; 6 else if Dφ 1 P Explored. φ 1 Ď φ then discard φ; 7 else 8 ToExplore Ð ToExplore Y Pre pExplored Y tφuq; 9 Explored Ð tφu Y φ 1 | φ 1 P Explored ^pφ Ď φ 1 q ( ; 10 return false adding any constraint whose symbol is X init and parameter equals to 0 to Explored. The fourth invariant holds initially since ToExplore Y Explored " Φ T Y H " Φ T .

  is finite, then xA, "y is a BQO, and xP pAq , Ďy is a BQO.-xN, ďy is a BQO.-If xA i , ď i y is a BQO for i : 1, . . . , n then xA 1 ˆ. . . ˆAn , ĺ p y is a BQO. -If xA, ĺy is a BQO, then @ Flat Constraints. Fix a set V " tx 1 , . . . , x n u of variables. A flat constraint ψ over V if of the form A 0 c 1 A 1 ¨¨¨c m A m ,where c 1 , . . . , c m P N, and A 0 , A 2 , . . . , A m is a partitioning of V , i.e., V " A 0 Y A 1 Y ¨¨¨Y A m , A i ‰ H, and A i X A j " H if i ‰ j. In other words, a flat constraint is a word which alternatively contains sets of variables and natural numbers, starting and ending with a set of variables. The flat constraint ψ characterizes an infinite set ψ of vectors over N of length n, i.e., ψ Ď N n . More precisely, define h

	P pAq , ĺ P D	is a BQO.

ψ : t1, . . . , nu Þ Ñ t0, . . . , mu such that h ψ piq " k if x i P A k . v " xd 1 , . . . , d n y P ψ iff the following conditions are satisfied for all i, j : 1 ď i, j ď n:

The technical definition of BQOs is quite complicated and can be found in e.g.[START_REF] Abdulla | Better is better than well: On efficient verification of infinite-state systems[END_REF]. The actual definition is not needed for understanding the rest of the paper, and is therefore omitted here.


Somsak Vanit-Anunchai
email: somsav@sut.ac.th

Validating SCTP Simultaneous Open Procedure

Keywords: Coloured Petri Nets, Procedure-based, Verification Tags, Tie-Tags, COOKIE ECHO

The Stream Control Transmission Protocol (SCTP) is a reliable unicast transport protocol originally specified by the Internet Engineering Task Force (IETF) in RFC 2960. After years of implementing and testing, defects and errors in RFC 2960 were reported and later fixed in RFC 4460. Incorporating those suggested fixes, IETF revised the SCTP specification and published RFC 4960, which replaces RFC 2960. Despite of being the revised specification, the descriptions of the simultaneous open and the restart procedures are still unclear and difficult to understand. To clarify this informal specification and gain insights, we formally model and analyse the association management using Coloured Petri Nets. In particular this paper focuses on the Tie-Tag operation and the simultaneous open procedure operating over the simplest channels, First In First Out (FIFO) with no loss. Our analysis reveals errors in which both sides are in ESTABLISHED but the verification tags in both Transmission Control Blocks do not match.

Introduction

The Stream Control Transmission Protocol (SCTP), RFC 4960 [START_REF] Ed | Stream Control Transmission Protocol (SCTP), RFC4960[END_REF] is a unicast connection oriented transport protocol providing an error-free reliable flow of data between a client and a server. Originally it was designed by the Signalling Transport working group for transporting telephony signalling messages over UDP. Foreseeing its significance and great potential to become a major transport protocol, IETF decided to operate SCTP over IP instead.

After several years of implementation and testing, fifty-two defects in the original specification (RFC 2960) and solutions were discussed in RFC 4460 [START_REF] Stewart | Stream Control Transmission Protocol (SCTP) Specification Errata and Issues[END_REF]. The IETF has published a revised version of the SCTP informal specification, RFC4960 [START_REF] Ed | Stream Control Transmission Protocol (SCTP), RFC4960[END_REF], in September 2007, and RFC 2960 has become obsolete. Despite many years of implementing and testing SCTP, it is still important to have a proper formal model and to perform formal analysis of SCTP association management, especially when SCTP is designed for reliable data transfer such as signalling in Public Switching Telephone Networks. Previously in [START_REF] Vanit-Anunchai | Toward Formal Modelling and Analysis of SCTP Connection Management[END_REF] we focused on modelling the typical procedure of SCTP association management. This paper places emphasis on the exception handling procedure (handling an unexpected packet) which is more complex. Analysis of a formal model in [START_REF] Vanit-Anunchai | Toward Formal Modelling and Analysis of SCTP Connection Management[END_REF] illustrated that SCTP simultaneous open procedure in RFC 4960 could fall into an undesired final state in which both sides are in ESTABLISHED with mismatched VTAGs. However, it is arguable that these errors could happen only if a packet is reordered and delayed too long so that these defects are unlikely to occur. This paper discovers an error when SCTP operates over First in First out (FIFO) channel without losses. Thus, this error is more likely to occur than those errors previously found.

This paper is organised as follows. Section 2 provides an overview of SCTP association set up. Section 3 discusses the related work and contributions. A brief description of the CPN model of SCTP association management is given in Section 4. Section 5 presents the analysis results and a discussion of terminal markings. Section 6 presents conclusions and future work.

Overview of Stream Control Transmission Protocol

SCTP Packet Format

Figure 1 (a) shows an SCTP packet comprising a common header and one or more chunks. The SCTP header contains 16 bit source and destination port numbers, a 32 bit verification tag (VTAG) and a 32 bit checksum. The VTAG is used to protect an association from blind attacks. Each end point keeps two values of VTAG: "local VTAG" and "peer's VTAG". "local VTAG" sometimes is called "My VTAG". In general, any received packets containing a VTAG differing from "local VTAG" will be discarded. On the other hand, sent packets will carry a VTAG equal to "peer's VTAG". These tag values are randomly selected at initialization and exchanged between the end points during association set up.

A Chunk is an information unit. According to RFC 4960, there are 12 different control chunks but only one data chunk. The control chunks are Init1 , InitAck, SACK, Heartbeat, HeartbeatAck, Abort, Shutdown, ShutdownAck, Error, CookieEcho, CookieAck and ShutdownComplete. Control chunks are used to setup and shutdown the association, selectively acknowledge, report error messages, monitor reachability of the peer, etc. Association setup uses a four-way handshake comprising four control chunks: Init; InitAck; CookieEcho and CookieAck. Graceful closing uses a three-way handshakes comprising three control chunks: the Shutdown; ShutdownAck and ShutdownComplete chunks. The Data transfer phase involves Data and SACK (Selective Acknowledgement) chunks. Further detail of the structure of chunks can be found in [START_REF] Ed | Stream Control Transmission Protocol (SCTP), RFC4960[END_REF].

SCTP Association Establishment Procedure

Normal Association Establishment Figure 1 (b) shows the state diagram when SCTP sets up the association. Figure 2 shows a typical procedure of association establishment. An association between two nodes, A and Z, is initiated by an SCTP user on node "A" issuing an "ASSOCIATE" command. After receiving the "ASSOCIATE" primitive, node A sends an SCTP packet with (VTAG) equal to zero. This SCTP packet contains only an Init chunk with an initial tag to specify the VTAG of returning packets. Handling Unexpected CookieEcho Chunks This procedure specified in RFC 4960 is unclear and subtle. With reference to Table 2 in RFC 4960 (Fig. 3), VTAGs and Tie-Tags are compared to identify which action SCTP shall take. If the conditions in Fig. 3 are not met, SCTP silently discards the received CookieEcho chunk. However Section 5.2 of RFC 2960 and of RFC 4960 define Tie-Tags differently.

According to RFC 2960, Tie-Tags are stored in a state Cookie. They are copies of VTAGs from the existing TCB (local VTAG and peer's VTAG). These Tie-Tags are created when SCTP creates InitAck. Using the Tie-Tags in the restart procedure (Section 5.2.4.1 of RFC 4960), a newly restarting association can be tied to the original association without shutting down and starting a new association. The first two columns of Fig. 3 compare a pair of VTAGs in Cookie with a pair of VTAGs in existing TCB. The third and fourth columns of Fig. 3 compare a pair of Tie-Tags in Cookie with a pair of VTAGs in existing TCB. 2In order not to reveal the true VTAGs of the existing association, RFC 4960 defines Tie-Tags as two 32-bit random numbers or 64-bit nonce. They are stored in both the state cookie and TCB. When we consider the third and fourth columns of Fig. 3, it is incorrect to compare 64-bit nonce with VTAGs. We should compare a pair of Tie-Tags (64-bit nonce) in Cookie with a pair of Tie-Tags (64-bit nonce) in existing TCB instead. 3Each row in Fig. 3 identifies the SCTP's action as follows: -----------+------------+---------------+--------------+------------- -----------+------------+---------------+--------------+------------- -----------+------------+---------------+--------------+------------- -----------+------------+---------------+--------------+------------- -----------+------------+---------------+--------------+-------------

+------------+------------+---------------+--------------+-------------+ | Local Tag | Peer's Tag | Local-Tie-Tag |Peer's-Tie-Tag| Action/ | | | | | | Description | +-
+ | X | X | M | M | (A) | +-
+ | M | X | A | A | (B) | +-
+ | M | 0 | A | A | (B) | +-
+ | X | M | 0 | 0 | (C) | +-
+ | M | M | A | A | (D) | +======================================================================+ |
Table 2: Handling of a COOKIE ECHO when a TCB Exists | +======================================================================+ Legend: X -Tag does not match the existing TCB. M -Tag matches the existing TCB. 0 -No Tie-Tag in cookie (unknown). A -All cases, i.e., M, X, or 0. Note: For any case not shown in Table 2, the cookie should be silently discarded. 2 in RFC 4960 from [START_REF] Ed | Stream Control Transmission Protocol (SCTP), RFC4960[END_REF].

Fig. 3. Table

-Action A is the restart scenario when the other side crashes and starts up in CLOSED. SCTP shall continue the association by replacing the existing VTAGs with the ones in Cookie and sending a CookieAck.

-Action B is the simultaneous open scenario when both sides attempt to start an association at about the same time. SCTP shall enter the ESTAB-LISHED state, update its peers VTAG from Cookie. and then send a Cook-ieAck.

-Action C is when the Cookie is so delayed that SCTP has already sent an Init, received an InitAck and then sent a CookieEcho. The delayed Cookie arrives after the CookieEcho is sent. In this case the delayed Cookie is silently discarded.

-Action D is when both local and peer's VTAG in both Cookie and TCB are matched, SCTP shall enter the ESTABLISHED state and reply with Cook-ieAck.

One subtle ambiguity is the meaning of the zero values in Fig. 3. The values of Tie-Tags are set to zero indicating that no previous TCB existed. Action C requires the conditions that the values of Tie-Tags in the received cookie are zero. The value of peer's tag in TCB can be zero or unknown only when SCTP endpoint is in the COOKIE WAIT state. It implies that action B in the third row of Fig. 3 occurs when SCTP endpoint is in COOKIE WAIT.

Handling Unexpected InitAck and CookieAck Chunks An unexpected

InitAck is simply discarded if SCTP is not in COOKIE WAIT. SCTP also discards the CookieAck if it is not in COOKIE ECHO.

Related Work

Modelling Approach

Coloured Petri Nets [START_REF] Jensen | Coloured Petri Nets: Modelling and Validation of Concurrent Systems[END_REF] are well known for modelling and analysing concurrent and complex systems including validating various transport protocols such as Wireless Application Protocol (WAP) [START_REF] Gordon | Verification of the WAP Transaction Layer uisng Coloured Petri Nets[END_REF], TCP [START_REF] Han | Formal Specification of the TCP Service and Verification of TCP Connection Management[END_REF], and Datagram Congestion Control Protocol (DCCP) [START_REF] Vanit-Anunchai | An Investigation of the Datagram Congestion Control Protocol's Connection Management and Synchronisation Procedures[END_REF]. Our model has been created and maintained using CPN Tools [START_REF]CPN Tools home[END_REF] which is a software package for the creation, editing, simulation and state space analysis of CPNs. It supports the hierarchical construction of CPN models [START_REF] Jensen | Coloured Petri Nets: Modelling and Validation of Concurrent Systems[END_REF], using constructs called substitution transitions. These transitions hide the details of subnets and allow further nesting of substitution transitions. This technique allows a complex specification to be managed as a series of hierarchically related pages.

According to [START_REF] Billington | Coloured Petri Net Modelling of an Evolving Internet Standard: the Datagram Congestion Control Protocol[END_REF], the hierarchical structure of the CPN model can be classified into three modelling styles: state-based; event-processing and procedurebased. Similar to state tables, the state-based style groups actions in the same state into a CPN page. ITU-T often describes their narrative specification based on the state tables. This approach has the advantage of readability and unspecified actions can be easily discovered during model construction. But its disadvantage comes from redundant specification of the same actions that are common across different states. Hence the event-processing style folds the similar actions across different states into a transition. An example of specification that uses event-processing style is RFC 793 [START_REF] Postel | Transmission Control Protocol (TCP)[END_REF] Transmission Control Protocol (TCP). While the event processing style makes the CPN model smaller and easier to maintain, it has some drawbacks with respect to readability. Thus [START_REF] Billington | Coloured Petri Net Modelling of an Evolving Internet Standard: the Datagram Congestion Control Protocol[END_REF] proposed the procedure-based modelling style, which structures the CPN model according to the protocol's functionality. Actually suitability of the modelling style depends on how the narrative specification is written. As long as the model can be read and understood easily alongside the narrative specification, it is a good modelling style. We notice that IETF's transport protocol specifications (TCP, SCTP and DCCP) are more suitable to the procedure-based style. During modelling SCTP association management [START_REF] Vanit-Anunchai | Toward Formal Modelling and Analysis of SCTP Connection Management[END_REF], we discovered that this procedure-based style has two merits. First, using a state-based or event processing style a CPN page contains actions that are scattered in different sections of RFC 4960. Illustrated in [START_REF] Vanit-Anunchai | Toward Formal Modelling and Analysis of SCTP Connection Management[END_REF], with the procedure-based style actions in each CPN page are confined to only a few sections in RFC 4960. Our SCTP-CPN model in [START_REF] Vanit-Anunchai | Toward Formal Modelling and Analysis of SCTP Connection Management[END_REF] is easy to read alongside RFC 4960. Second, the procedure-based CPN model comprises typical procedures (straight forward) and unexpected procedures (complex). Beginners can pay attention to the typical scenarios before getting into the complex procedures later.

Comparing to the SCTP-CPN Model by Others

Despite a lot of work on SCTP's security, performance and multi-homing, we have found only three works [START_REF] Martins | Modelagem e Análise Formal de algumas Funcionalidades de um Protocolo de Transporte Atrvés das Redes de Petri[END_REF][START_REF] Vanit-Anunchai | Toward Formal Modelling and Analysis of SCTP Connection Management[END_REF][START_REF] Wang | Modelling and Verification of SCTP Association Management Based on Coloured Petri Nets[END_REF] that use Coloured Petri Nets to model SCTP association management operating over reordering channels. The CPN model in [START_REF] Martins | Modelagem e Análise Formal de algumas Funcionalidades de um Protocolo de Transporte Atrvés das Redes de Petri[END_REF] followed the state-based style whereas [START_REF] Wang | Modelling and Verification of SCTP Association Management Based on Coloured Petri Nets[END_REF] used the event-processing style similar to [START_REF] Han | Formal Specification of the TCP Service and Verification of TCP Connection Management[END_REF]. Our CPN model in [START_REF] Vanit-Anunchai | Toward Formal Modelling and Analysis of SCTP Connection Management[END_REF] was the procedure-based style following the approach proposed in [START_REF] Billington | Coloured Petri Net Modelling of an Evolving Internet Standard: the Datagram Congestion Control Protocol[END_REF]. The work in [START_REF] Vanit-Anunchai | Toward Formal Modelling and Analysis of SCTP Connection Management[END_REF] attempted to build the CPN models according to the revised specification, RFC 4960 while [START_REF] Martins | Modelagem e Análise Formal de algumas Funcionalidades de um Protocolo de Transporte Atrvés das Redes de Petri[END_REF][START_REF] Wang | Modelling and Verification of SCTP Association Management Based on Coloured Petri Nets[END_REF] used RFC 2960 which was obsolete. The CPN models in [START_REF] Martins | Modelagem e Análise Formal de algumas Funcionalidades de um Protocolo de Transporte Atrvés das Redes de Petri[END_REF][START_REF] Wang | Modelling and Verification of SCTP Association Management Based on Coloured Petri Nets[END_REF] were incomplete because [START_REF] Martins | Modelagem e Análise Formal de algumas Funcionalidades de um Protocolo de Transporte Atrvés das Redes de Petri[END_REF] did not include the procedure when SCTP nodes receive duplicated or unexpected messages and [START_REF] Wang | Modelling and Verification of SCTP Association Management Based on Coloured Petri Nets[END_REF] assumed no retransmission.

Contributions

The contribution of this paper is three-fold. First, while [START_REF] Vanit-Anunchai | Toward Formal Modelling and Analysis of SCTP Connection Management[END_REF] illustrates a CPN model of typical SCTP's association management, it leaves out the model of handling an unexpected CookieEcho chunk partly because it was not well understood at that time. In this paper, we attempt to finish up the CPN model of handing an unexpected CookieEcho chunk. Second, [START_REF] Vanit-Anunchai | Toward Formal Modelling and Analysis of SCTP Connection Management[END_REF] followed Fig. 5 (a restart example) of RFC 4960 and used the Tie-Tags as "old VTAGs" instead of 64-bit nonce. We compared the pair of Tie-Tags in Cookie with the pair of VTAG in existing TCB. Unfortunately, it turns out that Fig. 5 of RFC 4960 is incorrect 4 . Nevertheless, those errors uncovered in [START_REF] Vanit-Anunchai | Toward Formal Modelling and Analysis of SCTP Connection Management[END_REF] were not related to this mistake. This paper attempts to rectify the mistake in [START_REF] Vanit-Anunchai | Toward Formal Modelling and Analysis of SCTP Connection Management[END_REF]. We use Tie-Tags as 64-bit nonce and compare the pair of Tie-Tags in Cookie with the pair of Tie-Tags in existing TCB. This correction leads us to an undesired terminal marking in which both sides are in ESTABLISHED with a mismatched VTAG. This error scenario happens even when SCTP operates over FIFO channels without loss.

Third, after we have investigated the actions in Fig. 3 using state space analysis, we found two implementation flaws. Firstly, the implementor does not need to check the condition for action C because the Cookie will be discarded anyway if the conditions in Fig. 3 are not met. Secondly, the condition of action B in the third row (Fig. 3) has never been reached because the condition of action B in the second row is always satisfied before reaching the third row. We suggest the implementor checking the condition of the third row before checking the second row.

CPN Model of SCTP Association Management

Space limitation prevents us from including all CPN model pages. This paper focuses on handling an unexpected CookieEcho which is excluded from [START_REF] Vanit-Anunchai | Toward Formal Modelling and Analysis of SCTP Connection Management[END_REF]. However, for sake of completeness, we shall briefly describe the model starting from the top level toward the Unexpected CookieEcho and CookieAck Page. The rest of the model and its declarations can be found in [START_REF] Vanit-Anunchai | Toward Formal Modelling and Analysis of SCTP Connection Management[END_REF].

The top-level page of the SCTP-CPN model is illustrated in Fig. contain 32-bit random values of the initial verification tags. Places TCB A and TCB Z model Transmission Control Block represented by TCB. Both end points are connected via two channel places, CH A2Z and CH Z2A. We assume that during association set up and closing down a packet contains only one chunk represented by CHUNK. To form a FIFO queue the channel places are represented by a list of CHUNK (L CHUNK). The layout of the top level CPN page also reflects the well-known model of the n-layer in a layered protocol architecture. The application layer is placed on the top while the underlying medium layer is below the protocol entity. The substitution transitions, SCTP A and SCTP Z in Fig. 4 are linked to the second level page named SCTP Procedures (Fig. 5 (a)). We divide SCTP Procedures into five categories: normal events; unexpected events; retransmission; abort; and checking invalid tags. Substitution transition

Unexpected Init and InitAck Page

Figure 6 shows the CPN page dealing with the unexpected events of receiving Init and InitAck chunks in states other than CLOSED. Transitions RcvInit CK WAIT and RcvInit CK ECHOED model the actions according to Section 5.2.1 of RFC 4960 [START_REF] Ed | Stream Control Transmission Protocol (SCTP), RFC4960[END_REF] when an endpoint receives an Init chunk in the COOKIE WAIT or COOKIE ECHOED state. The difference between these actions is that the Tie-Tags from the COOKIE WAIT state are set to zeros but from COOKIE ECHOED, they are set to 64-bit nonce. Transitions Rcv InitOtherThan models the action according to Section 5.2.2 of RFC 4960 when the endpoints receive unexpected Init chunks in states other than CLOSED, COOKIE WAIT, COOKIE ECHOED and SHUTDOWN ACK SENT. The action is similar to that of transition RcvInit CK ECHOED but the "local VTAG" in the cookie and

Unexpected CookieEcho and CookieAck Page

Substitution transition CookieEcho CookieAck in Fig. 5 (b) links to the CPN page CookieEcho CookieAck (Fig. 7). The first four substitute transitions in Fig. 7 represent the actions when SCTP receives an unexpected CookieEcho chunk. The last transition models when SCTP receives CookieAck in states other than COOKIE ECHOED.

The Restart page Substitute transition Restart in Fig. 7 is linked to the Restart page shown in Fig. 8. This page models action A of Fig. 3. SCTP replaces its VTAGs with the VTAGs in the received Cookie and replies with CookieAck. If SCTP is in SHUTDOWN ACK SENT, it retransmits Shutdow-nAck.

The Simultaneous Open page Substitute transition Simultaneous Open in Fig. 7 is linked to the Simultaneous Open page shown in Fig. 9. This page models action B of Fig. 3. This page includes the actions when SCTP receives an unexpect CookieEcho in COOKIE WAIT. It also include the actions when the conditions in Fig. 3 are not met (Case E).

Analysis of SCTP-CPN Association Management Model

Initial configuration

We analyse our SCTP association management model using CPN Tools version 3.2.2 on an Intel(R)Core i5 2.67 GHz computer with 4GB RAM. The SCTP-CPN model is initialised by distributing initial tokens to the places shown in Fig. 4. No packet is in both channel places. Places ITAG A and ITAG Z store initial verification tags which are randomly generated. Place Tie Tag Nonce in Fig. 6 contains a pair of 32-bit random numbers for Tie-Tags.

Analysis Results

The analysis results of our SCTP simultaneous open CPN model are shown in Table 1. The 2-tuple in the first column is the maximum retransmissions allowed for Init and CookieEcho. The state space tool in CPN Tools provides the number of nodes, arcs and terminal markings. In all cases the number of nodes and arcs in the Strongly Connected Component (SCC) Graph are the same as the number of nodes and arcs in the state space. Thus, no livelocks are found. We classify the terminal markings into four categories based on the SCTP endpoint states.

TYPE-I terminal marking (CLOSED-CLOSED) is a desirable terminal marking when the association cannot be established thus both sides go to CLOSED state (No connection). TYPE-III and TYPE-IV terminal markings5 occur when one side is in ESTABLISHED while the other is in CLOSED. This can happen when the maximum number of retransmissions of the CookieEcho chunk is reached and the node enters CLOSED before CookieAck arrives. An example of this scenario is shown in Fig. 12. Although TYPE-III and TYPE-IV are unwanted, they are not harmful. This is because SCTP in CLOSED will report the failure to its user so that the user may decide to re-initiate the ASSOCIATE command. Thus the association can be restored as described in Fig. 5 of RFC 4960 (a restart example).

TYPE-II terminal markings should be desirable when both sides successfully establish the association. However when we check the verification tags stored in the TCBs, some terminal markings of TYPE-II are undesirable. "peer's VTAG" of node A must equal "local VTAG" of node Z and vice versa, otherwise received data packets will be discarded. In column TYPE-II, the number in parenthesis is the number of TYPE-II terminal markings in which verification tags between both TCBs do not match each other.

Figure 13 shows a message sequence diagram leading to an undesired deadlock for case (0,1). Node A starts initiating the first connection (solid line). After replying with InitAck (itag=78), node Z initiates the second connection (dot line) using a different initial tag (itag=47). Node Z in COOKIE WAIT keeps discarding the returned CookieEcho of the first connection (solid line) because the conditions in Fig. 3 (dot line) is always sent by node Z. After both sides are in ESTABLISHED, "peer's VTAG" of node A (47) is not equal to "local VTAG" of node Z (78). Node A can receive data but will not receive any acknowledgement from node Z. Node Z cannot receive any data from node A. Node Z cannot get into the restart procedure immediately because it is not in CLOSED yet. Node Z and node A have to wait for time-out before closing down the association.

Conclusions and Future Work

This paper has presented a Coloured Petri Nets model and analysis of SCTP simultaneous open procedure. While constructing the SCTP-CPN model, we identify the incorrect description of the Tie-Tags in RFC 4960. Our rigorous analysis shows that SCTP simultaneous open procedure, operating over FIFO channels with no loss, could fail into an undesired deadlock. Both sides in ES-TABLISHED could have mismatched verification tags in their TCBs. When the server is located behind middle-boxes such as fire wall or Network Address Translators (NAT), the transport protocols (UDP, TCP, DCCP and SCTP) normally use simultaneous open procedures. Nowadays NATs are widely deployed so that these defects in simultaneous open procedures should not be overlooked.

Formal analysing connection management of the other transport protocols: WAP [START_REF] Gordon | Verification of the WAP Transaction Layer uisng Coloured Petri Nets[END_REF], TCP [START_REF] Han | Formal Specification of the TCP Service and Verification of TCP Connection Management[END_REF] and DCCP [START_REF] Vanit-Anunchai | An Investigation of the Datagram Congestion Control Protocol's Connection Management and Synchronisation Procedures[END_REF], reveal no error when the protocols operate over FIFO channels with no loss. Usually errors could appear when the protocols operate over reordering and/or lossy channels. But the deadlock shown in Fig. 13 does not require any reordered or irregularly delayed packets. Although the odds of this particular scenario is low, the number of terminal markings Type II in Table 1 suggests that depending on the number of retransmitted Init Chunks, there are a large number of possible scenarios leading to the similar deadlock.

SCTP includes various capabilities, such as the restart and multi-homing procedures, aiming for high reliability or fault tolerance applications. When SCTP nodes enter the deadlock state, they have to wait for time-out before closing down the association. This delay degrades SCTP performance. As far as we are aware, this kind of errors has not been raised before. Given the above reasons and the enormous number of potential SCTP connections in the Internet, we consider that this problem could be a serious threat to SCTP applications especially when the high reliability is required.

In future, we are interested in modelling SCTP operating via Network Address Translators (NAT) with multi-homing functions.

Fig. 1 .

 1 Fig. 1. (a) SCTP packet format. (b) SCTP state diagram: association set up (redrawn from [8]).

Fig. 2 .

 2 Fig. 2. Typical message sequence charts association set up.

Fig. 4 .

 4 Fig. 4. The Top-level CPN page.

Fig. 5 .

 5 Fig. 5. (a) The SCTP Procedures page. (b) The Unexpected page.

Fig. 6 .

 6 Fig. 6. The Unexpected'Init InitAck page.

Fig. 7 .

 7 Fig. 7. The Unexpected'CookieEcho CookieAck page.

Fig. 8 .Fig. 9 .

 89 Fig. 8. The Restart page.

Fig. 10 .Fig. 11 .

 1011 Fig. 10. The Delayed Cookie page.

Fig. 13 .

 13 Figure13shows a message sequence diagram leading to an undesired deadlock for case (0,1). Node A starts initiating the first connection (solid line). After replying with InitAck (itag=78), node Z initiates the second connection (dot line) using a different initial tag (itag=47). Node Z in COOKIE WAIT keeps discarding the returned CookieEcho of the first connection (solid line) because the conditions in Fig.3are not met. After receiving InitAck of the second connection (dot line) and replying with CookieEcho, node Z stays in COOKIE ECHOED state. Owing to the condition of action C in Fig. 3, node Z in COOKIE ECHOED keeps discarding the returned CookieEcho of the first connection (solid line). When the timer expires or an intermittent fault occurs, node Z enters the CLOSED state. After node Z in CLOSED receives the Cook-ieEcho of the first connection (solid line), it restores ESTABLISHED state from the received cookie. After node A in COOKIE ECHOED, receives the Cook-ieEcho of the second connection (dot line), it enters the ESTABLISHED state (Action B ). Note that in Fig. 13 the CookieEcho of the first connection (solid line) is always sent by node A and the CookieEcho of the second connection

  Then node A enters the COOKIE WAIT state. On receiving the Init chunk, node Z replies with an InitAck chunk indicating that it is willing to communicate with node A. The response includes node Z's initial tag number and encrypted cookie contain-To acknowledge the InitAck, node A returns the cookie in a CookieEcho chunk and enters COOKIE ECHOED. When carrying an Init or InitAck chunk, the SCTP packet comprises only one chunk.

	When send-
	ing a CookieEcho chunk, the SCTP packet may enclose Data chunks after the
	CookieEcho chunk. On receiving a CookieEcho from node A, node Z creates its
	TCB from the received cookie, enters the ESTABLISHED state, replies with
	CookieAck and is ready for data transfer. After receiving CookieAck, node A
	enters ESTABLISHED indicating that the association is established. During
	data transfer, endpoint nodes A and Z may exchange Data and SACK chunks.
	Handling Unexpected Init Chunks The rules for handling duplicate or un-
	expected Init, InitAck, CookieEcho, and CookieAck chunks are specified in the
	Section 5.2 of RFC 4960. When SCTP receives an unexpected Init before the
	association established, SCTP composes a state Cookie using its local VTAG
	and the initial tag found in the unexpected Init. The Cookie is attached to the
	outbound InitAck. When an unexpected Init is received after the association es-
	tablished, SCTP composes a state Cookie using a new random number for local
	VTAG and the initial tag found in the unexpected Init. This implies that the
	Cookie contains state information of a new connection. When an unexpected
	Init is received in SHUTDOWN ACK SENT, SCTP replies with ShuntDow-
	nAck.

ing enough information to create node Z's Transmission Control Block (TCB). To prevent state exhaustion attacks node Z is still in CLOSED after replying with an InitAck.

Table 1 .

 1 State space analysis results.

	Case Nodes Arcs	Time		Terminal Markings
			(sec) (I)CL-CL (II)EST-EST (III)CL-EST (IV)EST-CL
	(0,0) 278	444	-	1	15(0)	8	8
	(0,1) 663	1,158	-	1	19(2)	9	9
	(0,2) 1,353 2,554 00:00:02	1	21(2)	10	10
	(0,3) 2,458 4,892 00:00:04	1	23(2)	11	11
	(0,4) 4,098 8,458 00:00:06	1	25(2)	12	12
	(0,5) 6,405 13,564 00:00:15	1	27(2)	13	13
	(0,6) 9,523 20,548 00:00:25	1	29(2)	14	14
	(1,0) 10,242 18,820 00:00:28	1	74(0)	37	37
	(0,7) 13,608 29,774 00:00:22	1	31(2)	15	15
	(0,8) 18,828 41,632 00:00:40	1	33(2)	16	16
	(1,1) 27,433 54,104 00:02:51	1	102(8)	47	47
	(1,2) 65,589 135,134 00:17:13	1	122(8)	57	57
	(1,3) 139,919 296,178 01:29:02	1	142(8)	67	67
	Node A				Node Z
	CLOSED					CLOSED
	[ASSOCIATE]
				Init (vtag=0, itag=Ax)
	COOKIE_WAIT
	(itag=Ax)
		InitAck (vtag=Ax, itag=Zx, CK[Zx.Ax])
	COOKIE_ECHOED
	(my vtag=Ax,			CookieEcho (vtag=Zx, CK([Zx.Ax])
	peer vtag =Zx)					CLOSED
	Time-out
	CLOSED		CookieAck (vtag=Ax)		ESTABLISHED
						(my vtag=Zx,

Fig. 12. A scenario leads to a terminal marking TYPE III (half open state).

Chunk names in the RFC are shown in all uppercase letters. To increase readability and distinguish them from SCTP States, the chunk names in this paper are given with only the first letters capitalized instead.

[START_REF] Vanit-Anunchai | Toward Formal Modelling and Analysis of SCTP Connection Management[END_REF] uses this comparison which is incorrect.

This paper uses this comparison.

See Transport Area Discussion Archive http://www.ietf.org/mail-archive/web/tsvwg/current/msg08603.html.

TYPE-III: node A terminates in CLOSED but node Z in ESTABLISHED. TYPE-IV: node A terminates in ESTABLISHED but node Z in CLOSED.

Acknowledgments This work is supported by Research Grant from the Thai Network Information Center Foundation and the Thailand Research Fund. The author is thankful to Jonathan Billington, Guy Gallasch and the anonymous reviewers. Their constructive feedback has helped the author improve the quality of this paper.

⋆ Supported by the the Thai Network Information Center Foundation and the Thailand Research Fund Contract no.TRG 5380023.


Félix Fernandez-Alonso

F Javier Bermejo

Carlos Cabrillo

Raouf O Loutfy

Vincent Leon

Marie-Louise Saboungi

Nature of the bound states of molecular hydrogen in carbon nanohorns

The effects of confining molecular hydrogen within carbon nanohorns are studied via high-resolution quasielastic and inelastic neutron spectroscopies. Both sets of data are remarkably different from those obtained in bulk samples in the liquid and crystalline states. At temperatures where bulk hydrogen is liquid, the spectra of the confined sample show an elastic component indicating a significant proportion of immobile molecules as well as distinctly narrower quasielastic line widths and a strong distortion of the line shape of the para→ortho rotational transition. The results show that hydrogen interacts far more strongly with such carbonous structures than it does to carbon nanotubes, suggesting that nanohorns and related nanostructures may offer significantly better prospects as light-weight media for hydrogen storage applications.

INTRODUCTION

After a rather optimistic start [1], the usefulness of carbon-based nanostructured materials (mostly in the form of multi-, MWNT, or single-walled, SWNT, nanotubes) as viable hydrogen storage media remains questionable. While early work [1] reported values largely in excess of the US-DOE target of 6.5 %, most subsequent studies could not verify the promising prospects referred to in Ref. [1]. The difficulty in reproducing such measurements has usually been attributed to problems in preparing SWNT or MWNT samples of high enough purity [2]. One study [3] has shown that molecular hydrogen (H 2 ) loaded into SWNTs at relatively high pressures (~100 bar) behaves as free H 2 , as attested by the absence of any significant change in the line profile of the para→ortho rotational transition, while another investigation [4] reports a rather different behavior. Moreover, H 2 loaded into carbon nanotubes at low temperatures does not bind firmly to the carbonous matrix and most of it evaporates once the sample is brought back to room temperature. This latter fact severely limits the potential applications of carbon nanotubes since any useful material must be able to release adsorbed H 2 both under controlled conditions and mild thermal treatments.

Single-walled carbon nanohorns (SWNH) consist of graphitic structures formed out of a single-walled graphene sheet with an average size of 2-3 nm. They adopt a horn-like shape and aggregate to form flower-like structures with sizes of about 80-100 nm. These nanostructures exhibit very large surface areas approaching 1500 m 2 g -1 [5] and are therefore attractive candidates for gas and liquid storage. Moreover, no metal catalyst is required for their synthesis thus enabling low-cost, large-scale production of high-purity samples.

Our interest in these materials stems from previous studies [8] where H 2 adsorption isotherms suggested a higher adsorbate density than that of the liquid at 20 K, with values approaching those of solid H 2 near its triple point (T = 13.83 K). This remarkable solidlike behavior was attributed to strong quantum effects [8], a conjecture later confirmed by detailed quantum simulations [9]. More recently, Tanaka et al. [10] have reported isosteric heats of adsorption for H 2 on SWNHs nearly three times as large as those on SWNTs, corresponding to H 2 binding energies as high as 100-120 meV. This increase in H 2 binding energy was attributed to strong solid-fluid interactions at the conical tips. Weaker H 2 adsorption was also observed away from the SWNH tips, with an interaction very similar to what has been found for SWNTs. In addition, preliminary results on H 2 adsorption in SWNHs [6] have shown that the para→ortho rotational line shape is significantly distorted from what is observed in SWNT and bulk H 2 samples. Also, thermal cycling from 10 K to 290 K and back to 10 K recovers a spectrum close to that measured after the initial low-temperature loading, indicating that most H 2 remains firmly attached to these carbon nanostructures. In the present Letter, high-resolution neutron spectroscopy is utilized to gain unique microscopic insight on the nature of H 2 adsorption on SWNHs.

II.

RESULTS AND DISCUSSION

Quasielastic (QENS) and inelastic (INS) neutron scattering are powerful probes of the dynamics and bonding of molecules in condensed matter [11]. Here we report on QENS and INS experiments of H 2 physisorbed on SWNHs. Our aim is to probe the bound states of H 2 in these novel carbon nanostructures via an analysis of the dependence of the QENS line widths and intensities on wave vector and temperature. Deviations of the para→ortho INS rotational line shape from free-rotor behavior provide additional insight on the strength and angular character of the interactions between H 2 and the SWNH surface.

SWNH samples were obtained from MER Corporation (Tucson, Arizona, USA). The IRIS backscattering spectrometer at ISIS represents an optimal choice for these experiments as it can provide high-resolution QENS and INS data [12]. The instrument configuration was set to the 002 reflection from cooled pyrolytic graphite with a beryllium filter to prevent contamination from higher-order reflections. QENS measurements covering an energy transfer range of -0.2 -1.0 meV with an energy resolution of 8.8 μeV (HWHM) were carried out at T = 5, 15, and 25 K. INS spectra were recorded at T = 1.5 K over the energy-transfer range 6 -20 meV by using the same energy analyser and phasing the choppers to run in offset mode, providing an energy resolution of 75 μeV at energy transfers around the H 2 para→ortho rotational transition at 14.7 meV. For the adsorption experiments, normal H 2 (75% ortho, 25% para) was condensed at T = 25 K and P = 1 bar into an annular-geometry aluminum cell. In order to keep total scattering powers below the canonical value of 15 %, sample thicknesses of 0.25 mm and 1 mm were used for bulk and adsorbed H 2 , respectively.

Fig. 1 displays a comparison of QENS spectra for the bulk liquid (L) as well as H 2 adsorbed on SWNHs (H 2 NH). An obvious difference between the two sets of data is the strictly elastic component in H 2 NH, indicating the presence of species with highly reduced mobility at temperatures and pressures where bulk H 2 is liquid.

QENS spectra were first analysed with a model-free Bayesian algorithm that infers from the data the mini-mum number of spectral components needed to account for the experimental observations [13]. The results show that the spectra for L can be described adequately with a single Lorentzian component, whereas those for H 2 NH require an additional, resolution-broadened elastic line. The wave vector dependence and the intensity of the quasielastic components for both L and H 2 NH are displayed in Fig. 2.

QENS data were analysed further by recourse to a jump-diffusion model where the HWHM of the QENS width is given by where DT stands for the translational self-diffusion coefficient and τ = ħ/E 0 is a mean residence time. Our value for the self-diffusion coefficient of L, D T = 0.43±0.01 Å 2 ps -1 , compares favourably with 0.47 Å 2 ps -1 of Egelstaff et al. [START_REF] Egelstaff | An Introduction to the Liquid State[END_REF] and with a value of 0.43±0.09 Å 2 ps -1 obtained by constant-gradient spin-echo NMR [START_REF] O'reilly | [END_REF]. As shown in Fig 2, QENS intensities in L conform to the form factor of a freely rotating H 2 molecule given by [16] where j n stands for spherical Bessel functions and R e = 0.7416 Å is the internuclear separation in H 2 [START_REF] Huber | Molecular Spectra and Molecular Structure IV. Constants of Diatomic Molecules[END_REF]. The analysis of the QENS spectra for H 2 NH required an additional delta-function contribution with an intensity about four times that of the lorentzian component. The elastic line proves that a large fraction of molecules are immobile within the time window of the measurements (1 -75 ps), while the QENS line can be assigned to translational motions of the mobile fraction. The wave-vector dependence of the latter at T = 15 K and T = 25 K is shown in Fig 2 . The higher temperature is about 5 K above the boiling point of the liquid at a pressure of 1 bar and so what we are observing here corresponds to a fluid tightly bound to the SWNH matrix. Analysis of the QENS energy widths yields values for D T of 0.96±0.1 Å 2 ps -1 and 6.5±1.7 Å 2 ps -1 at T = 15 K and 25 K, respetively. Values for the characteristic energies E 0 of 0.13±0.01 meV and 0.55±0.045 meV at 15 K and 25 K, respectively, are to be compared with 3.38±0.27 meV for L at T = 15 K. These results show that the mobile fraction of H 2 undergoes jump motions that are some 2.3 times faster than those found in L at the same temperature, whereas the residence time increases by a factor of about 25 due to interaction with the carbon matrix. Corresponding estimates for the length of a diffusive step l =√6Dτ are 0.7±0.07 Å and 5.44±0.41 Å for L and H 2 NH at T =15 K, respectively, and 6.81±0.56 Å for H 2 NH at T = 25 K.

Further information about the bound H 2 fraction is provided by the elastic form factors. Results are presented in Fig 3. Such data may be parameterized using an equation similar to Eq. 2 with the inclusion of an extra multiplicative factor to read I elast (Q) = Irot(Q) •Icm(Q). The Debye-Waller factor I cm = exp(-< u 2 >Q 2 /3) is characterized by an effective mean-square amplitude < u 2 > describing motions of the H 2 center of mass. In the present description, it is the only free parameter, since the internuclear distance R e = 0.7416 Å has been fixed to its tabulated value. Least-squares fitting of the elastic intensity data to the above expression reveals an increase of the effective < u 2 > from 0.77±0.06 Å 2 at T = 5 K to 1.47±0.08 Å 2 at T = 25 K. The observed temperature dependence of < u 2 > may be further understood in terms of a harmonic oscillator with energy levels E n = ħω c (n + 1/2 ) and Bose population factors P n (T) = exp (-βE n )/∑n exp (-βEn) according to [START_REF] Lovesey | Theory of Neutron Scattering from Condensed Matter[END_REF] where < u 2 n > = (n + 1/2) ħ/Mω c , M is the mass of H 2 , ω c is a characteristic frequency of centre-of-mass vibration, and β = 1/k B T. From our lowest-temperature measure-ments at T = 5 K we obtain ω c = 1.36 meV. As shown in Fig. 3, calculation of the expected form factors at higher temperatures using this value of ω c provides a unifieddescription of the data.

The H 2 NH INS spectrum displays a severely distorted line shape suggestive of inhomogeneous broadening, as shown in Fig. 4. Moreover, the broad component is markedly asymmetric with a bias towards lower frequencies. This situation represents a stark departure from SWNTs, where H 2 spectra at T = 4.5 K display a single and narrow contribution centered at 14.5±0.1 meV indicative of free rotation [3]. These differences are also in agreement with the higher binding energies found by Tanaka et al. [10]. To analyze our results, we consider a Stark splitting of the para→ortho rotational transition. Physically, it could arise from the presence of electrostatic interactions between H 2 and the carbon matrix. To lowest order, this interaction potential takes the form V(Θ, Φ) = V 2 cos 2 Θ, where V 2 stands for the height of the potential barrier and Θ is the angle between the diatom axis and the field direction (e.g., the surface normal) [START_REF] Silvera | [END_REF]. Using this model, the para→ortho transition energies have been calculated as a function of barrier height by direct diagonalization of the Hamiltonian matrix in the free-rotor |JM> ≡ Y JM (Θ, Φ) basis, where Y JM (Θ, Φ) is a spherical harmonic, and a given |JM> state is characterized by a rotational energy E JM = B rot J(J + 1). Convergence of energy eigenvalues was ensured by using a basis-set size J ≥ 20. The results of these model calculations are shown in the inset of Fig. 4. The gas-phase value B rot = 7.35 meV [START_REF] Huber | Molecular Spectra and Molecular Structure IV. Constants of Diatomic Molecules[END_REF] has been assumed throughout the analysis. The three Zeeman sublevels of the ortho state split into two components corresponding to the M = ±1 (maximal) and 0 (minimal) projections of the total angular momentum along the quantization axis. In the limit of a small perturbation (e.g., V 2 /B rot → 0 ), both intensities I M and energy positions relative to the free-rotor energy ΔE M approach a constant ratio given by I M=±1 /I M=0 = ΔE M=0 /ΔE M=±1 = 2. By constraining our fitting procedures to obey these restrictions, it is possible to fit the observed INS spectrum as shown in Fig. 4. The unperturbed rotational transition gives rise to the narrow component centered at 14.68±0.01 meV with a resolution-limited HWHM of 0.07±0.01 meV. In addition, two broad satellites are centered at 14.51±0.03 meV and 15.02±0.04 meV with HWHMs of about 0.31 meV. The intensity ratio of the Stark-split component relative to the unperturbed line is roughly 3.3, that is, about 75 % of the molecules are interacting with the carbon lattice strongly enough to perturb their highfrequency internal rotation. This ratio agrees with the amount of immobile H 2 extracted from QENS data, further reinforcing the notion that the most energetically favourable SWNH adsorption sites lead to a solid-like H 2 phase characterized by a significant angular anisotropy in the interaction potential. The observed INS spectral splitting is about 0.5 meV, corresponding to a temperature of about 6 K and a hindering barrier in the meV range. Moreover, since most of the spectral intensity appears below the freerotor line, the preferred orientation of the H 2 molecular axis must be parallel to the SWNH surface.

Lacking detailed information on the phonon spectrum of SWNH, an assignment of the vibrational frequency ħω c ~ 1.3 meV must remain tentative. This frequency is certainly below the phonon spectrum of molecular hydrogen [START_REF] Manzhelii | Physics of Cryocrystals[END_REF] so it must be related to low-energy modes of the SWNH substrate. In spite of its relevance to explain our experimental findings quantitatively, we note that the role of carbon-substrate motions has been largely neglected in simulation work to date [7,9,10]. Also, since ħω c ~ V 2 , the coupling between internal (rotational) and center-of-mass (translational) degrees of freedom is likely to play an important role in dictating the precise nature of H 2 motions on the SWNH substrate. In this context, recent 13 C NMR relaxation data [START_REF] Imai | [END_REF] have identified two distinct processes with disparate relaxation times. On the basis of previous information on the electronic subsystem [22], these can be assigned to either fast processes occurring in SWNHs in close proximity to the surface of the bundles or to slow motions taking place inside the graphitic cores.

III. CONCLUSION

In summary, this Letter provides unambiguous experimental signatures of a strong interaction between H 2 and SWNHs. More importantly, the character of this interaction is quantitatively different from what is known for H 2 in SWNTs. Both the stochastic (i.e., mass diffusion) and vibrational dynamics of free and bound species are strongly altered due to their adsorption on the carbon substrate. The mobile fraction exhibits a remarkably higher mobility than in the weakly interacting bulk phase. The vibrations of the SWNH-H 2 complex also display large mean-square displacements, indicative of strong quantum effects that persist at temperatures well above the boiling point of the bulk liquid. Our results also explain findings from previous modeling and experimental studies reporting the presence of two kinds of preferential adsorption sites with significantly different mobilities [10].

AKNOWLEGMENTS

FIG. 2 :

 2 FIG. 2: Wave-vector dependence of the QENS widths and amplitudes (insets) for L (top) and H 2 NH. Solid lines are fits to these data as explained in the text.

We thank RBE Down and CM Goodway from the ISIS User Support Group for their expert assistance. FFA gratefully acknowledges financial support from the UK Science and Technology Facilities Council.