Raphaël Chane-Yack-Fa

Marc Frappier
email: marc.frappier@usherbrooke.ca

Amel Mammar

Alain Finkel

Parameterized Verification of Monotone Information Systems

Keywords: model checking, parameterized verification, process algebra, well-structured transition systems, well-quasi-ordering, coverability, information systems

In this paper, we study the information system verification problem as a parameterized verification one. Informations systems are modeled as multi-parameterized systems in a formal language based on the Algebraic State-Transition Diagrams (ASTD) notation. Then, we use the Well Structured Transition Systems (WSTS) theory to solve the coverability problem for an unbounded ASTD state space. Moreover, we define a new framework to prove the effective pred-basis condition of WSTSs, i.e. the computability of a base of predecessors for every states.

Introduction

Information Systems (IS) have been evolving for years now and the validation of such systems has become a prominent topic. An IS can be viewed as a complex system composed of a set of related entities and which can manage a substantial amount of data. They are used for various applications such as banking services, online sales or data warehouse [START_REF] Bernus | Handbook on Architectures of Information Systems[END_REF]. In some cases, they are critical systems and one must ensure that the system is reliable. Therefore, the verification of IS specifications is essential. Furthermore, in this paper, we will see IS as parameterized systems which model systems with an unbounded number of components. For instance, the specification of a library management system, which is an IS, may abstract the number of books which interact in the library, and thus can be represented by a parameterized system. The aim of this paper is to find suitable techniques to specify and verify ISs from the point of view of parameterized systems. Parameterized verification is a widely addressed topic in the literature [McM99, EK00, CTV06, Mey09, SK09b, SK09a, HSBR10, KKW10, AHH13, DSZ10, KS14] and we can explore the relation between parameterized systems and ISs. Among the characteristics of ISs, we can notice the multiplicity of entity types and the complex relationships between them. For example, in the library system we can model a book entity and a member entity together with a loan relationship. The number of instances of each entity is unbounded: that justifies the need for a parameterized specification. In general, an IS has more than one entity and thus Example of a library system multiple parameters. However, in most of the methods in the literature, parameterized verification is limited to some specific models like systems with only one parameter or without any relationship. We propose in this paper a method that handles systems with many parameters and relationships. To model ISs, we use an adapted fragment of the Algebraic State-Transition Diagram (ASTD) notation, proposed in [FGL + 08], which we call Parameterized ASTD (PASTD) and which can model many related entities. As for the verification we based our method on the Well-Structured Transition Systems (WSTS) framework [START_REF] Finkel | Well-structured transition systems everywhere![END_REF] which can verify monotone infinite systems equipped with a well-quasi-order.

In order to use the WSTS framework, we make some hypothesis on ISs that are essential to prove the monotony of the system and the termination of the verification procedure. First, we assume that the specification of an IS cannot synchronize an arbitrary number of processes as it would break the monotony condition, which states that a similar configuration with more entity instances must be able to fire a similar transition. Moreover, to ensure termination, we devise some structural conditions on the states. However, unlike [FS01, DSZ10, Mey09, KS14], we deal with those conditions separately as we describe a general semidecision procedure. This leads us to the definition of a new framework called Ranked Monotone Transition System (RMTS) which is useful to show the effectiveness condition of WSTS. As a result, we prove that PASTDs are RMTSs. This paper is structured as follows. Section 2 presents the ASTD notation and the PASTD fragment. In Section 3, we recall the WSTS theory and show how to apply it to PASTDs by determining adequate conditions. Section 4 presents the RMTS framework and proves that PASTDs are RMTSs. The related work is presented in Section 5 and Section 6 concludes.

A Visual Process Algebra

An Algebraic State-Transition Diagram (ASTD) [FGL + 08] is a graphical notation combining automata, statecharts [START_REF] Harel | Statecharts: a visual formalism for complex systems[END_REF] and process algebras to describe complex dynamic systems like information systems. ASTDs are closely related to process algebras like CSP [START_REF] Charles | Communicating sequential processes[END_REF], CCS [START_REF] Milner | Communication and Concurrency[END_REF], ACP [START_REF] Bergstra | Process algebra for synchronous communication[END_REF], LOTOS [START_REF] Bolognesi | Introduction to the ISO specification language LOTOS[END_REF] and EB 3 [START_REF] Frappier | EB 3 : an entity-based black-box specification method for information systems[END_REF]. Essentially, they are like a process algebra with hierarchical automata as elementary process expressions. Automata can be combined freely with process algebra operators. ASTDs have a structured operational semantics in the Plotkin style, which was first used by Milner for CCS and later on for LO-TOS and CSP [START_REF] Roscoe | The Theory and Practice of Concurrency[END_REF]. They are recursively defined structures and include many types like automaton, synchronization, quantified choice and quantified interleaving.

ASTDs are useful to model information systems as they provide a concise, visual and formal mechanism for specifying all the scenarios of an information system [FGL + 08]. For example, they make explicit the handling of instances of information system entities by using quantifications. Furthermore, the model has been used in [EJFG + 10] to specify access control and security policies.

For instance, an ASTD model of a library system is given in Figure 1. The system manages loans of books by members. Books and members are the entities of the library system. The ASTD on the top left corner, whose name is library, is a synchronization between two other ASTDs, which consist in a quantified interleaving on the set T m of members for the the process member, and a quantified interleaving on the set T b of books for the process book. The process book(b) is described by the ASTD on the bottom right corner. A book is acquired by the library. It can be discarded if it is not lent. If acquired, a book b can "choose" a member m to run the process loan(b, m). The member process is similar except that a member m runs the loan(b, m) process for every book.

Parameterized ASTD

In this paper, we restrict ourselves to a fragment of the ASTD language. The graphical and textual notation of the original ASTDs are detailed in [START_REF] Frappier | Algebraic state transition diagrams[END_REF].

Let us denote a labeled tree by an expression thanks to the grammar T ree ::= N ode | N ode[T ree, . . . , T ree].

Definition 1 (ASTD expression). ASTD expressions are defined inductively by the following grammar:

F ::= A (automaton) | F || ∆ F (synchronization) | | x∈T F (quantified choice) | ||| x∈T F (quantified interleaving)
where:

• A is an Automaton ASTD (Q, Σ, δ, q 0 , Q f ) such that Q is a finite set of states where for each q ∈ Q, q is either an elementary state or a composite state, i.e. another ASTD expression, Σ a set of labels, δ a labeled transition relation, q 0 ∈ Q an initial state, Q f ⊆ Q a set of final states; the transition relation δ is given by a set of tuples (q 1 , q 2 , σ, f inal?), where q 1 , q 2 ∈ Q, σ ∈ Σ is an event and f inal? is a boolean denoting a transition that can be fired only from a final state (represented by a big dot at the origin of the arrow); an event is noted l(v 1 , . . . , v n ) where l is the event label, and v i are event parameters; function α extracts the label of an event: α(l(v 1 , . . . , v n )) = l; • F || ∆ F denotes a Synchronization between two component ASTDs running concurrently by executing events, whose labels are in ∆, at the same time and interleaving the other events; if ∆ is empty we denote the operator by ||| and if ∆ is omitted, the processes synchronize on the set of shared labels; • a Quantified Choice ASTD | x∈T F allows us to pick a value v from a finite set T and execute its component ASTD F, where every occurrence of the variable x is replaced by the value v; • a Quantified Interleaving ASTD ||| x∈T F allows us to execute as many interleaving instances of F as the number of values in T , where each instance is executed such that x is replaced by the corresponding value.

In the following, we introduce the following tree-like notation, which is easier to manipulate:

F ::= A[q 1 [F'], . . . , q k [F']] (one subtree for each state q i ∈ Q) | || ∆ [F, F] | | x∈T [F] | ||| x∈T [F] F' ::= F | ǫ
Note that ǫ is used to create elementary automaton states. Figure 2 shows the tree notation of the ASTD of Figure 1, where A member , A book and A loan are the automata for member, book and loan processes respectively.

In this fragment of the ASTD language, we make two notable modifications from the original definition. First, we do not allow recursion, so that an ASTD specification is a tree-like structure. Moreover, we do not allow quantified synchronizations and we weaken the quantified interleaving ASTD by allowing the process to be in a final state if one of the sub-processes is in a final state, i.e. there is no final synchronization between all interleaving processes (see Definition 23 of Appendix A). Indeed, the property of monotony, that we will explain in Section 3.2, is easier to obtain without quantified synchronizations.

The quantified operators (interleaving and choice) allow us to model replication of processes and interactions

|| ||| m∈Tm ||| b∈T b A member A book A loan M 0 M 1 L0 L1 B0 B1 | m∈Tm ||| b∈T b A loan L0 L1
Fig. 2. The tree representation of an ASTD between them. For instance, in the example of the library system, we use the quantified interleaving to model many replicated processes running concurrently. To model a library that works with any number of members and books, we can consider a more abstract specification that takes the sets of members and books as parameters. Indeed, we allow quantification sets to be variables in quantified choice and quantified interleaving. We call those variables the parameters of the system.

Definition 2 (Parameterized ASTD). A Parameterized ASTD (PASTD) is a triple (F, -→ T , -→ P ) where F is an ASTD expression, -→ T = (T 1 , . . . , T n ) is a vector of n variables, called parameters, and -→ P = (P 1 , . . . , P n ) is a vector of n sets of elements, called parameter domains. Each variable T i represents a finite subset of the possibly infinite set P i and appears in the expression of F as quantification set for quantified choice or quantified interleaving.

In a PASTD (F, -→ T , -→ P ), remark that the ASTD F does not correspond to a concrete transition system as it contains the variables -→ T . However, if we choose a sequence of sets U 1 ⊆ P 1 , . . . , U n ⊆ P n , the substitution of -→ T by -→ U in F does represent a transition system. Intuitively, a PASTD represents the union of all possible instantiations of the expression F , which may correspond to an infinite system. For instance, in the library system, we use two parameters T m and T b , with parameter domains P m = {m 1 , m 2 . . .} and P b = {b 1 , b 2 . . .}, respectively the sets of member and book identifiers. As a PASTD describes a dynamical system, for each PASTD, we can define a set of PASTD states. A state is given by a tree structure.

Definition 3 (ASTD state). A PASTD state is always associated with an ASTD expression with which it must be consistent. ASTD states are defined inductively by the following grammar:

S ::= (aut • , q) (automaton, elementary state q) | (aut • , q)[S] (automaton, composite state q) | || • [S, S] (synchronization) | |: • (quantified choice, value not chosen yet) | |: • [p[S]] (quantified choice, p is chosen) | |||: • [p 1 [S], . . . , p k [S]] (quantified interleaving on {p 1 , . . . , p k }, k ∈ N 1 )
Let s be a state of PASTD A. For s to be consistent with A, the following constraints must be satisfied:

(aut • ,M1) (aut • ,M0) (aut • ,B1) (aut • ,L1) (aut • ,L1) m 1 m 1 m 2 b 1 b 1 b 2 b 2 || • ||| :• ||| :• (aut • ,B0) | : • ||| :• (aut • ,L0) (library) (members)
(books) Fig. 3. A state of the library system

s = (aut • , q) : A = (Q, Σ, δ, q 0 , Q f ) ∧ q ∈ Q and q is elementary s = (aut • , q)[s ′ ] : A = (Q, Σ, δ, q 0 , Q f ) ∧ q ∈ Q and s ′ is consistent with the PASTD of composite state q s = || • [s ′ , s ′′ ] : A = A ′ || ∆ A ′′ and s ′ is consistent with A ′ and s ′′ is consistent with A ′′ s = |: • : A = | x∈T A ′ s = |: • [p[s ′ ]] : A = | x∈T A ′ ∧ p ∈ T and s ′ is consistent with A ′ s = |||: • [. . . , p[s ′ ], . . .] : A = ||| x∈T A ′ ∧ p ∈ T and s ′ is consistent with A ′
For a PASTD A, we denote by T A the set of all well-formed and consistent states of A.

An ASTD state is represented by a tree where each node is labeled either by the type of state or by a value from quantification sets. If a type of state includes a sub-state in its definition, then it is represented by a child node. Furthermore, we split up the nodes for quantifications so that the values appear in child nodes. Let us denote an undirected graph by a pair (V, E) such that V is a set of vertices and E a set of edges, where an edge is a pair of vertices. A labeled graph is a triple (V, E, λ) where (V, E) is a graph and λ : V → Λ a labeling function with Λ a set of labels. A labeled tree can be given by an expression T ree ::= N ode | N ode[T ree, . . . , T ree] or equivalently by a labeled acyclic connected graph (V, E, λ). In the following, we will sometimes represent an ASTD state by a graph (V, E, λ). We denote by Im(f ) the image of the function

f : X → Y , i.e. Im(f ) = {y ∈ Y | ∃x ∈ X • f (x) = y}.
Definition 4. For a PASTD A = (F, (T 1 , . . . , T n ), (P 1 , . . . , P n )) and a state s = (V, E, λ) ∈ T A , we denote by val(s) = (R 1 , . . . , R n ) the sets of elements appearing in the state s, i.e. R i = P i ∩ Im(λ) for all i ∈ 1..n.

For instance, consider the library system (F, (T m , T b ), (P m , P b )) of Figure 1. Let the state s consist of two members m 1 and m 2 and two books b 1 and b 2 , where the book b 2 is borrowed by the member m 1 as depicted in Figure 3. We have val(s) = ({m 1 , m 2 }, {b 1 , b 2 }). In this state, the member m 1 has joined the library and has borrowed the book b 2 . The member m 2 has not joined the library yet; similarly, the book b 1 has not been acquired yet; these two cases are represented by the initial state of the member and book automata, respectively. Remark that we allow an ASTD state to represent a more abstract state by omitting some branches of the quantified interleaving and by considering that the local configuration of some entities is unknown. See for example Figure 4 where the book b 1 is omitted in the quantified interleave of the state M 1 in member process m 1 . The operational semantics of PASTD consists of a set of inference rules defined inductively on the ASTD states. For a PASTD A, we denote the corresponding transition relation on T A by → and we obtain the transition system S A = (T A , →). Intuitively, || • makes a transition if both its sub-branches are able to do the transition on the same event. ||| :• can do the transition if one of its branches can and | :• if its sub-branch can. Finally, an automaton state fires a transition either by a classical automaton transition or within a sub-state.

(aut • ,M1)

(aut • ,M0) (aut • ,B1) (aut • ,L1) (aut • ,L1) m 1 m 1 m 2 b 1 b 2 b 2 || • ||| :• ||| :• (aut • ,B0) | : • ||| :• Fig. 4. An abstract state (aut • ,M1) (aut • ,M0) (aut • ,B1) (aut • ,L1) (aut • ,L1) m 1 m 1 m 2 b 1 b 2 b 2 || • ||| :• ||| :• (aut • ,B0) | : • ||| :• b 1 (aut • ,L0) → (aut • ,L0) (aut • ,L0) return(b 2 ) (aut • ,M1) (aut • ,M0) (aut • ,B1) m 1 m 1 m 2 b 1 b 2 b 2 || • ||| :• ||| :• (aut • ,B0) | : • ||| :• b 1 (aut • ,L0)
Fig. 5. A transition Figure 5 shows an example of transition in the library system where the member m 1 returns the book b 2 . The branches involved in the transition are depicted by bold strokes and the notable change in red. For a complete description of the operational semantics of ASTDs and PASTDs, see Appendix A or [START_REF] Frappier | Algebraic state transition diagrams[END_REF]. Note that the transition system of a PASTD A = (F, (T 1 , . . . , T n ), (P 1 , . . . , P n )) correspond to the infinite union of transition systems for ASTDs

F [(T 1 , . . . , T n ) := (R 1 , . . . , R n )] for all (R 1 , . . . , R n ) ⊂ (P 1 , . . . , P n ) (see [CYF17]).

Expressiveness of PASTD

Considering the previous extension of ASTDs with parameters, we can show that PASTDs are more expressive than some types of infinite systems like Petri Nets [START_REF] Lyle | Petri Net Theory and the Modeling of Systems[END_REF] or Vector Addition Systems with States (VASS) [START_REF] Hopcroft | On the reachability problem for 5-dimensional vector addition systems[END_REF]. More precisely, we remark that PASTDs can simulate VASSs with resets. An n-dimensional VASS with resets (RVASS) is a finite directed graph (V, E) with arcs labeled by vectors of integers or a reset symbol r, i.e. E ⊆ V × (Z ∪ {r}) n × V together with an initial vertex p i ∈ V and an initial natural vector u i ∈ N n . A configuration is a pair (p, u) ∈ V × N n . There is a transition between two configurations (p, (u 1 , .

a i = u ′ i -u i or a i = r ∧ u ′ i = 0.
We denote a transition system by a pair S = (Q, →), where Q is a set of states and → ⊆ Q × Q is the set of transitions between states. We write q → q ′ for (q, q ′ ) ∈ →, and q * -→ q ′ if either q = q ′ or there exists a finite sequence of transitions q → q 1 → q 2 → • • • → q ′ , called a path. We say that a transition system

c i ++ c i -- |||k ∈ T i ,aut reset(c i ) counter i ,aut Q0 i Q1 i
Fig. 6. ASTD model of a counter (Q, →) simulates another transition system (Q ′ , ֒→) if there exists an injection f :

Q ′ → Q such that for all q ′ 1 , q ′ 2 ∈ Q ′ such that q ′ 1 ֒→ q ′ 2 , we have f (q ′ 1 ) * -→ f (q ′ 2 ).
Intuitively, an RVASS consists of a finite set of counters {c 1 , . . . , c n } and of a graph called control graph. Each arc of the graph is labeled by an action that can change the values of the counters.

Proposition 1. PASTDs simulate RVASSs.

Proof. Let (V, E) be an RVASS. Let us construct a PASTD that simulates (V, E).

• First, let us model the counters. Each counter c i can be modeled by a two states automaton ASTD within a quantified interleaving ASTD as shown in Figure 6. There is a c i ++ action which increments the counter i, a c i -action which decrements it and a reset action reset(c i ) which sets c i to zero. To handle the reset action, we add a non-final loop on the interleaving operation. The value of c i is given by the number of processes in the local state Q1 i . For an unbounded counter, the quantification set is simply represented by a variable T i taking values in the subsets of N. • Second, the control graph can be represented by a simple automaton ASTD. According to the previous model of counters, we increase or decrease only one counter at the same time and only by one. Thus, we need to split some transitions into sequences of transitions by adding new control states. • Finally, we put together all counters thanks to interleaving PASTDs. Then, the global PASTD modeling the RVASS is represented by a synchronization PASTD between the control graph and the counters. Each time a counter c i is incremented by a c i ++ action, one instance of automaton in the quantified interleaving is non-deterministically chosen to move from Q0 i to Q1 i . Similarly, a c i -action decrements the counter c i only if there is an automaton in Q1 i to move to Q0 i . A reset(c i ) action will reinitialize all automaton to their initial states, i.e. Q0 i . Note that instances in quantified interleaving are not generated dynamically during transitions, but each sequence of states exists in the infinite union of instantiated systems. Thus, this construction works for unbounded counters.

A configuration of RVASS is represented by a set of states in the PASTD, which happens to be an equivalence class (as shown further in Section 3.3). Each transition of configuration of the RVASS is mimicked by a transition or a sequence of transitions in the resulting PASTD. A transition of states in the PASTD corresponds to a transition of equivalence classes (as will be shown in Section 4.2). As a consequence, PASTDs can simulate RVASSs. See an example of simulation in Figure 7.

This construction allows us to deduce some decidability results with regards to reachable configurations. For instance, the reachability problem is known to be undecidable for RVASSs [START_REF] Dufourd | Reset nets between decidability and undecidability[END_REF]. Since simulation preserves reachability of states, we can conclude that the reachability problem of equivalence classes is undecidable for PASTDs (see Section 4.2).

Well-Structured PASTD

Preliminaries

For a transition system S = (Q, →), we define P red(q) = {q ′ ∈ Q | q ′ → q} as the set of immediate predecessors of q and P red * (q) = {q ′ ∈ Q | q ′ * -→ q} as the set of all predecessors of q. A quasi-ordering (qo) is a reflexive and transitive binary relation ≤ on a set X; we also say that (X, ≤) is a qo. A partial ordering (po) is an antisymmetric qo. Note that for natural numbers, we use the same symbol ≤ and denote by (N, ≤) the natural order and by (N k , ≤) the product order. Let (X, ≤) be a po. For all s 1 , s 2 ∈ X, we say that s 3 ∈ X is the supremum (or sup) of s 1 and s 2 noted sup(s 1 , s 2 ) if s 3 is an upper bound of s 1 and s 2 (i.e. s 1 ≤ s 3 and s 2 ≤ s 3 ), and for all upper bounds s 4 ∈ X, we have s 3 ≤ s 4 . Let (X, ≤) be a qo. An upward-closed set is a subset Y ⊆ X such that if x ≤ y and x ∈ Y then y ∈ Y . For some x ∈ X, we write ↑x = {y ∈ X | x ≤ y} its upward-closure, and for some Y ⊆ X, ↑Y = x∈Y ↑x. A basis of an upward-closed subset Y ⊆ X is any set B such that Y = ↑B. We say that an upward-closed set Y has a finite basis if there exists some finite basis B of Y . A qo (X, ≤) is well-founded if there is no infinite sequence (x n ) n∈N over X such that x i+1 ≤ x i for every i ∈ N. It is a well-quasi-ordering (wqo) if every infinite sequence (x n ) n∈N over X contains an increasing pair, i.e. ∃i < j such that x i ≤ x j . If the wqo is a po, then it is called a well partial order (wpo). An antichain is a set in which each pair of different elements is incomparable.

Proposition 2 ([Hig52]

). If ≤ is a qo on X then the following are equivalent:

1. ≤ is a wqo; 2. Every infinite sequence (x n ) n∈N in X contains an infinite nondecreasing subsequence x n0 ≤ x n1 ≤ • • • with n 0 < n 1 < • • • ; 3.
≤ is well-founded and has no infinite antichain; 4. Every upward-closed subset U ⊆ X has a finite basis; 5. Every nondecreasing sequence

U 0 ⊆ U 1 ⊆ • • • ⊆ U i ⊆ • • • of upward-closed subsets U i of X eventually stabilizes.

Well-Structured Transition Systems

The theory of Well-Structured Transition Systems [Fin87, ACJT96, FS01] has been developed to unify and generalize some decidability results on termination, boundedness and coverability problems for infinite state systems equipped with a wqo on their states and a monotone transition relation with regards to this wqo. However, because of the monotony condition, wqos are typically hard to find for complex systems. Sometimes, we will focus on transition systems with weaker constraints, that is, monotone transition systems.

We consider Ordered Transition System (OTS) S = (Q, →, ≤) where (Q, →) is a transition system and Q is equipped with a quasi-ordering ≤. We are mainly interested here in the coverability problem for ordered transition systems, which consists, given an OTS S = (Q, →, ≤), a set of initial states I ⊆ Q and a state s ∈ Q, in deciding whether there exists a (possibly empty) run i * -→ s ′ such that s ≤ s ′ and i ∈ I. We says that s is coverable if there is such a run. Let us denote the coverability problem by the predicate cov(S, I, s). As shown in [START_REF] Parosh | General decidability theorems for infinitestate systems[END_REF], the coverability problem can be solved by computing the set P red * (↑s) of all predecessors of ↑s and then it suffices to check whether I ∩ P red * (↑s) is empty to verify whether s is coverable. To compute P red * (↑s), we can iteratively compute the sequence of sets of predecessors P red(↑s), P red 2 (↑s) = P red(P red(↑s)), . . . , P red n (↑s) . . . and we have P red * (↑s) = n∈N P red n (↑s). But this sequence, in general, does not necessarily stabilize. For monotone (ordered) transition systems, the set P red * (↑s) is upward-closed; and if moreover ≤ is a wqo, the set P red * (↑s) also have a finite basis. This opens the way to compute this finite basis which represents the set P red * (↑s).

Definition 5 (Monotone transition system [FS01]

). A monotone transition system (MTS) S = (Q, → , ≤) is an ordered transition system such that for all q 1 ≤ q ′ 1 and transition q 1 → q 2 , there exists a run

q ′ 1 * -→ q ′ 2 such that q 2 ≤ q ′ 2 In Proposition 3.1 of [FS01]
, the monotony of an ordered transition system is presented as the compatibility of ≤ with the transition relation →. Now if a monotone transition system S = (Q, →, ≤) has a wqo ≤, it is a WSTS.

Definition 6 (Well-Structured Transition System [FS01]). A Well-Structured Transition System S = (Q, →, ≤
) is a monotone transition system such that ≤ is a wqo on Q.

For example, Petri Nets are WSTSs if we take the inclusion of markings as the partial order. Indeed, the multiset inclusion is wpo and the transition system is monotone. Lossy Channel Systems [START_REF] Finkel | Decidability of the termination problem for completely specified protocols[END_REF] are another example of WSTS.

Monotone transition systems and WSTSs are both supposed to be effective: ≤ is decidable (i.e. there exists an algorithm determining whether a pair of elements belongs to ≤) and → is decidable.

The following lemma relies on the monotony condition.

Lemma 1 ([FS01]

). For a monotone transition system S = (Q, →, ≤) and q ∈ Q, we have ↑P red * (↑q) = P red * (↑q).

To make the iterative computation of the P red n (↑q), we need an OTS with effective pred-basis.

Definition 7 (Effective pred-basis [START_REF] Finkel | Well-structured transition systems everywhere![END_REF]). An OTS S = (Q, →, ≤) has effective pred-basis if there exists an algorithm accepting any state q ∈ Q and returning pb(q), a finite basis of ↑P red(↑q) (or predbasis).

For an OTS S = (Q, →, ≤) with effective pred-basis, and a finite subset of states F ⊆ Q, the backward coverability analysis consists in computing a sequence of finite sets of states

K 0 , K 1 . . . such that K 0 = F and K n+1 = K n ∪ pb(K n ).
We may verify that P red * (↑F ) = i∈N ↑K i .

Lemma 2 ([FS01]

). Let S = (Q, →, ≤) be a monotone transition system and s ∈ Q. If there exists m ∈ N such that ↑K m = ↑K m+1 , then ↑K m = P red * (↑s).

Effective pred-basis condition is sufficient to show that a finite basis for each ↑K i is computable according to the definition of the K i . Since we suppose that MTSs and WSTSs are effective, the qo ≤ is decidable, and then inclusion ↑K n ⊇ ↑K n+1 and equality ↑K n = ↑K n+1 can be tested. Moreover, if ≤ is a wqo, then (↑K i ) i∈N converges. Hence, the iterative computation of K n gives a procedure to the problem of reachability of ↑s (i.e., the coverability of s).

Theorem 1 ([FS01]

). For a WSTS S = (Q, →, ≤) with effective pred-basis and s ∈ Q, a finite basis B ⊆ Q of P red * (↑s) is computable. Hence, for any set of initial states I ⊆ Q, cov(S, I, s) is decidable, assuming the emptiness of I ∩ ↑B is decidable.

(aut • ,M1) (aut • ,M0) (aut • ,B1) (aut • ,L1) (aut • ,L1) m 1 m 2 b 1 b 1 b 2 b 2 || • ||| :• ||| :• (aut • ,B0) | : • ||| :• (aut • ,L0) m 2

Fig. 8. A state of the library system

Remark that if I is a finite set or an upward-closed set given by a finite basis, checking the emptiness of I ∩↑B is straightforward with a decidable ≤. But here we consider any I (because in PASTD the set of initial states is infinite and not upward-closed) and state the decidability of I ∩ ↑B = ∅ as a condition compared to [START_REF] Finkel | Well-structured transition systems everywhere![END_REF].

Monotone PASTD

In this section, we present a qo based on the subgraph relation such that PASTDs are monotone. To apply the theory of WSTSs to PASTDs, we need to define a qo on the set of states. But first, let us define an equivalence relation on states. We consider, from a reachability and coverability perspective, that the identifier of an entity instance has no importance and can always be replaced by another one; this has the advantage of reducing the computational complexity while allowing for a qo to be defined for a subset of PASTD. We consider that two states are equivalent if they are syntactically equivalent after renaming the entity identifiers using a permutation. We call permutation any bijection f :

X → X. A graph isomorphism from (V, E) to (V ′ , E ′ ) is a bijective function f : V → V ′ such that for all v 1 , v 2 ∈ V , {v 1 , v 2 } ∈ E iff {f (v 1 ), f (v 2 )} ∈ E ′ . Definition 8 (State equivalence). Let A = (F, - → T , - → P ) be a PASTD and s, s ′ ∈ T A such that s = (V, E, λ) and s ′ = (V ′ , E ′ , λ ′ ). We define s ∼ s ′ if there is a graph isomorphism φ from (V, E) to (V ′ , E ′ ) such that for each P i there is a permutation σ i on P i where for all v ∈ V , σ i (λ(v)) = λ ′ (φ(v)) if λ(v) ∈ P i .
Recall that for a PASTD A = (F, -→ T , -→ P ), the set of labels for the nodes of the tree representation of a state is given by the set {(aut • , q 1 ), . . . , (aut

• , q j ), || • , |: • , |||: • } ∪ i P i .
Definition 8 means that the entity instance identifiers are irrelevant for our purpose. Hence, we can always rename an identifier of P i by another one of the same P i if all occurrences are renamed similarly. For example, the state of Figure 3 is equivalent to the state of Figure 8 where the book b 1 is borrowed by the member m 2 . Take the permutations σ b and σ m on P b and P m respectively such that

σ b = id P b ⊕{b 1 → b 2 , b 2 → b 1 } and σ m = id Pm ⊕{m 1 → m 2 , m 2 → m 1 }
, where id X the identity on the set X and f ⊕ g the overriding of f :

X → Y by g : W → Y , i.e. (f ⊕ g)(x) = g(x) if x ∈ W and (f ⊕ g)(x) = f (x) otherwise.
To define a quasi-ordering on the set of states, we use the definition of induced subgraph.

(V, E) is called an induced subgraph of (V ′ , E ′ ) if V ⊆ V ′ and E = {{v 1 , v 2 } ∈ E ′ | v 1 , v 2 ∈ V }.
Let (Λ, ≤) be a qo set of labels. We define by ⊑ the extension of the induced subgraph relation (modulo isomorphism) to labeled graphs such that (V, E, λ) ⊑ (V ′ , E ′ , λ ′ ) if there exists f an isomorphism from (V, E) to an induced subgraph of (V ′ , E ′ ) such that λ(v) ≤ λ ′ (f (v)) for all v ∈ V . If no ordering on Λ is specified, we assume that ⊑ is defined according to the identity (Λ, id Λ ).

(aut • ,B1) (aut • ,B2) 3 1 2 3 (aut • ,B2) (aut • ,B2) 3 1 2 3 (aut • ,B2) (aut • ,B1) 4 (aut • ,B2) 4 (aut • ,C2) (aut • ,C2) ... 2 2 (aut • ,C2) ||| :• ||| :• | : • | : • | : • | : • | : • (aut • ,C1) (aut • ,C1) s 1 s 2 Fig. 9. An infinite antichain in (T A , )
Definition 9 (State quasi-ordering). Let A be a PASTD and s, s ′ ∈ T A . We define s s ′ iff there exists s ′′ ∼ s such that s ′′ ⊑ s ′ .

Intuitively, we have s s ′ if s is a subtree of s ′ modulo renaming. Furthermore, as we consider only well-formed states for a specific PASTD, subtree states can only be obtained by pruning branches from a quantified interleaving node. Proposition 3. PASTDs under are monotone transition systems.

Proof. The proof of monotony is similar to the one given in [START_REF] Chane-Yack-Fa | Verification of parameterized algebraic state transition diagrams[END_REF] for a superset of PASTD.

Bounded-PASTD

PASTDs under are not WSTSs because in general is not wqo.

Proposition 4. There is a PASTD such that is not wqo.

Proof. Figure 9 shows an example of infinite antichain for a PASTD. We construct the antichain similarly to the infinite antichain {abc, abbc, abbbc . . .} for the prefix ordering, or the H graphs for the subgraph ordering [START_REF] Ding | Subgraphs and well-quasi-ordering[END_REF]. Consider the state s 1 with 3 branches of interleaving, where val(s 1 ) = ({1, 2, 3}). The first branch of the interleaving is linked to the second one because they share the value 2. Likewise, the second branch is linked to the last one by the value 3. We construct s 2 with val(s 2 ) = ({1, 2, 3, 4}) by adding a new branch between the second and the last branch of s 1 and removing the direct link between them. Thus, we have s 1 s 2 . We construct the other states of the infinite antichain following the same principle. By Proposition 2, is not wqo.

We have not found yet a useful wqo for all PASTDs. Nonetheless, for some PASTDs, the set of states is wqo. For example, it is obviously the case for PASTDs without parameters, as the set of states is then finite. Some other weaker conditions can be used to get a wqo. We define in the following a class of PASTDs (aut • ,M1)

(aut • ,M0) (aut • ,B1) (aut • ,L1) (aut • ,L1) || • ||| :• ||| :• (aut • ,B0) | : • ||| :• (aut • ,L0) 1 1 2 2 0 0 0 0 0 0 0 m 1 m 1 m 2 b 1 b 1 b 2 b 2
Fig. 10. The graph representation of the state from Figure 3 satisfying the wqo property. But first, we propose another representation of the state. Indeed, we aim at using a wqo theorem from [START_REF] Ding | Subgraphs and well-quasi-ordering[END_REF] (see Theorem 2 in the sequel) and we need a graph structure with a wqo on the set of labels. However, we did not find any adequate wqo on the set of labels if we keep the same tree structure (that is also why we cannot use Kruskal's wqo theorem on trees [START_REF] Kruskal | Well-quasi-ordering, the tree theorem, and vazsonyi's conjecture[END_REF]). Hence, we use the following representation, where we replace labels denoting values e of P i by new nodes which are labeled by i, thus abstracting from the particular value of e. This little trick removes infinite sequences of incomparable elements without losing critical information.

Definition 10 (Graph of s). Let A = (F, -→ T , -→ P ) be a PASTD. For every s = (V, E, λ) ∈ T A with (R 1 , . . . , R n ) = val(s), let g(s) = (V ′ , E ′ , λ ′ ) be defined as follows:

• V ′ = V ∪ {(i, p) | i ∈ 1..n ∧ p ∈ R i } • E ′ = E ∪ {{(i, p), w} | i ∈ 1..n ∧ p ∈ R i ∧ w ∈ V ∧ λ(w) = p} • λ ′ = λ ⊕ {(i, p) → i | i ∈ 1..n ∧ p ∈ R i } ⊕ {w → 0 | ∃i ∈ 1..n • λ(w) ∈ R i }
Intuitively, the function g consists in replacing labels p from parameter sets R i by using new nodes of the form (i, p) and new edges between new nodes and nodes labeled from R i . Each new node (i, p) is connected with each node that has the same label in P i . Old labels p from R i are replaced with a default value 0. New nodes (i, p) are labeled with i. In this way, we obtain another representation of the state, which is still a graph but not a tree. But the codomain of the labeling λ ′ for the set of all possible states T A is now bounded as it does not include i P i anymore. Note that each equivalent state in the previous version has the same graph representation in the new version. An example is given in Figure 10 which shows the graph corresponding to the state of Figure 3. The red labels represent the new nodes and the blue ones are the old labels. The dotted lines are the new added edges. We denote by G A = g(T A ) the set of new graph representations for states and by Λ A the set of all labels in G A , i.e. the codomain of each labeling function.

Λ A = {(aut • , q 1 ), . . . , (aut • , q j ), || • , |: • , |||: • } ∪ i∈1..n {i} ∪ {0}
We introduce a new class of PASTD called Bounded-PASTD which satisfies the wqo property. In a graph (V, E), a path is a sequence of vertices

v 1 , v 2 , . . . , v n ∈ V such that {v i , v i+1 } ∈ E for all i ∈ 1..n -1. A simple path is a path v 1 , v 2 , . . . , v n ∈ V such that v i = v j
for all i = j. We denote by P k (Λ) the set of graphs P k whose vertices are labeled by the set Λ. Let P k the class of graphs without simple paths of length k.

Definition 11 (Bounded-PASTD). A PASTD

A is a Bounded-PASTD if there exists k ∈ N such that G A ⊆ P k (Λ A ).
Recall that ⊑ is the induced subgraph relation for labeled graphs with regards to a qo set of labels (Λ, ≤). When G A is only composed of graphs whose simple paths are bounded, we can refer to Ding's wqo theorem [START_REF] Ding | Subgraphs and well-quasi-ordering[END_REF] to show that (G A , ⊑) is a wqo, and thus to prove that Bounded-PASTDs are well-structured.

Theorem 2 (Ding's theorem [START_REF] Ding | Subgraphs and well-quasi-ordering[END_REF]). For k ∈ N, (P k (Λ), ⊑) is a wqo if (Λ, ≤) is a wqo.

We denote by T A /∼ the quotient set of T A with regards to the equivalence relation ∼ and we use the same symbol to denote the corresponding partial order between the equivalence classes. Let g : T A /∼ → G A the function such that g(s) = g(s) for all s ∈ T A , where s denotes the equivalence class of s. Consider the qo (G A , ⊑) using the identity (Λ A , id Λ A ) as the qo on the set of labels. Similarly to graph isomorphisms, we call isomorphism from a qo (X, ≤ X ) to a qo (Y, ≤ Y ) any bijective function f : X → Y such that for all

s 1 , s 2 ∈ X, s 1 ≤ X s 2 iff f (s 1 ) ≤ Y f (s 2 ). Such isomorphisms preserve wqo.
Lemma 3. For any PASTD A, g is an isomorphism from (T A /∼, ) to (G A , ⊑).

Proof. Let A = (F, {T 1 , . . . , T n }, {P 1 , . . . , P n }). Since G A is the image set of g, i.e. G A = g(T A ), we have that g is surjective. Thus, g is also surjective. Let us prove that there exists f :

G A → T A /∼ such that f • g is the identity on T A /∼. Let t = (V, E, λ) ∈ G A .
We define f (t) as the equivalence class of the state s = (V ′ , E ′ , λ ′ ) which is constructed as follows. For all i ∈ 1..n, let

V i = {v ∈ V | λ(v) = i} and λ i : V i → P i an arbitrary injection. Let V ′ = V \ i∈1..n V i and E ′ = E \ {{v, w} ∈ E | ∃i ∈ 1..n • w ∈ V i } and λ ′ = (λ ⊕ i∈1..n,w∈Vi {v → λ i (w) | {v, w} ∈ E})↾ V ′ ,
where f ↾ X is the domain restriction of the function f to X. It is easy to see that f (g(s)) = s for s ∈ T A /∼ by definition of g and f . Hence, the function g is also injective. Let x, y ∈ T A /∼. If x y then there are s 1 ∈ x, s 2 ∈ y such that s 1 ⊑ s 2 . By definition of g, g(s 1 ) ⊑ g(s 2 ). By the definition of g, g(x) = g(s 1 ) and g(y) = g(s 2 ). Hence g(x) ⊑ g(y). Now suppose that g(x) ⊑ g(y). Then, for all s 1 ∈ x and s 2 ∈ y, g(s 1 ) ⊑ g(s 2 ). Then, take s 1 ∈ x, s 2 ∈ y such that s 1 s 2 . Hence, x y. As Bounded-PASTDs are also monotone, we can conclude the following result.

Proposition 5. Bounded-PASTDs are WSTSs.

We will show in Section 4.2 that the coverability problem is decidable for Bounded-PASTDs.

Classes of Bounded-PASTD

Deciding if a PASTD is a Bounded-PASTD is an open problem, thus, in the following we propose two easily recognizable subclasses of Bounded-PASTD. For instance, a PASTD A = (F, -→ T , -→ P ) where each parameter T i appears only once in the expression F is called a 1-PASTD and a PASTD without nested quantifications is a Flat-PASTD. From an IS point of view, a 1-PASTD represents a system in which the entities can only be associated by weak entity relationships and a Flat-PASTD a system without relationships. Let us define formally these subclasses of PASTD. As illustrated in Figure 2, recall that for a PASTD A = (F, -→ T , -→ P ), where F is given in its tree notation (V, E, λ), the codomain of λ is the set of labels Λ

= i ({A i } ∪ j {q i,j }) ∪ i {|| ∆i } ∪ i∈1..n { | x∈Ti } ∪ i∈1..n { ||| x∈Ti },
where the A i are the different automaton ASTDs, q i,j the states of A i and || ∆i the synchronization ASTDs.

Definition 12 (1-PASTD). Let A = (F, {T 1 , . . . , T n }, {P 1 , . . . , P n }) be a PASTD with F = (V, E, λ). We call A a 1-PASTD if for all i ∈ 1..n, the set of nodes {v ∈

V | λ(v) ∈ { | x∈Ti , ||| x∈Ti }} is a singleton set. ... ... ... G s,3 G s,2 G s,1 g(s)
This level contains no quantification.

This level contains no quantification.

This level contains all quantifications.

Fig. 11. Node partition of a state

In a (labeled acyclic connected) graph (V, E, λ) that is also a tree, we denote by ch(v) the child nodes of v and by des(v) = ch + (v) its transitive closure, i.e. the sets of descendants of v. Similarly, we denote by pa(v) and anc(v) = pa + (v) the parent and ancestors of v respectively.

Definition 13 (Flat-PASTD).

Let A = (F, {T 1 , . . . , T n }, {P 1 , . . . , P n }) be a PASTD with F = (V, E, λ). Let V q = {v ∈ V | λ(v) ∈ i∈1..n { | x∈Ti , ||| x∈Ti }} (the quantified operator nodes). We call A a Flat-PASTD if for all v ∈ V q and all w ∈ des(v), λ(w) / ∈ i∈1..n { | x∈Ti , ||| x∈Ti }.
For instance, the PASTD simulating a VASS in Figure 7 is a Flat-PASTD as there is no nested quantified interleaving operators. It is also a 1-PASTD because T 1 and T 2 appear only in one quantified interleaving operator each.

Proposition 6. Any 1-PASTD is a Bounded-PASTD.

Proof. Let s ∈ T A such that s = (V, E, λ) and g(s) = (V ′ , E ′ , λ ′ ). It is easy to see that g(s) is a tree because every new node v ∈ V ′ \ V , which represents a value of a quantified node, is connected to only one other node. Moreover, the depth of s is bounded by the depth of F . Thus, every simple path in G A is bounded.

Now, let us prove that Flat-PASTDs are Bounded-PASTDs.

Let A = (F, - → T , - → P ) a PASTD, s = (V, E, λ) ∈ T A with (R 1 , . . . , R n ) = val(s) and g(s) = (V ′ , E ′ , λ ′ ). V can be decomposed into three disjoint sets V = V s,1 ∪ V s,2 ∪ V s,3 as follows: • V s,1 = {v ∈ V | λ(v) / ∈ {|: • , |||: • } ∧ λ(anc(v)) ∩ {|: • , |||: • } = ∅},
the nodes of the subtree containing the root of s and all descendants down to the first quantified operator;

• V s,2 = {v ∈ V | λ(v) ∈ {|: • , |||: • } ∪ i P i ∨ (λ(anc(v)) ∩ {|: • , |||: • } = ∅ ∧ λ(des(v)) ∩ i P i = ∅)
}, the nodes of subtrees whose root is a quantified operator and including all descendants down to the quantification values;

• V s,3 = V \ (V s,1 ∪ V s,2
), the remaining nodes.

Intuitively, as V s,2 is the only part containing values of quantification, then only the nodes of V s,2 have a different label through g in V ′ . V ′ can be decomposed into three disjoint sets

V ′ s,1 = V s,1 , V ′ s,2 = V s,2 ∪ i∈1.
.n,p∈Ri {(i, p)} and V ′ s,3 = V s,3 . We denote by G s,1 , G s,2 and G s,3 the subgraphs of s induced by V s,1 , V s,2 and V s,3 respectively and G ′ s,2 the subgraph of g(s) induced by V ′ s,2 . See Figure 11. Lemma 4. Let A be a PASTD. There exists k ∈ N such that for all s ∈ T A , G s,1 contains at most k nodes and G s,3 is composed of trees whose depth is at most k.

Proof.

As there is no quantified operator in V s,1 , then by the definition of the state structure, the number of nodes is bounded and depends on F only. Same reasoning for each tree in G s,3 .

Lemma 5. Let A be a PASTD. A is a Bounded-PASTD iff there exists k ∈ N such that for all s ∈ T A , G ′ s,2 ∈ P k (Λ A ). Proof. Direction =⇒ . By Definition 11, if A is a Bounded-PASTD, then there is k ∈ N such that for all s ∈ T A , we have g(s) ∈ P k (Λ A ). Thus, G ′ s,2 ∈ P k (Λ A ). Direction ⇐= . Let k 1 ∈ N such that for all s ∈ T A , we have G ′ s,2 ∈ P k1 (Λ A ). Let s = (V, E, λ) ∈ T A . Let us prove that there is k ∈ N such that g(s) ∈ P k (Λ A ). By Lemma 4, let k 2 ∈ N such that G s,1 contains at most k 2 nodes and G s,3 is composed of trees whose depth is at most k 2 . Let u = (v 1 , . . . , v m ) be a simple path in g(s)

with v i ∈ V for all i ∈ 1..m and m ∈ N its size. If u crosses only G s,1 , then m ≤ k 2 . If u crosses only G s,3 , then m ≤ 2 × k 2 , as there are only trees of depth ≤ k 2 in G s,3 . If u crosses only G ′ s,2 , then m ≤ k 1 .
A more general simple path u in g(s) can be decomposed into several segments u 1 , . . . , u j such that each segment crosses only one of the subgraphs G s,1 , G ′ s,2 or G s,3 . Typically, for a path having the most segments, remark that the first segment begins in G s,3 , then the next ones alternate between G ′ s,2 and (possibly) G s,1 and the final one ends back in G s,3 . The path can only alternate k 2 times between G ′ s,2 and G s,1 as G s,1 contains at most k 2 nodes. Thus,

m ≤ 2 × k 2 + k 1 + k 2 × (k 2 + k 1 ) + 2 × k 2 = k 2 (4 + k 1 + k 2 ) + k 1 . Let k ′ = k 2 (4 + k 1 + k 2 ) + k 1 . We have g(s) ∈ P k ′ (Λ A ). As k ′ is independent from s, g(s) ∈ P k ′ (Λ A ) for all s ∈ T A . Proposition 7. Any Flat-PASTD is a Bounded-PASTD. Proof. Let A = (F, {T 1 , . . . , T n }, {P 1 , . . . , P n }) a PASTD with F = (V F , E F , λ F ).
Let us prove that there is k ∈ N such that for all s ∈ T A , we have G ′ s,2 ∈ P k (Λ A ), which is equivalent to being a Bounded-PASTD thanks to Lemma 5. Let s ∈ T A and g(s) = (V, E, λ). Because A has no nested quantifications, there are only two types of nodes in

V ′ s,2 = W 1 ∪ W 2 , where W 1 = {v ∈ V | λ(v) ∈ {|: • , |||:
• }} the set of "quantified operator" nodes, and W 2 = {v ∈ V | λ(v) ∈ {0, 1, . . . , n}} the set of "parameters" nodes. Clearly, the longest simple path including only nodes from W 2 is of length 3, by construction of g(s). Moreover, remark that, without nested quantifications, the size of W 1 is bounded by a number k 1 that depends on the structure F only (W 1 contains at most one v ∈ V with λ(v) ∈ {|:

• , |||: • } for each v F ∈ V F such that λ F (v F ) ∈ i∈1..n { | x∈Ti , ||| x∈Ti })
. By a similar reasoning as in the previous lemma, a "maximal" simple path alternates between W 1 and W 2 and its length is bounded by k ′ = (1 + 3) × k 1 = 4 × k 1 . As k does not depend on s, G ′ s,2 ∈ P k ′ (Λ A ) for all s ∈ T A . As 1-PASTDs and Flat-PASTDs are Bounded-PASTDs, we can conclude that we have two easily recognizable classes of PASTD that are WSTSs.

Computation of pred-basis for PASTDs

To apply the backward analysis algorithm presented in Section 3.2 to PASTDs, we need to prove a last condition that is the effective pred-basis. By definition, the existence of pred-basis condition can be related to the wqo condition, because with a wqo any upward-closed set has a finite basis. However, we think that these two conditions should be independent from each other to have a better understanding of the algorithm. Thus, we propose in Section 4.1 a new framework which identifies a set of conditions proving the effective pred-basis without wqo. Then, we show in Section 4.2 how to use the framework on PASTDs, hence to solve the coverability problem.

Ranked Monotone Transition Systems

In this section, we describe a general method to prove the effective pred-basis in some infinite systems without the wqo condition. We will show first that without wqo and under some other conditions, there exists a finite basis of ↑P red(↑s). Then, we show that the finite pred-basis is computable with some effectivity hypothesis. In order to compute a pred-basis for s, a naive approach would be to compute the upward-closure of s and then the set of all predecessors. However, this procedure does not terminate when ↑s is infinite. In practice, for most interesting systems, there is no need to consider the entire set of upper states to compute a basis of

q 1 q 2 ≤ s 1 s 2 q 0 1 q 0 2 ∃ ∀ -→ -→ -→ ≤ ≤ ≤ Fig. 12
. Condition 4 of RMTS : the backward-downward monotony predecessors. Thus, we propose a method that determines which finite subset of ↑s is sufficient to compute a finite basis of ↑P red(↑s). To this end, we define a new class of transition systems called Ranked Monotone Transition Systems. Note that, to keep the definitions simple, we consider OTSs with partial ordering in the following. We will see in the next section how to apply the method to OTSs with quasi-ordering.

Definition 14 (Ranked MTS). A Ranked Monotone Transition System S = (Q, →, ≤, γ, c, d) is a monotone transition system (Q, →, ≤), where ≤ is a po, with a function γ : Q → N n and c, d ∈ N n s.t. :

1. γ is a monotone function and γ -1 (r) is finite for all r ∈ N n , 2. for all s 1 , s 2 , s 3 ∈ Q such that s 1 ≤ s 3 and s 2 ≤ s 3 , there exists s 4 ∈ Q such that s 1 ≤ s 4 , s 2 ≤ s 4 , s 4 ≤ s 3 and γ(s 4 ) ≤ γ(s 1 ) + γ(s 2 ), 3. for all s 1 → s 2 , there exists s ′ 1 ∈ Q such that s ′ 1 ≤ s 1 and s ′ 1 → s 2 and γ(s ′ 1 ) ≤ γ(s 2 ) + d, 4. S is backward-downward monotone (bdm): for each transition s 1 → s 2 , there is a transition q 1 → q 2 s.t.:

(a) q 2 ≤ s 2 , γ(q 2 ) ≤ c, and

(b) ∀q ′ 2 ∈ Q • q 2 ≤ q ′ 2 ≤ s 2 =⇒ ∃q ′ 1 ∈ Q • q ′ 1 → q ′ 2 ∧ q 1 ≤ q ′ 1 ≤ s 1 .
Let us give the intuition for each condition of Definition 14:

1. The function γ associates a vector of natural numbers called rank to each state of the system. Intuitively, the rank of a state represents its size and this size can be multidimensional. We can see the rank function as a way to split the partial ordering into several finite layers of states, each layer corresponding to a rank. This principle applies well to some ordered transition systems. In particular, parameterized systems can be naturally equipped with rank functions. Indeed, a rank of a state may correspond to the number of instances of each entity in the state. 2. Condition 2 demands that if s 1 and s 2 have an upper bound s 3 , then we can find a lesser one s 4 whose rank is bounded by the sum of the ranks of the two considered states. 3. To understand Condition 3, consider a parameterized system and suppose that the transition s 1 → s 2 is "destructive", that is some instances of entities are lost during the transition and γ(s 2 ) < γ(s 1 ). If it is a "reset transition" (i.e. the number of lost instances for similar transitions is unbounded), then there must exist a smaller configuration s ′ 1 ≤ s 1 whose rank is bounded by γ(s 2 ) + d and that can fire the transition. If the transition relation never decreases the rank by more than d, then the property is always satisfied. 4. The central property is Condition 4. It states that the kernel of a transition can be identified and is small. This kernel is the set of entity instances that change state in a transition (e.g., the book and member involved in a loan transition). For each transition we look for a smaller one that has the "same semantics" and such that there exist intermediate transitions. See Figure 12 for a graphical representation of the backward-downward monotony. The value c is an upper bound on the sizes of all minimal transitions in the system. Intuitively, for each transition we identify a smaller part that is essential to fire the transition while the rest remains stable. The definition ensures that the minimal transition is a good one by checking that every intermediate transition is also possible.

Definition 15 (Effective RMTS). An RMTS S = (Q, →, ≤, γ, c, d) is effective if → and ≤ are decidable and γ(q) and γ -1 (r) are both computable for all (q, r)

∈ Q × N n .
Example 1 (Petri Nets). Let N = (P, T, F ) be a Petri Net where P is a set of places, T a set of transitions and F : (P ×T ∪T ×P ) → N a multiset of arcs. A marking is a multiset of places, i.e. a mapping M : P → N.

We denote by S N = (Q, →, ⊆) the corresponding transition system with Q the set of markings and ⊆ the marking inclusion defined by

M 1 ⊆ M 2 if M 1 (p) ≤ M 2 (p) for all place p. Let γ : Q → N be a function such that γ(M ) = p∈P M (p). 1. Clearly, γ is monotone, i.e. M 1 ⊆ M 2 =⇒ γ(M 1 ) ≤ γ(M 2 ) and γ -1 (r) is finite for all r ∈ N because P is finite. 2. For all M 1 , M 2 , M 3 ∈ Q such that M 3 is an upper bound of M 1 and M 2 , sup(M 1 , M 2 ) ⊆ M 3 and γ(sup(M 1 , M 2 )) ≤ γ(M 1 ) + γ(M 2 ), because sup(M 1 , M 2 ) denotes max(M 1 (p), M 2 (p))
for each place p. 3. Let d ∈ N be the maximum number of tokens needed to fire a transition, then for all transitions M 1 → M 2 , we have γ(M 1 ) ≤ γ(M 2 ) + d. 4. Finally, take c = max(F ), i.e. the maximum token consumed or created by a transition. Then, the bdm condition is verified. Indeed, for all transition M 1 → M 2 fired by t ∈ T , we can always find a smaller one

M ′ 1 → M ′ 2 where for all p ∈ P , M ′ 1 (p) = F (p, t) and M ′ 2 (p) = F (t, p) such that Condition 4 is verified. Thus, (Q, →, ⊆, γ, c, d) is an RMTS.
Example 2 (Petri Net Extensions). Petri Nets with transfer arcs are RMTSs, considering the same function γ. Condition 3 is satisfied because the number of tokens lost during the transition is still bounded. The backward-downward monotony holds because a transfer arc is always possible for any smaller marking. The same holds for Petri Nets with reset arcs except that the number of tokens lost during a reset transition is not bounded but for any reset transition there is always a lesser transition that is bounded.

Example 3 (Lossy Channel Systems). Consider a Lossy Channel System S C with Q a set of control states, Σ an alphabet and c 1 , . . . , c n a set of FIFO channels. The system can send a message along a channel, receive one from a channel or lose one in a channel. Each message is represented by one letter of Σ. Hence, a transition can add or remove one letter in a channel at a time. We denote by ≤ the ordering between configurations from Q × Σ * n such that (q, w 1 , . . . , w n ) ≤ (q ′ , w ′ 1 , . . . , w ′ n ) if q = q ′ and w i ⊑ w ′ i for all i ≤ n, where ⊑ is the sub-word ordering. Take the function γ :

Q × Σ * n → N n such that γ(q, w 1 , . . . , w n ) = (|w 1 |, . . . , |w n |).
1. γ is monotone and γ -1 (r) is finite for all r ∈ N n as Q and Σ are finite. 2. Since |sup(w, w ′ )| ≤ |w|+|w ′ | for all w, w ′ ∈ Σ * , we have γ(sup(s, s ′ )) ≤ γ(s)+γ(s ′ ) for all s, s ′ ∈ Q×Σ * n .

Thus, the supremum satisfies Condition 2. 3. The size of a word in a channel can only increase or decrease by one, hence for every transition s → s ′ we have γ(s) ≤ γ(s ′ ) + (1, . . . , 1). 4. For each type of transition we have a minimal one satisfying the bdm condition. If it is a send action (q, w 1 , . . . , w i , . . . , w n ) → (q ′ , w 1 , . . . , w i .a, . . . , w n ), then take the smaller transition (q, ǫ, . . . , ǫ) → (q ′ , ǫ, . . . , a, . . . , ǫ). If it is a receive action (q, w 1 , . . . , a.w i , . . . , w n ) → (q ′ , w 1 , . . . , w i , . . . , w n ), then take (q, ǫ, . . . , a, . . . , ǫ) → (q ′ , ǫ, . . . , ǫ, . . . , ǫ). Finally, if it is a loss of message (q, w 1 , . . . , a.w i , . . . , w n ) → (q, w 1 , . . . , w i , . . . , w n ), then take (q, ǫ, . . . , a, . . . , ǫ) → (q, ǫ, . . . , ǫ, . . . , ǫ). Condition 4 is then verified for c = (1, . . . , 1).

Thus, (Q × Σ * n , →, ≤, γ, c, c) is an RMTS.

Nicely Sliceable WSTS (NSW) [START_REF] Bingham | Empirically efficient verification for a class of infinite-state systems[END_REF] share some similarities with RMTSs. They both use the same notion of partitioning of the state space and downward monotony. However, they rely on different assumptions and some of their requirements are unnecessary for our purpose. In [START_REF] Bingham | Empirically efficient verification for a class of infinite-state systems[END_REF], the authors propose an algorithm to compute the set of all predecessors P red * (↑s) and use the NSW framework in order to prove its correctness. That differs from our goal which is to give a complete method to prove the existence of pred-basis, that is not guaranteed without the wqo condition, and to compute it. Petri Nets, Broadcast Protocols, Lossy Channel Systems and Context-free grammars are examples of NSWs [START_REF] Bingham | Empirically efficient verification for a class of infinite-state systems[END_REF].

Definition 16 ([BH05]). A δ-NSW (Nicely Sliceable WSTS) is a WSTS S = (Q, →, ≤) such that 1. ≤ is discrete over Q, i.e.
(a) ∀q ∈ Q, ∃k ∈ N s.t. for any sequence q 0 ≤ • • • ≤ q l = q we have l ≤ k and there is a weight function w : Q → N that maps each q ∈ Q to the minimum such k.

(b) {q ∈ Q | w(q) = i} is finite for each i ∈ N 2. S is weight respecting, i.e.
(a) for all x, x ′ , y ∈ Q such that x → x ′ and x ≤ y, there exists y ′ ∈ Q such that y → y ′ and w(x ′ )-w(x) = w(y ′ )w(y).

3. S is δ-deflatable, i.e.

(a) for δ ∈ N, if x → x ′ and z ≤ x ′ , then there exist y, y ′ such that

• y ≤ x and y → y ′ and z ≤ y ′ ,

• w(y) ≤ w(z) + δ and w(y ′ ) ≤ w(z) + δ.

More precisely, the main differences between NSWs and RMTSs are that NSWs are based on a wqo and require the "weight respecting" condition whereas RMTSs need a po. "Weight respecting" is necessary in [START_REF] Bingham | Empirically efficient verification for a class of infinite-state systems[END_REF] to prove their convergence theorem (Theorem 1). Nonetheless, the RMTS condition 1 is similar to the NSW definition of discrete system (without wqo) and the RMTS conditions 2, 3 and 4 to the NSW definition of deflatability (where δ = max(c, d)). Even if the RMTS conditions may look more complex, we think that stating these conditions instead of the deflatability one is more useful for the following reasons.

• The backward-downward monotony gives a better intuition, because the search for the right c is guided by the notion of the "least transition" whose states have their rank bounded by c. Thus, the RMTS definition targets the biggest "least transition" of the system. • Proving the existential condition of the deflatability, may require an explicit construction of the states y and y ′ , which is not trivial. We will see in the proof of Lemma 6 that the conditions 2 and 4 give a direct construction of the state y ′ (the state y is then chosen among the predecessors of y ′ ). • RMTSs distinguish between the two values c and d (instead of δ). That allows for a better precision at the computation of the pred-basis, as shown in the following.

The objective is now to show that RMTSs allow for the determination of effective pred-basis easily without wqo. In order to find a finite basis of ↑P red(↑s), the idea is to compute a finite subset S ⊂ ↑s, then a finite subset P ⊆ P red(S).

Definition 17. Let S = (Q, →, ≤, γ, c, d) be an RMTS. For all e ∈ N n , let us denote P red e (s) = {q ∈ P red(s) | γ(q) ≤ γ(s) + e} and ↑ e s = {q ∈ ↑s | γ(q) ≤ γ(s) + e}.

P red c (s) and ↑ c s restrict the set of predecessors and the upward-closure of s to the states that are interesting to compute the pred-basis.

Lemma 6. Let S = (Q, →, ≤, γ, c, d) be an RMTS and s ∈ Q. We have ↑P red(↑s) = ↑P red d (↑ c s).

Proof. ⊇ is obvious. To prove ⊆, let us show that P red(↑s) ⊆ ↑P red d (↑ c s) (then ↑P red(↑s) ⊆ ↑P red d (↑ c s) by upward-closure). Let p ′ ∈ P red(↑s) and s ′ ∈ Q such that p → s ′ and s ≤ s ′ . We want to show that there

exists p ∈ Q such that p ≤ p ′ ∧ ∃s ′′ ∈ Q • s ≤ s ′′ ∧ p → s ′′ ∧ γ(s ′′ ) ≤ γ(s) + c ∧ γ(p) ≤ γ(s ′′ ) + d, which entails Definition 17 and p ′ ∈ ↑P red d (↑ c s)
. By the bdm, there exists q 1 → q 2 such that q 2 ≤ s ′ , γ(q 2 ) ≤ c, and

∀q ′ 2 ∈ Q • q 2 ≤ q ′ 2 ≤ s ′ =⇒ ∃q ′ 1 ∈ Q • q ′ 1 → q ′ 2 ∧ q 1 ≤ q ′ 1 ≤ p ′ .
By Condition 2, there exists s ′′ an upper bound of s and q 2 such that s ′′ ≤ s ′ . Thus have q 2 ≤ s ′′ ≤ s ′ . By the bdm, there is p ′′ ∈ Q such that q 1 ≤ p ′′ ≤ p ′ and p ′′ → s ′′ . By Condition 3, there exists p ∈ Q such that p ≤ p ′′ , p → s ′′ and γ(p) ≤ γ(s ′′ ) + d. Finally, by Condition 2, γ(s ′′ ) ≤ γ(s) + γ(q 2 ) ≤ γ(s) + c. A graphical representation of the proof is given in Figure 13.

We construct a basis of ↑P red(↑s) by computing the set P red d (↑ c s). Let us show that this set is finite.

Lemma 7. Let S = (Q, →, ≤, γ, c, d) an RMTS. For all s ∈ Q, ↑P red(↑s) has a finite basis.

Proof. P red d (↑ c s) is a basis of ↑P red(↑s) by Lemma 6. The set {r ∈ N n | r ≤ c} is finite, thus ↑ c s is finite by definition of a rank function. Similarly, for all q ∈ Q, P red d (q) is finite. Consequently, P red d (↑ c s) is finite.

Proposition 8. Effective RMTSs have effective pred-basis. 13. Illustration of Lemma 6 γ(s) + c}, compute the finite set X = r≤γ(s)+c γ -1 (r) and select the elements q ∈ X such that s ≤ q. Then, for all q ∈ ↑ c s, compute P red d (q) = {q ′ ∈ P red(q) | γ(q ′ ) ≤ γ(q) + d} = {q ′ ∈ r≤γ(q)+d γ -1 (r) | q ′ → q}.

Proof. Let S = (Q, →, ≤, γ, c, d) be an effective RMTS. Let us show that for all s ∈ Q, P red d (↑ c s) is computable. As γ is effective, then for all r ∈ N n , γ -1 (r) is computable. To compute ↑ c s = {q ∈ ↑s | γ(q) ≤ p q 1 q 2 s s 0 s 00 ≤ ≤ ≤ ↑s ↑ c s -→ p 00 p 0 -→ ≤ Fig.
This proof gives a naive algorithm to compute P red d (↑ c s), but in practice enumerating an entire set γ -1 (r) is not always necessary. Especially, if P red(q) is computable, then computing P red d (q) is more straightforward.

Example 4 (Petri Nets). Let N = (P, T, F ) be a Petri Net. We denote by S N = (Q, →, ⊆, γ, c, d) the corresponding RMTS defined in Example 1 with c, d ∈ N. Let M be a marking and let us compute a predbasis of M . The set of markings ↑ c M is clearly finite and can be enumerated. For each element M ′ of ↑ c M , P red(M ′ ) is also finite and computable, hence so is P red d (M ′ ).

Even if computing a pred-basis is easy for systems like Petri Nets or Lossy Channel Systems, finding one for some more complex systems [KS14, Mey09] is more difficult. The RMTS framework gives a systematic way to prove the existence of pred-basis without the wqo hypothesis and gives a generic algorithm. Now, if ↑P red(↑s) is computable, then as shown in Section 3.2, we can compute P red * (↑s) by iteration assuming the number of iterations is finite. This is guaranteed by the fact that the quasi-ordering is a wqo.

Proposition 9. For an effective RMTS S = (Q, →, ≤, γ, c, d) with I ⊆ Q and s ∈ Q, if ≤ is a wqo, then a finite basis B ⊆ Q of P red * (↑s) is computable. In addition, if I ∩ ↑B = ∅ is decidable, then cov(S, I, s) is decidable.

Proof. S has effective pred-basis thanks to Proposition 8. Since ≤ is a wqo, then S is a WSTS. Thus, by Theorem 1, the coverability problem is decidable.

Remark that if we do not have a wqo, we can still use the procedure computing P red * (↑s) of Section 3.2 as a semi-algorithm. Furthermore, like in [START_REF] Bingham | Empirically efficient verification for a class of infinite-state systems[END_REF], we have intermediate results by restricting ourselves to the verification for some specific ranks. Let S = (Q, →, ≤, γ, c, d) be an effective RMTS. Then, we can always consider a cut-off value r ∈ N n and a subsystem S r = (Q r , →, ≤) whose set of states is reduced to

Q r = {q ∈ Q | γ(q) ≤ r}.
During the computing of a basis of P red * (↑s), we can conclude on the coverability of s in S r as we go. Indeed, if all backward paths contain a state of rank r and no initial state is currently reached, then s is not coverable in S r . That is more efficient than choosing a value r and checking each S r one by one. We just need to adapt the backward reachability procedure of Section 3.2 either by prioritizing lower ranks or by keeping track of computed paths.

Ranked PASTD

In this section we use RMTSs to prove that PASTDs have effective pred-basis. Because we use a quasiordering on the state space of PASTDs, we cannot say that PASTDs are RMTSs as they require a partial ordering. However, it is natural to consider the quotient set of the state space instead of the entire space when studying systems like PASTDs. Exploiting the symmetries in systems in order to simplify a verification process is usual in the context of formal verification [START_REF] Emerson | Symmetry and model checking[END_REF]. In our case the symmetries entailed by the equivalence relation allow us to consider the coverability problem on the quotient space. In order to satisfy condition 2 of Definition 14 we also need to enlarge PASTD states with the size of parameters used to instantiate the PASTD to which a state belongs. Accordingly, the ordering relation is adjusted to take into account these parameters. For bounded PASTD, this extended order is also a wqo. We first state the monotonicity of (T A , →, ∼), which is necessary for the well-definedness of the quotient state space transitions.

Proposition 10. Let A be a PASTD. Then, (T A , →, ∼) is monotone.

Proof. The proof is done by induction the structure of states, and similar to the one for (T A , →, ) (Proposition 3). It stems from the fact that permutation preserves equality and that an ASTD cannot test a particular value.

Let the point-wise extension of finite set cardinality to vectors of finite sets be noted as

|(R 1 , . . . , R n )| = (|R 1 |, . . . , |R n |)
Definition 18 (Quotient Instantiated ASTD state). Let A be a PASTD with n parameters. Let Q ⊆ T A . We denote by

Q ♯ = {(s, u) | s ∈ Q ∧ u ∈ N n ∧ |val(s)| ≤ u}. Let ( s1 , u 1 ), ( s2 , u 2 ) ∈ T ♯ A .
We say that ( s1 , u 1 ) ♯ ( s2 , u 2 ) iff s 1 s 2 and u 1 ≤ u 2 . Let (x 1 , u 1 ), (x 2 , u 1 ) ∈ T ♯ A . We say that (x 1 , u 1 ) → ♯ (x 2 , u 1 ) iff

∃s 1 ∈ x 1 , s 2 ∈ x 2 • s 1 → s 2 .
We denote by S ♯ A = (T ♯ A , → ♯ , ♯ ) the quotient system. Proposition 11. Let A be a PASTD. Then, S ♯ A is monotone. Proof. The proof stems easily from Definition 18 and Proposition 3.

We need the following lemma to prove that the coverability problem in S A can be reduced to the coverability problem in S ♯ A . Lemma 8. If (x 1 , u 1 ) → ♯ (x 2 , u 1 ), then

∀s 1 ∈ x 1 • ∃s 2 ∈ x 2 • s 1 → s 2 .
Proof. The proof stems easily from Definition 18 and Proposition 10.

u = sup({|val(q)| | q is a state of i * -→ s ′ }).
Let q → q ′ be a step of than run. By definition of → ♯ , we have (q, u) → ♯ ( q′ , u). Thus, we have ( ĩ, u) * -→♯ ( s′ , u) and (s, |val(s)|) ♯ ( s′ , u). For other direction (⇐): let (x 1 , u ′ ) * -→♯ (x m , u ′ ) with x 1 ∈ I ♯ and (s, |val(s)|) ♯ (x m , u ′ ) be a run of S ♯ A . We can construct a run s 1 * -→ s m such that s s m . By definition of → ♯ , there exists s

′ 1 , s ′ 2 • s ′ 1 ∈ x 1 ∧ s ′ 2 ∈ x 2 ∧ s ′ 1 → s ′ 2 .
Take s 1 = s ′ 1 and s 2 = s ′ 2 . Since x 1 ∈ I ♯ and s 1 ∈ x 1 , then s 1 ∈ I. By Lemma 8, we can construct each s j for j ∈ 3..m -1 such that s j → s j+1 . Since s m ∈ x m and (s, |val(s)|) ♯ (x m , u ′ ), then by definition of ♯ we have s s m .

Similarly, the reachability problem in S A si equivalent to the reachability problem in S ♯ A and we can state the following result.

Proposition 12. Reachability is undecidable for PASTDs.

Proof. From Proposition 1, PASTDs simulates RVASSs. Hence, for every RVASS, there exist a PASTD A and an injection from the RVASS to S ♯ A preserving the transitions. Reachability of configurations is undecidable for RVASSs, thus reachability of equivalence classes is undecidable for PASTDs.

From now on, for a PASTD A we study the coverability problem on the quotient MTS S ♯ A . The objective is to find an RMTS for A. Let us define an adequate rank function.

Definition 19. For a PASTD A, let γ : T ♯ A → N n be defined by γ((s, u)) = u.

A state s of T A can belong to any instantiation of a PASTD such that val(s) ⊆ -→ U . The function γ gives for a particular instantiation of state s the size of the instantiation parameters. All states of an equivalence class in T ♯ A have the same size. For instance, the state of Figure 3 from the library example can be from a PASTD instantiated with

- → U ⊇ ({m 1 , m 2 }, {b 1 , b 2 }).
The state describes a configuration with at least two members and two books. Now, let us prove that Condition 2 of Definition 14 is satisfied, i.e. that if two PASTD states have an upper bound, they have a "bounded" one according to the rank function γ.

Lemma 9. Let A be a PASTD. For all x 1 , x 2 , x 3 ∈ T ♯ A such that x 1 ♯ x 3 and x 2 ♯ x 3 , there exists

x 4 ∈ T ♯ A such that x 1 ♯ x 4 , x 2 ♯ x 4 , x 4 ♯ x 3 and γ(x 4 ) ≤ γ(x 1 ) + γ(x 2 ). Proof. Let A = (F, - → T , - → P ). Let x 1 = ( s1 , u 1 ), x 2 = ( s2 , u 2 ), x 3 = ( s3 , u 3 ). Let s 1 = (V 1 , E 1 , λ 1 ), s 2 = (V 2 , E 2 , λ 2
) and s 3 = (V 3 , E 3 , λ 3 ). By Definition 18, s 1 s 3 ; by Definition 9, there exist an isomorphism f 13 from (V 1 , E 1 ) to an induced subgraph of (V 3 , E 3 ) and permutations σ 13,i on P i for each i ∈ 1..n. Consider the same notations f 23 and σ 23,i for s 2 s 3 . We construct x 4 = ( s4 , u 4 ) as follows Let

s 4 = (V 4 , E 4 , λ 4 ) such that V 4 = {v ∈ V 3 | v ∈ Im(f 13 ) ∪ Im(f 23 )}, E 4 = {{v, w} ∈ E 3 | v, w ∈ V 4 } and λ 4 = λ 3 ↾ V4 .
s 4 is a wellformed state because s 1 , s 2 and s 3 are from the same PASTD and only branches from quantified interleaving nodes are pruned from s 3 to obtain s 4 . Hence, s 4 ∈ T A . Clearly, s 4 s 3 by construction. Using the same injection f 13 and permutations σ 13,i , we have that s 1 s 4 . Same for s 2 s 4 . Let Z = {|val(s 4 )|, u 1 , u 2 } and u 4 = sup(Z). Since u 3 is an upper bound of Z, we have u 4 ≤ u 3 , hence ( s1 , u 1 ), ( s2 , u 2 ) ♯ ( s4 , u 4 ) ♯ ( s3 , u 3 ). We have that |val(s

4 )| ≤ |val(s 1 )| + |val(s 2 )| because for each v ∈ V 4 with λ 4 (v) ∈ P i either there is w ∈ V 1 such that σ 13,i (λ 1 (w)) = λ 4 (v) or there is w ∈ V 2 such that σ 23,i (λ 2 (w)) = λ 4 (v). For each i ∈ 1..n: if u 4 [i] = |val(s 4 )[i]| then u 4 [i] ≤ |val(s 1 )[i]| + |val(s 2 )[i]| ≤ u 1 [i] + u 2 [i], by Definition 18; if u 4 [i] = u 1 [i] or u 2 [i], then u 4 [i] ≤ u 1 [i] + u 2 [i]. Hence γ(x 4 ) ≤ γ(x 1 ) + γ(x 2 ).
Intuitively, take the example of the library and consider a state x 1 such that γ(x 1 ) = (1, 1) and where the member m 1 borrowed the book b 1 and a state x 2 such that γ(x 2 ) = (1, 1) and where the member m 2 has returned the book b 2 , then clearly x 1 and x 2 have upper bounds. We can construct a "little" state x 3 such that γ(x 3 ) = (2, 2) including the two different cases. Now, for each PASTD, we can determine a c ∈ N n which is a bound satisfying Condition 4 of Definition 14, using the function µ defined as follows.

Definition 20. Let A = (F, -→ T , -→ P ) be a PASTD. The function µ, which gives for each PASTD expression F a vector of natural c ∈ N n , is defined recursively as follows. 1. µ

(ǫ) = (0, . . . , 0) 2. µ(A[q 1 [F 1 ], . . . , q j [F j ]]) = sup({µ(F i ) | i ∈ 1..j}) 3. µ(|| ∆ [F 1 , F 2 ]) = µ(F 1 ) + µ(F 2 ) 4. µ( | x∈Ti [F ]) = µ(F ) + (u 1 , . . . , u n ), where u i = 1 and ∀i = j • u j = 0 5. µ( ||| x∈Ti [F ]) = µ(F ) + (u 1 , . . . , u n ), where u i = 1 and ∀i = j • u j = 0
The function µ determines the maximum number of instances of each type that are involved in a transition. Intuitively, we count one instance for each quantified operator associated to the corresponding parameter. Remark that there is at least one instance for each parameter that is used in a quantified operator. For a PASTD A = (F, -→ T , -→ P ), µ(F ) allows us to prove the backward-downward monotony.

Lemma 10. Let A = (F, -→ T , -→ P ) be a PASTD and c = µ(F ). For each transition x 1 → ♯ x 2 , there is For instance, consider the PASTD of the library (F, (T m , T b ), (P m , P b )) whose expression F is illustrated in Figure 2. By Definition 20, we have µ(F ) = (2, 2) (remark that each parameter appears twice in the tree). It means that for each transition in the system, a maximum of 2 members and 2 books will be actually involved. The property is verified in the transition depicted in Figure 5: the lesser transition is represented by bold strokes and includes only one member and one book. We can now state that PASTDs are effective RMTSs. adequate subgraph wqo that is similar to our case: the set of states is restricted to those of bounded simple paths. The work of [START_REF] Meyer | Structural Stationarity in the π-Calculus[END_REF] studies π-Calculus expressions, a class a process algebras. For a subclass of π-Calculus expressions, called structurally-stationary dynamically reconfigurable systems, the author proposes a qo based on a rooted tree ordering on process fragments, and shows that processes of bounded depth form a WSTS. Fragments are based on sequential processes which are related by the restriction operator. Depth boundedness is based on the nesting of restriction expressions within a fragment, whereas in our case boundedness arises from simple paths whose length depends on occurrences of quantified variables values in a state, which are more difficult to characterise syntactically. We provide two syntactical subclasses of Bounded-PASTDs. Alternate wqos on graphs, like the graph minor relation [START_REF] Robertson | Graph minors xxiii. nash-williams' immersion conjecture[END_REF], can also be used [START_REF] König | A general framework for well-structured graph transformation systems[END_REF]. But in our case it does not satisfy the monotony condition. In [START_REF] König | A general framework for well-structured graph transformation systems[END_REF], the authors present a framework for viewing Graph Transformation Systems as WSTSs under certain conditions. They give as well an algorithm computing pred-basis in this particular context. The framework of Nicely Sliceable WSTS [START_REF] Bingham | Empirically efficient verification for a class of infinite-state systems[END_REF], which is closer to ours in term of requirements, gives also a subclass of WSTS. However, they are both tied to a wqo condition (by definition of WSTS), unlike the RMTS framework.

y 1 → ♯ y 2 such that y 2 ♯ x 2 , γ(y 2 ) ≤ c, and ∀z 2 ∈ T ♯ A • y 2 z 2 x 2 =⇒ ∃z 1 ∈ T ♯ A • z 1 → z 2 ∧ y 1 z 1 x 1 . Proof.

Conclusion

Results and discussion. In this article, we presented a model called PASTD, a variant of ASTD, which allows for the specification of complex parameterized systems like information systems. A PASTD specification is a formal model with a graphical notation which is easy to read. PASTDs are more expressive than VASSs with resets, hence the reachability problem is undecidable for PASTDs. Furthermore, we pointed out some subclasses of PASTD (Bounded-PASTD, 1-PASTD and Flat-PASTD) which are WSTSs. Then, we introduced a new general framework called RMTS to prove the existence and computability of pred-basis in any monotone transition system. RMTSs give a set of properties that should be satisfied by a system to compute a pred-basis but do not require a wqo as in WSTSs. Finally, we showed that PASTDs are RMTSs and thus that the coverability problem is decidable for Bounded-PASTDs. The relation between the different classes of model presented in this paper is summarized in Figure 14. Remark that to match with the definition of RMTS, we assume that all quasi-orderings are partial orderings (by considering quotient space for instance). For Bounded-PASTDs, we have a complete procedure to decide coverability and thus to verify safety properties. We think that Bounded-PASTDs can model a larger class of parameterized systems than classical models like RVASSs. Unfortunately, many parameterized systems are not Bounded-PASTDs. Indeed, the library example presented in this paper is not well-structured as we can find an example of antichain similar to the one of Figure 9. However, we were able to prove that PASTDs are effective RMTSs. In fact, the RMTS framework allowed us to find the adequate conditions to construct the PASTD class of systems that is RMTS. For instance, considering abstract states in PASTDs was necessary to prove the backward-downward monotony, thus to prove the effective pred-basis without wqo and can make the computation easier in the same time. Intuitively, an abstract state is a state where the local configurations of some instances are unknown. It is useful to model a quantified interleaving state with partial information. Hence, an abstract state represents a set of concrete states whose quantified interleaving are completely instantiated. This allows for the factorization of the pred-basis computation (see [START_REF] Chane-Yack-Fa | Verification of parameterized algebraic state transition diagrams[END_REF] for more details). Considering an effective RMTS S = (Q, →, ≤, γ, c, d) and a state s ∈ Q, a semi-decision procedure to determine if an initial state belongs to P red * (↑s) is possible. More than a semi-algorithm, sometimes the procedure may terminate without wqo even if s is not coverable. This is the case when a basis of P red * (↑s) is computed. Indeed, even if (Q, ≤) is not a wqo, (P red * (↑s), ≤), which depends on the state s, may be wqo. That justifies the practical importance of this semi-decidability result. Moreover, determining the complexity of a wqo-based algorithm is not easy [START_REF] Schmitz | Algorithmic aspects of wqo theory[END_REF]. In practice, if we are not able to get a reasonable complexity, the wqo argument may not be sufficient to guarantee that the implemented verification procedure will end.

Future work. Experimenting the backward algorithm on different RMTSs like PASTDs would be the next step in order to determine for which kind of systems and coverability properties the procedure is likely to stop within a reasonable amount of time. Besides, concerning PASTDs, we have given two easily recognizable subclasses of Bounded-PASTDs but we should be able to determine a more general algorithm deciding if a PASTD is well-structured, which is hinted by Lemma 5. Finally, as computing P red * (↑s) should not be necessary to solve the coverability problem, it would be interesting to find other termination conditions than wqo for a backward algorithm that checks emptiness of the intersection of P red * (↑s) and the set of initial states; some conditions that would be more dependent on the transition system.

As we also consider abstract states, we introduce a function Abinit which characterizes the set of abstract initial states.

Definition 22 (Abstract initial states). Let F be an ASTD expression. We define the set Abinit(F ) by: Abinit(F ) = {s | s init(F )} Similarly to initial states, we define final states by a predicate final that determines whether a state is considered as final.

Definition 23 (Final states). Let F be an ASTD expression and s a state of F . The predicate final F (s), which determines if s is final in F , is defined as follows:

1. If s = (aut • , q) and F = A = (Q, Σ, δ, q 0 , Q f ), then final F (s) ≡ q ∈ Q f 2. If s = (aut • , q)[s ′ ] and F = A[q 1 [F 1 ], . . . , q[F ′ ], . . . , q k [F k ]] with A = (Q, Σ, δ, q 0 , Q f ), then final F (s) ≡ q ∈ Q f ∧ final Automaton ASTDs can be defined with free variables, which are used in parameterized events. Those variables can be bound by some quantified operator ASTD. In order to keep track of the bound variables in a sub-state, when computing a transition, we need an execution environment that contains a valuation for each variable.

Definition 24 (Environment). An environment is a function which maps a variable to a value. An environment is noted ([x 1 , . . . , x n := v 1 , . . . , v n ]), or ([ x := v]). An empty environment is noted ([]). An environment Γ can be used in a substitution. The symbol is a composition operator on environments such that if Γ 1 , Γ 2 are environments and u an expression, u[Γ 1 Γ 2 ] = (u[Γ 1 ])[Γ 2 ] (here, brackets denote a substitution). Note that Γ 1 has precedence over Γ 2 when Γ 1 Γ 2 is used in a substitution. Remark that the notion of environment does not affect the definitions of the function init and predicate final . However, it is important in the definition of the transition relation of ASTDs. The operational semantics of ASTDs consists of a set of inference rules defined inductively. We write transitions with respect to an environment Γ, noted as s σ,Γ --→ F s ′ , where s and s ′ are two states of an ASTD F and σ an event. Subscript F can be omitted when it is clear from the context which ASTD is being referred to.

Definition 25 (Transition rules). Let F be an ASTD expression and s and s ′ two states of F . We compute a transition starting from an empty environment, using the following inference rule. The rule env allows to introduce the environment in transitions, that is necessary to use the other inference rules described below. Let F be an ASTD, Γ an environment and σ an event. The operational semantics is inductively defined for each ASTD subtype. [START_REF][END_REF]. If F = A[q 1 [F 1 ], . . . , q k [F k ]] with A = (Q, Σ, δ, q 0 , Q f ), each transition in F is given by one of the two following inference rules: δ(q i , q j , σ ′ , f inal?) f inal? ⇒ final Fi (s)

σ ′ [Γ] = σ s ′ ∈ Abinit(F j ) aut 1 (aut • , q i )[s] σ,Γ --→ F (aut • , q j )[s ′ ] s σ,Γ --→ Fi s ′ aut 2 (aut • , q i )[s] σ,Γ --→ F (aut • , q i )[s ′ ]
Rule aut 1 describes a transition between local states. There is a transition, labeled by σ and with environment Γ, between some state of q i and the initial state of q j if there is an arrow in the automaton between q i and q j , labeled by σ ′ and such that the environment applied as a substitution on σ ′ gives σ, and if the transition marked as final, then the source state must be a final state. Rule aut 2 handles transition within a sub-state. Rule |: 1 describes the execution of the first event from the initial state, whereas Rule |: 2 deal with the execution of the subsequent events. In both cases, the value bound to the quantification variable is added to the execution environment and can be used to make the proof after the environment has been applied as a substitution. Rule |||: 1 describes the execution of an event from the component ASTD instantiated by value p i . The value p i bound to the quantification variable x is added to the execution environment.

  Fig. 1. Example of a library system

Fig. 7 .

 7 Fig. 7. An RVASS and its PASTD simulation

Theorem 3 .

 3 For any Bounded-PASTD A, (T A , ) is a wqo.Proof. Let k ∈ N satisfying Definition 11. By Ding's theorem (P k (Λ A ), ⊑) is a wqo. Then, any subset G A ⊆ P k (Λ A ) is a wqo and by Lemma 3 (T A /∼, ) is a wqo, because isomorphisms preserve wqos. Thus, (T A , ) is a wqo.

Theorem 4 .

 4 Let A be a PASTD. Then, cov(S A , I, s) ⇐⇒ cov(S ♯ A , I ♯ , (s, |val(s)|)). Proof. Direction ⇒ : Let i * -→ s ′ with i ∈ I and s s ′ be a run of S A . Let

  By induction on the structure F of the PASTD. See a similar proof in [CYF17].

  Pred * (↑s) is computable for WSTS ∩ RMTS

Fig. 14 .

 14 Fig. 14. Comparison of the models

F

  ′ (s ′ ) 3. If s = || • [s 1 , s 2 ] and F = || ∆ [F 1 , F 2 ], then final F (s) ≡ final F1 (s 1 ) ∧ final F2 (s 2 ) 4. If s = |: • and F = | x∈T [F ′ ], then final F (s) ≡ final F ′ (init(F ′ )) 5. If s = |: • [p[s ′ ]] and F = | x∈T [F ′ ], then final F (s) ≡ final F ′ (s ′ ) 6. If s = |||: • [p 1 [s 1 ], . . . , p k [s k ]] and F = ||| x∈T [F ′ ], then final F (s) ≡ ∃i ≤ k • final F ′ (s i )

  For example, if we consider the ASTD book(b) from Figure1where b is instantiated by a value b 1 , and we look locally at the sub-state (aut • , B1)[|: • [m 1 [(aut • , L0)]]], we need the environment ([b := b 1 ]) in the sub-ASTD loan(b 1 ) to compute the transition lend(b 1 , m 1 ), because the valuation does not appear in the expression of the sub-state.

1

 1 2. If F = || ∆ [F l , F r ], || • [s l , s r ] σ,Γ --→ F || • [s ′ l , s r ] Fr s ′ r || 2 || • [s l , s r ] σ,Γ --→ F || • [s l , s ′ r ] Fr s ′ r || 3 || • [s l , s r ] σ,Γ --→ F || • [s ′ l , s ′ r ]Rules || 1 and || 2 respectively describe execution of events with no synchronization required on the lefthand side and the right hand side of the synchronization ASTD. Rule || 3 describes the synchronization between the left hand side and the right hand side.3. IfF = | x∈T [F ′ ], s σ,([x:=p]) Γ --------→ F ′ s ′ s ∈ Abinit(F ′ ) p ∈ T |: 1 |: • σ,Γ --→ F |: • [p[s ′ ]] s σ,([x:=p]) Γ --------→ F ′ s ′ |: 2 |: • [p[s]] σ,Γ --→ F |: • [p[s ′ ]]

  4. If F = ||| x∈T [F ′ ], s σ,([x:=pi]) Γ --------→ F ′ s ′ |||: 1 |||: • [p 1 [s 1 ], . . . , p i [s], . . . , p k [s k ]] σ,Γ --→ F |||: • [p 1 [s 1 ], . . . , p i [s ′ ], . . . , p k [s k ]]

  . . , u n )) → (p ′ , (u ′ 1 , . . . , u ′

n )) if (p, (a 1 , . . . , a n ), p ′ ) ∈ E, where for all i ∈ 1..n, either

Theorem 5. Let A = (F, -→ T , -→ P ) be a PASTD and S ♯ A = (T ♯ A , → ♯ , ♯ ) the quotient MTS, then S = (T ♯ A , → ♯ , ♯ , γ, µ(F ), -→ 0 ) is an effective RMTS.

Proof. (T ♯ A , → ♯ , ♯ ) is a MTS by Proposition 11 and a po on T ♯ A . [START_REF][END_REF]. Let x, y ∈ T ♯ A such that x ♯ y. We clearly have γ(x) ≤ γ(y) by definition of γ. Thus, γ is monotone. Let r ∈ N n be a specific rank. Remark that there exists a k ∈ N such that for all x = (s, r) ∈ γ -1 (r) with g(s) = (V, E, λ), |V | ≤ k. Then, for all x = (s, r) ∈ γ -1 (r) with g(s) = (V, E, λ), |V | and |E| are bounded and Im(λ) is always finite. By a combinatorial argument, there is a finite number of possible graphs whose rank is r. And because g is a bijection, γ -1 (r) is then finite. 2. Condition 2 is proved by Lemma 9. As a consequence, S is an RMTS. The transition relation is decidable as it is defined by a set of rules (see Appendix A). Also by definition, ♯ is decidable and γ(x) computable for x ∈ T ♯ A . For r ∈ N n , γ -1 (r) is computable by enumerating all well-formed states x such that γ(x) = r. Thus, S is an effective RMTS.

For any PASTD, we conclude that we can compute a finite pred-basis of any state x. An alternative to enumerating γ -1 (r) for computing the finite pred-basis

is computable. Thus, we can iterate over the successors x ′ until γ(x ′ ) > γ(x) + c and compute their predecessors s ′′ wrt → ♯ until γ(x ′′ ) > γ(x ′ ) + d. P red(x ′ ) can be infinite for a PASTD, but it can be enumerated by starting with the smallest predecessors and incrementing their ranks until γ(x ′′ ) > γ(x ′ ) + d. If we want to compute a finite basis of P red * (↑x) and decide coverability, we need the wqo condition.

Proposition 13. Let A be a Bounded-PASTD. (T ♯ A , ♯ ) is a wqo. Proof. By Theorem 3, (T A , ) is a wqo; thus the quotient T A /∼ is also a wqo. (N n , ≤) is also a wqo (Dickson's lemma). Thus, (T ♯ A , ♯ ) is a Cartesian product of wqos. The Cartesian product of wqos is a wqo. Theorem 6. Bounded-PASTDs are WSTSs with effective pred-basis. Hence, the coverability problem is decidable.

We have that ♯ is a wpo as A is a Bounded-PASTD, thus we can compute a basis of P red * (↑x). We can check whether P red * (↑x) ∩ I ♯ is empty or not because I ♯ is easily recognisable (initial states are explicited in Appendix A). Hence, by Proposition 9, cov(S ♯ A , I ♯ , x) is decidable.

Related Work

Several models in the literature allow for the specification of parameterized systems [Pet81, HSBR10, SK09b, DSZ10, KS14], but most of them are too restrictive for some complex systems like information systems because they do not allow us to model relationships between entities or parameters. In general, process algebras [BK84, BB87, FSD03] are suitable to specify information systems but it is not always clear how to handle parameterized systems. In particular, [FFC + 10] shows that specifying and verifying information systems can be done for finite state systems. However, most of the existing models are not adapted to parameterized verification. The verification of EB 3 specifications, from which the ASTD notation derives, has been studied in [START_REF] Vekris | Verification of eb 3 specifications using CADP[END_REF] but the paper does not consider parameters. In [START_REF] Siirtola | Parameterised process algebraic verification by precongruence reduction[END_REF], the authors present a model close to ours called LTS schema that improves labeled transition systems with process algebra operators and allows parameterization.