Marius Bozga
email: marius.bozga@univ-grenoble-alpes.fr

Radu Iosif
email: radu.iosif@univ-grenoble-alpes.fr

Specification and Safety Verification of Parametric Hierarchical Distributed Systems

We introduce a term algebra as a new formal specification language for the coordinating architectures of distributed systems consisting of a finite yet unbounded number of components. The language allows to describe infinite sets of systems whose coordination between components share the same pattern, using inductive definitions similar to the ones used to describe algebraic data types or recursive data structures. Further, we give a verification method for the parametric systems described in this language, relying on the automatic synthesis of structural invariants that enable proving general safety properties (absence of deadlocks and critical section violations). The invariants are defined using the WSκS fragment of the monadic second order logic, known to be decidable by a classical automata-logic connection. This reduces the safety verification problem to checking satisfiability of a WSκS formula. We implemented the invariant synthesis method into a prototype tool and carried out verification experiments on a number of non-trivial models specified using the term algebra.

Introduction

The separation between behavior and coordination is a fundamental principle in the design of large-scale distributed systems [START_REF] Kramer | Analysing dynamic change in distributed software architectures[END_REF]. By behavior we mean a set of traces of observable events. A component is a representation of a behavior, by means of a (finite) state machine, whose actions are labeled by events. The architecture of the system defines the interactions between components, as sets of events that must occur simultaneously in several components. For instance, Fig. 1a shows a token-ring systems, whose components are depicted in yellow boxes (behaviors are modeled by the finite-state machines within the boxes) and whose architecture is the set of connections between components (depicted with solid lines). Such high-level models of real-life distributed systems are suitable for reasoning about correctness in the early stages of system design, when details related to network reliability or the implementation of coordination mechanisms, by means of low-level synchronization mechanisms (e.g. semaphores, monitors, compare-and-swap, etc.) are abstracted away. This modular view of a distributed system is key to scalable design methods that exploit a conceptual hierarchy, in which each module is split into submodules. For instance, a ring is a chain whose final output port is connected to the initial input port, whereas a chain consists of a (head) component linked to a separate (tail) chain (Fig. 1b). Furthermore, system designers are accustomed to the use of predefined architectural patterns, that define the interactions between (unboundedly large) sets of modules (e.g. crowds, rings, pipelines, stars, trees, etc.). In this context, the contribution of the paper is three-fold.

1. We introduce a formal language to describe the coordinating architectures of distributed systems parameterized by (i) the number of components of each type that are active in the system, e.g. a system with n readers and m writers, in which n and m are not known a priori and (ii) the pattern in which the interactions occur (e.g. a pipeline, ring, star or more general hypergraph structures). The language uses predicate symbols to hierarchically break the architecture into sub-modules. The interpretation of these predicate symbols is defined inductively by rewriting rules consisting of terms that contain predicate atoms, in a way that recalls the usual definitions of algebraic datatypes [START_REF] Barrett | An abstract decision procedure for a theory of inductive data types[END_REF] or heaps [START_REF] Reynolds | Separation logic: A logic for shared mutable data structures[END_REF].

2. We tackle the parametric safety problem for systems described in this language, which is checking that the reachable states of every jnstance stays clear of a set of global error configurations, such as deadlocks or critical section violations. We synthesize invariants directly from the syntactic description of the system, generate WSκS formulae [START_REF] Thatcher | Generalized finite automata theory with an application to a decision problem of second-order logic[END_REF] that are unsatisfiable only if every system described by the given inductive definitions is safe and use off-the-shelf WSκS solvers [START_REF] Henriksen | Mona: Monadic second-order logic in practice[END_REF] for proving safety automatically. The invariant synthesis method models the set of executions of a parametric system as a boolean (1-safe) Petri net of unbounded size and computes structural invariants (trap invariants, linear invariants) of this Petri net.

3. We implemented the invariant synthesis in a prototype tool and experimented with a number of parametric component-based systems with non-trivial architectural patterns, such as trees with root links, trees with linked leaves, token-rings with or without a main controller, etc.

Example 1. Let us consider a distributed system consising of components of type C, having two interaction ports, namely in and out and whose behavior is described by a finite state machine with transitions q 0 out -→ q 1 and q 1 in -→ q 0 . These components are arranged in a ring, such that the out port of a component is connected to the in port of its right neighbour, with the exception of the last component, whose out port connects to the in port of the first component (Fig. 1a). The connections (interactions) in the system are described by the predicate Ring(), defined inductively by the rules below:

Ring() ← νy 1 νy 2 . out(y 2 ) • in(y 1 ) (Chain(y 1 , y 2 )) ( 1)

Chain(x 1 , x 2 ) ← out(x 1 ) • in(x 2 ) (Comp(x 1 ), Comp(x 2 )) (2) Chain(x 1 , x 2 ) ← νy 1 . out(x 1 ) • in(y 1 ) (Comp(x 1 ), Chain(y 1 , x 2 )) (3) Comp(x) ← C(x) (4)
q 0 • • • out out out in in in C(y 1 ) C(y 1 1 ) C(y n 1 ) C(y 2 ) in out (a) (b) C(y 1 ) C(y 1 1 ) out Chain(y 2 1 , y 2 ) in in in out out
Ring()

Chain(y 1 1 , y 2 ) Chain(y 1 , y 2 ) 3 1 3 in out q 1 q 0 in out q 1 q 0 in out q 1 q 0 in out q 1
Fig. 1. Recursive Specification of a Token-Ring System Rule (1) states that a Ring() consist of a Chain(y 1 , y 2 ), where y 1 and y 2 are the indices of the first and last components1 , respectively. The last out port is connected to the first in port, written as out(y 2 ) • in(y 1 ). Rule [START_REF] Barrett | An abstract decision procedure for a theory of inductive data types[END_REF] states that the least Chain(x 1 , x 2 ) consists of two instances of type C, namely C(x 1 ) and C(x 2 ), and the out port of x 1 connects to the in port of x 2 , described as out(x 1 )•in(x 2 ). Rule (3) gives the inductive step, namely that every Chain(x 1 , x 2 ) consists of a component C(x 1 ) that interacts with a disjoint chain from y 1 to x 2 . Here the binder νy 1 makes sure the value of y 1 is different from the value of every other variable in the system. Since this binder is used in a recursive rule, each identifier in a subsequent unfolding of Chain(y 1 , x 2 ) is guaranteed to be unique. Last, rule (4) is used to instantiate (i.e. create new) components of type C. In principle, this rule is not necessary, as any occurrence of a predicate Comp(y) can be replaced by a component C(y), however it is considered for technical reasons related to our invariant-based verification approach.

Fig. 1b shows the unfoldings of this set of recursive definitions. The system depicted in Fig. 1a is obtained by an application of rule (1), followed by n applications of rule (3), ending with an application of rule [START_REF] Barrett | An abstract decision procedure for a theory of inductive data types[END_REF]. The first two applications of (3) following the application of (1) are depicted in Fig. 1b, with rule labels annotated (each application of rule (3) creates a fresh variable, denoted by y 1 1 , . . . , y n 1 , respectively).

Preliminaries

This section introduces preliminary definitions used throughout the paper. Given sets A and B, we denote by A → B the set of total functions f :

A → B. If a = a 1 , . . . , a n is a tuple of values from A, then f (a) def = f (a 1 ), . . . , f (a n )
. By a • b we denote the concatenation of tuples a and b. For two positive integers k, ∈ N, we denote by [k, ] the set {k, k + 1, . . . , }, assumed to be empty if k > . The cardinality of a finite set A is denoted by |A|. Trees Trees play a key role in the definition of parametric distributed systems from the following section ( §3). Let κ ≥ 1 be an integer constant, fixed throughout this paper, and let [1, κ] * denote the set of finite sequences of integers between 1 and κ, called nodes in the following. A κ-ary tree T is a partial function mapping [1, κ] * to a set of labels. The domain of T , denoted nodes(T ), is such that wi ∈ nodes(T ) for some i ∈ [1, κ] The invariant synthesis method uses the restriction of monadic second order logic to trees of branching degree κ and quantification over finite sets only. Let V 1 = {x, y, z, . . .} and V 2 = {X, Y, Z, . . .} be countably infinite sets of first and second order variables, respectively. The formulae of the WSκS logic are defined inductively by the syntax:

τ ::= | x ∈ V 1 | τ 1 .i, i ∈ [1, κ] terms φ ::= τ = τ | X(τ ) | φ ∧ φ | ¬φ | ∃x . φ | ∃X . φ formulae As usual, we write φ 1 ∨ φ 2 def = ¬(¬φ 1 ∧ ¬φ 2 ), φ 1 → φ 2 def = ¬φ 1 ∨ φ 2 , φ 1 ↔ φ 2 def = (φ 1 → φ 2 ) ∧ (φ 2 → φ 1 ), ∀x . φ def = ¬∃x . ¬φ and ∀X . φ def = ¬∃X . ¬φ.
WSκS formulae are interpreted over an infinite tree, where first order variables x ∈ V 1 range over individual nodes n ∈ [1, κ] * , second order variables X ∈ V 2 range over finite sets of nodes, is a constant symbol interpreted as the root of the tree and, for all i ∈ [1, κ], the notation .i is is interpreted as the function mapping

each w ∈ [1, κ] * into wi. Given a valuation ν : V 1 ∪ V 2 → [1, κ] * ∪ 2 [1,κ] * , such that ν(x) ∈ [1, κ] * , for each x ∈ V 1 and ν(X) ⊆ [1, κ] * (ν(X) is finite), for each X ∈ V 2 ,
the satisfaction relation |= is defined inductively, as usual [START_REF] Khoussainov | Automata Theory and its Applications[END_REF]. A valuation ν is a model of a formula φ iff ν |= φ. A formula is satisfiable if and only if it has a model. Petri nets A Petri net (PN) is a tuple N = S, T, E , where S is a set of places, T is a set of transitions, S ∩ T = ∅, and E ⊆ (S × T ) ∪ (T × S) is a set of edges. Given x, y ∈ S ∪T , we write E(x, y)

def = 1 if (x, y) ∈ E and E(x, y) def = 0, otherwise. Let • x def = {y ∈ S ∪ T | E(y, x) = 1}, x • def = {y ∈ S ∪ T | E(x, y) = 1}
and lift these definitions to sets of nodes. A marking of N is a function m : S → N. A transition t is enabled in m if and only if m(s) > 0 for each place s ∈ • t. We write m t -→ m whenever t is enabled in m and m (s) = m(s) -E(s, t) + E(t, s), for all s ∈ S and t ∈ T . A sequence of transitions σ = t 1 , . . . , t n is a firing sequence, written m σ -→ m if and only if either (i) n = 0 and m = m , or (ii) n ≥ 1 and there exist markings m 1 , . . . , m n-1 such that m

t 1 -→ m 1 . . . m n-1 tn -→ m .
A marked Petri net is a pair N = (N, m 0 ), where m 0 is the initial marking of N. A marking m is reachable in N if there exists a firing sequence σ such that m 0 σ -→ m. We denote by R(N ) the set of reachable markings of N . A marked PN N is boolean if m(s) ≤ 1, for each s ∈ S and m ∈ R(N ). All marked PNs considered in the following will be boolean and we shall silently blur the distinction between a marking m : S → {0, 1} and the set {s ∈ S | m(s) = 1}.

Given a set of markings E, a marked PN N is safe w.r. • def

= (P )

• (w) (we omit brackets when they are clear from the context). We consider below a set B of component types, with pairwise disjoint sets of port and state types. Architectures The coordination in a system is defined by architectures. An interaction π ∈ 2 P is a finite set of ports. An architecture γ ⊆ 2 P is a finite set of interactions. Given component types B i = P i , S i , I i , ∆ i ∈ B and tree nodes w i ∈ [1, κ] * , the behavior of the system consisting of the components B i (w i ), i = 1, . . . , n, coordinated by the architecture γ is defined by the marked PN γ(B 1 (w 1 ), . . . ,

B n (w n )) def = ( S, γ, E , m 0 ), where S def = n i=1 {S(w i ) | S ∈ S i
} is the set of places, for each interaction π ∈ γ, the edges to (from) π are given by

• π def = { • p | p ∈ π} (π • def = {p • | p ∈ π}) and the initial marking is m 0 def = {I i (w i ) | i ∈ [1, n]}.
Example 2. Fig. 2 shows the marked PN that defines the behavior of the system from Fig. 1a. The tree node 1 . . . 1 (i times) is represented by its value i in the unary encoding. The interaction {in(n), out(1)} is duplicated, for readability. The initially marked places are surrounded by dashed circles. q 0 (1)

q 1 (1)
in( 1) out(2)

q 0 (2) q 1 (2) q 0 (n) q 1 (n) in(n -1) out(n) in(2) out(3) in(n) out(1) . . . in(n) out(1)
Fig. 2. The Behavior of a Token-Ring System

A Term Algebra of Behaviors

In this section we introduce a term algebra for describing the systems resulting from the application of an architecture to an unbounded number of component type instances (see Example 1 for the specification of a token-ring system in this language). Let A be a countably infinite set of predicate symbols, and let #(A) denote the arity of the predicate symbol A ∈ A.

Syntax The following syntax generates behavioral terms inductively:

P ∈ [1, κ] * → P, x ∈ V 1 , B ∈ B, A ∈ A I ::= P (x) | I 1 • I 2 interactions Γ ::= I | Γ 1 + Γ 2 architectures b ::= B(x) | Γ (b 1 , . . . , b n ) | νx . b 1 | A(x 1 , . . . , x #(A) ) behavioral terms A variable
x occurring in a behavioral term b is free if it does not occur in the scope of some subterm of the form νx . b 1 and bound otherwise. The set of free variables occurring in a term b is denoted by fv(b). In the following, we assume that all bound variables occurring in a term are pairwise distinct and distinct from the free variables. This assumption loses no generality because terms obtained by α-conversion (renaming of bound variables) are usually viewed as the same term. A term b is closed if fv(b) = ∅ and predicateless if no predicates from A occur in b. We denote by b[y 1 /x 1 , . . . , y n /x n ] the term obtained by substituting the variable x i ∈ fv(b) with y i , for each i ∈ [1, n]. We write size(b) for the number of occurrences of symbols in b.

A term B(x) is called an instance atom and a term A(x 1 , . . . , x n ) is called a predicate atom. We denote by # pred (b) the number of occurrences of predicate atoms and by pred i (b) the predicate atom that occurs i-th in b, for i ∈ [1, # pred (b)], in some linear order of the nodes in the syntax tree of b. The predicate symbols are interpreted as the least sets of predicateless terms inductively defined by a rewriting system: Definition 1. A rewriting system is a finite set R of rules of one of the forms:

A(x) ← B(x) A(x 1 , . . . , x #(A) ) ← νy 1 . . . νy n . Γ (A 1 (z 1 1 , . . . , z 1 #(A1) ), . . . , A m (z m 1 , . . . , z m #(Am) )) where m ≥ 1 and {z i 1 , . . . , z i #(Ai) } m i=1 is a partition of {x 1 , . . . , x #(A) , y 1 , . . . , y n }
For instance, in Example 1, rule ( 4) is an instantiation rule, whereas (1), ( 2) and (3) are inductive rules. We write Semantics Let us consider a given closed behavioral term b and a rewriting system R. First, we define the semantics of a (closed) predicateless behavioral term t ∈ [b] R , as the behavior (i.e. marked PN) resulting from joining the components defined by the instance atoms from t, via the architecture consisting of all the interactions that occur in t. This definition is done in two steps: (a) we write t in prenex form as νx 1 . . . νx n . u, where u contains no more terms of the form νx . b, by moving all the ν binders upfront. Because all bound variables in t, including those introduced by rewriting, are assumed to be pairwise distinct, this step incurs no name clashes. (b) we apply the following flattening relation exhaustively:

A(x 1 , . . . , x #(A) ) ← R b for A(x 1 , . . . , x #(A) ) ← b ∈ R. The size of R is size(R) def = A(x1,...,x #(A) )← R
Γ 1 ( Γ 2 (b 1 , . . . b i ), b i+1 , . . . b n ) Γ 1 + Γ 2 (b 1 , . . . , b n ) (5)
Example 3. Consider the below rewriting sequence, using rules from Example 1:

Ring() ⇐ νy1νy2 . out(y2) • in(y1) (Chain(y1, y2)) ⇐ νy1νy2 . out(y2) • in(y1) (νy 1 1 . out(y1) • in(y 1 1 ) (Comp(y1), Chain(y 1 1 , y2))) ⇐ νy1νy2 . out(y2) • in(y1) (νy 1 1 . out(y1) • in(y 1 1 ) (Comp(y1), out(y 1 1 ) • in(y2) (Comp(y 1 1 ), Comp(y2)))) ⇐ ... ⇐ νy1νy2 . out(y2) • in(y1) (νy 1 1 . out(y1) • in(y 1 1 ) (C(y1), out(y 1 1 ) • in(y2) (C(y 1 1 ), C(y2)))) = t
By applying flattening to the last term, we obtain:

t = νy1νy2 . out(y2)•in(y1)+out(y1)•in(y 1 1 )+out(y 1 1 )•in(y2) (C(y1), C(y 1 1 ), C(y2))
Note that every chain t 1 t 2 . . . is finite, because the height of terms strictly decreases with flattening. The result of flattening is of the form

t def = Γ (B 1 (x 1 ), . . . , B n (x n )), where Γ = m k=1 P k1 (x k1 ) • . . . • P kr k (x kr k ) is an ar- chitecture description, such that each P k ∈ [1, κ] * → P is a port type, x k ∈ {x 1 , . . . , x n }, for all k ∈ [1, m] and ∈ [1, r k ]. Given an injective valuation ν : V 1 → [1, κ] * that
maps variables into distinct nodes of a tree of branching degree κ, we define the architecture Γ (ν)

def = {{P k1 (ν(x k1 )), . . . , P kr k (ν(x kr k ))} | k ∈ [1,
m]} and the behavior:

B t ν def = Γ (ν)(B 1 (ν(x 1 )), . . . , B n (ν(x n ))) (6)
The semantics of the behavioral term b in the rewriting system R is the following set of marked PNs:

[[b]] R def = {B t ν | t ∈ [b] R , ν ∈ V 1 → [1, κ] * injective} (7)
As a remark, the flattening step is required because applying an architecture to a set of components is a global operation; if an interaction P k1 (x k1 ) • . . . • P kr k (x kr k ) occurs as a monomial in the architecture description Γ of a subterm u = Γ (t 1 , . . . , t ) of t and some variable x ki occurs in an instance atom B(x ki ) in t but not in u, the interaction would be ignored if we applied Γ (ν) directly to B t1 ν , . . . , , B t ν , for some injective valuation ν.

The Parametric Safety Problem

Having defined a rewriting-based term algebra for the specification of distributed systems, we move on to the problem of verifying that every behavior generated by a given rewriting system R, starting from a given behavioral term b is safe with respect to a given set of error markings. This problem is challenging, because we ask for a proof of safety that holds for the behavior(s) of every predicateless rewriting of the behavioral term, i.e. for each t ∈ [b] R . Since, even for token-ring systems with finite-state components, the parametric safety problem is undecidable [START_REF] Emerson | Reasoning about rings[END_REF], we resort to a sound but necessarily incomplete solution, that consists in computing inductive invariants.

Structural invariants

In contrast with the classical approach to invariant synthesis, based on a fixpoint iteration in an abstract domain [START_REF] Cousot | Systematic design of program analysis frameworks[END_REF], we consider a particular class of invariants, that can be obtained directly from the syntactic structure of the marked PN representation of behaviors. For this reason, we call these invariants structural. In the following, we define two kinds of such invariants, namely trap and mutex invariants: Note that, since N is boolean, each marking can be represented as a set of places. Moreover, it is easy to check that Θ(N ) and Ω(N ) contain the initial marking m 0 and are closed under the transition relation of the net. Thus both sets are inductive invariants of N , that can be used to prove a safety property, by checking the emptiness of the intersection of the above sets with a set E of error markings.

Definition 2. Given a marked PN N = ( S, T, E , m 0 ), a set θ ⊆ S is a: 1. trap if |θ ∩ m 0 | ≥ 1 and, for any t ∈ T , if |θ ∩ • t| ≥ 1 then |θ ∩ t • | ≥ 1. 2. mutex if |θ ∩ m 0 | =
Our method encodes the families of sets

{Θ(N ) | N ∈ [[b]] R } and {Ω(N ) | N ∈ [[b]] R }
by formulae of WSκS, for a suitable integer constant κ ≥ 1. To prove a parametric safety property given by a WSκS encoding of the E set, a sufficient (but not necessary) condition is that the WSκS formula defining the family of sets {Θ(N

) ∩ Ω(N ) ∩ E | N ∈ [[b]] R } is unsatisfiable.
Since automatatheoretic decision procedures exist for WSκS [START_REF] Thatcher | Generalized finite automata theory with an application to a decision problem of second-order logic[END_REF], we rely on existing provers [START_REF] Henriksen | Mona: Monadic second-order logic in practice[END_REF] to perform this check.

Rewriting trees The crux of the method is to represent each predicateless behavioral term t ∈ [b] R by a tree labeled with the rewriting rules from some rewriting sequence b ⇐ * R t. As will be shown below, each such rewriting tree

x 1 ← 1, x 2 ← 2
Ring() ← νy 1 νy 2 . out(y 2 ) • in(y 1 ) (Chain(y 1 , y 2 )) ( 1)

y 1 ← 11, y 2 ← 122 Chain(x 1 , x 2 ) ← νy 1 1 . out(x 1 ) • in(y 1 1 ) (Comp(x 1 ), Chain(y 1 1 , x 2 )) (3) x 1 ← 1, y 1 1 ← 21, x 2 ← 22 x ← Comp(x) ← C(x) (4) x ← Comp(x) ← C(x) (4) Comp(x) ← C(x) (4) x ← Chain(x 1 , x 2 ) ← out(x 1 ) • in(x 2 ) (Comp(x 1 ), Comp(x 2 )) (2)
Fig. 3. A Rewriting Tree for the Token-Ring System (Def. 3) defines an injective valuation ν : [START_REF] Chen | Learning to prove safety over parameterised concurrent systems[END_REF]. Since each term t ∈ [b] R can be represented by a rewriting tree (Prop. 1), it follows that each behavior N ∈ [[b]] R corresponds to a rewriting tree (up to a permutation of component identifiers). Our encoding uses rewriting trees T as backbone parameters for the definition of the trap (Θ(N (T ))) and mutex (Ω(N (T ))) invariant, respectively, where N (T ) = B t ν is the behavior induced by T . In fact, any injective valuation of the variables is sufficient for safety checking, provided that the safety properties considered are defined by sets of error markings that are closed under permutations of component identifiers.

V 1 → [1, κ] * of the bound variables from t (Def. 4) that, in turn, induces a behavior B t ν ∈ [[b]] R (
To simplify technicalities, we assume the existence of a rule A b (x 1 , . . . , x n ) ← b in R, where fv(b) = {x 1 , . . . , x n } and A b is a predicate symbol of arity n not occurring elsewhere in R. We also assume that the constant κ is greater than the number of predicate atoms that occur in any rule of R. Definition 3. Given a rewriting system R and a behavioral term b, a rewriting tree for b is a tree T : [1, κ] * → R, such that:

1. T ( ) = (A b (x 1 , . . . , x n ) ← b)
and, for all nodes w ∈ nodes(T ), such that T (w) = A w (x 1 , . . . , x #(Aw) ) ← b w , the following hold: 2. for all i ∈ [1, # pred (b w )], if pred i (b w ) = A wi (y 1 , . . . , y #(Awi) ) then wi ∈ nodes(T ) and T (wi) = A wi (x 1 , . . . , x #(Awi) ) ← b wi , for some rule of the form A wi (x 1 , . . . , x #(Awi) ) ← b wi from R. 3. for all i ≥ # pred (b w ), we have wi ∈ nodes(T ). We denote by T R b the set of rewriting trees for b in R.

A rewriting tree T induces a characteristic term C [T ] , obtained by the application of the rewriting rules labeling the tree nodes in some order of traversal, and a characteristic valuation ν [T ] , that maps each variable in the term to the node where it is instantiated.

C [T ] def = νy 1 . . . νy n . Γ (C [T↓1] [z 1 1 /x 1 , . . . , z 1 #(A1) /x #(A1) ], . . . , C [T↓m] [z m 1 /x 1 , . . . , z m #(A1) /x #(Am) ])
where

ν [T ] (z i j ) def = i • ν [T↓i] (x j ), for all i ∈ [1, m] and j ∈ [1, #(A i )], such that T ( ) = A(x 1 , . . . , x #(A) ) ← νy 1 . . . νy n . Γ (A 1 (z 1 1 , . . . , z 1 #(A1) ), . . . , A m (z m 1 , . . . , z m #(Am) ))
A consequence of the specific form of rewriting rules (Def. 1) is that each (free or bound) variable y from C [T ] is mapped by ν [T ] to a unique node w ∈ nodes(C [T ] ), such that C [T ] (w) contains an instance atom B(x), where x is substituted with y along the path from the node u that introduces y (take

u = if y ∈ fv(C [T ]
)) to w. For example, Fig. 3 shows the rewriting tree for the rewriting sequence from Example 3; we annotate on the side of the tree the bottom-up definition of the characteristic valuation associating the bound variables y 1 and y 2 with the nodes of the rewriting tree where they are instantiated. Below we show that the set [b] R of predicateless terms obtained by complete rewriting is the same as the set of characteristic terms that correspond to some rewriting tree:

Proposition 1. Given a behavioral term b, we have [b] R = {C [T ] | T ∈ T R b }.
Its proof is an easy consequence of the confluence of the rewriting system, i.e. the order in which the rules are applied to a term does not change the resulting predicateless term.

Encoding Invariants and Error Configurations

We begin by building a WSκS formula that describes an infinite κ-ary tree whose finite prefix encodes a rewriting tree T ∈ T R b . Let us assume that R = {r 1 , . . . , r N }, such that r 1 = (A b (x 1 , . . . , x n ) ← b). We use a designated tuple of second order variables U = U 1 , . . . , U N , where each variable U i is interpreted as the set of tree nodes labeled with the rule r i in T . With this convention, the RTree(U) formula (Fig. 4) defines a rewriting tree:

line (8) states that the sets U are pairwise disjoint and that U 1 is a singleton containing the root of the tree (condition 1 of Def. 3). line [START_REF] Emerson | Reasoning about rings[END_REF] states that the union of the sets U is prefix-closed, i.e. the parent x of each node x. from some U i belongs to some U j , for i, j ∈ [1, N ]. lines ( 10) and ( 11) encode the conditions 2 and 3 of Def. 3, respectively. Clearly, for each model ν of RTree(U), there is a unique rewriting tree, denoted Let

T U ν ∈ T R b , such that nodes(T U ν ) = N i=1 ν(U i ) and T U ν (w) = r i iff w ∈ ν(U i ), for all i ∈ [1, N ]
B i def = P i , S i , I i , ∆ i K i=1
be the set of component types that occur in the rules of R and let Z = Z 1 , . . . , Z K be a tuple of second-order variables, where Z i is interpreted as the set of identifiers of the components of type B i .

RTree(U) def = ∀x . 1≤i<j≤N ¬Ui(x) ∨ ¬Uj(x) ∧ U1(x) ↔ x = ∧ (8) ∀x . i:r i ∈R κ =1 Ui(x. ) → r j ∈R Uj(x) ∧ (9)
∀x .

i:r i =(A (x 1 ,...,x #(A ) )←b ) We encode the markings of N (T ) by a WSκS formula using a tuple of secondorder variables X = X S | S ∈ K i=1 S i , where each X S is interpreted as the set of identifiers of the components currently in state S(w) and define the set

# pred (b ) j=1 Ui(x) → j:pred j (b )=A (ξ 1 ,...,ξ #(A ) ) :r =(A (x 1 ,...,x #(A ) )←b ) U (x.j) ∧ (10) ∀x . i:r i =(A (x 1 ,...,x #(A ) )←b ) κ j=# pred (b )+1 Ui(x) → N =1 ¬U (x.j) (11)
σ X ν def = {S(w) | S ∈ K i=1 S i , w ∈ ν(X S )}.
The following formula constrains the set represented by X to be a marking of N (T U ν ):

mark (X, Z) def = ∀x. S =S ∈ K j=1 S j ¬XS(x) ∨ ¬X S (x) ∧ S∈ K j=1 S j XS(x) ↔ K j=1 Zj(x) inst(Z, U) def = ∀x. K i=1 Zi(x) ↔ j:r j =(A (y)←B i (y)) Uj(x)
Intuitively, mark (X, Z) states that no component can be in two different states (first conjunct) and each component is an instance of some component type (second conjunct). The formula inst(Z, U) above relates the instance indices to the nodes of the rewriting tree where the corresponding instance atoms occur, assuming that the sets U are constrained by RTree(U). Then, for each model ν of mark (X, Z) ∧ inst(Z, U) ∧ RTree(U), the set σ X ν is a marking of N (T U ν ). We proceed with the encoding of invariants and error states, by assuming the existence of a flow formula, that defines the pre-and post-sets of the transitions from a behavior N (T U ν ), formally described next ( §4.2). In the following, the primed copy of the tuple X is denoted as X . Definition 5. Φ(X, X , U) is a flow formula for b and R if, for each model ν of RTree(U), we have ν |= Φ(X, X , U) if and only if

• t = σ X ν and t • = σ X ν , for some transition t of N (T U ν ).
Given a flow formula Φ, the parametric trap invariant TrapInv Φ (X, U) is defined by the formula below:

trap Φ (X, U) def = ∀Y 1 ,Y 2 . Φ(Y 1 , Y 2 , U) ∧ inter (X, Y 1 ) → inter (X, Y 2 ) TrapInv Φ (X, U) def = ∃Z . mark (X, Z) ∧ ∀Y 1 ,Y 2 . init(Y 1 , Z) ∧ inter (Y 1 , Y 2 ) ∧ trap Φ (Y 2 , U) → inter (X, Y 2 )
where the tuples Y i def = Y i S | S ∈ K j=1 Sj , for i = 1, 2, are distinct copies of X. The auxiliary formula init(X, Z) def = mark (X, Z) ∧ K j=1 ∀x . Zj(x) ↔ XI j (x) states that X represents the initial marking of the behavior, whereas inter (X, Y) def = ∃x. K j=1 S∈S j XS(x) ∧ YS(x) means that the sets of places encoded by X and Y, respectively, have a non-empty intersection. Intuitively, the formula trap Φ (X, U) defines the traps (point 1 of Def. 2), whereas TrapInv Φ (X, U) defines the set of markings that intersect with the initial marking and with each trap of the behavior, i.e. the trap invariant (point A of Def. 2.

Mutexes and mutex invariants (points 2 and B of Def. 2) are defined by the formulae:

mutex Φ (X, U) def = ∀Y 1 ,Y 2 . Φ(Y 1 , Y 2 , U) → ¬inter (X, Y 1 ) ↔ ¬inter (X, Y 2 ) single(X, Y 1 ) ↔ single(X, Y 2 ) MutexInv Φ (X, U) def = ∃Z . mark (X, Z) ∧ ∀Y 1 ,Y 2 . init(Y 1 , Z) ∧ single(Y 1 , Y 2 )∧ mutex Φ (Y 2 , U) → single(X, Y 2 )
where single(X, Y)

def = ∃1x . K j=1 S∈S j XS(x) ∧ YS(x)
states that the intersection of the sets of places defined by X and Y is a singleton3 . The following lemma states the correctness of the encoding: Lemma 1. Given a flow formula Φ(X, X , U) and a model ν of RTree(U)∧inst(Z, U), we have:

1. Θ(N (T U ν )) = {σ X µ | µ |= TrapInv Φ (X, U), µ(U • Z) = ν(U • Z)}, 2. Ω(N (T U ν )) = {σ X µ | µ |= MutexInv Φ (X, U), µ(U • Z) = ν(U • Z)}.
In our examples ( §5) we consider two kinds of error sets, defined as:

DeadLock Φ (X, U) def = ∀Y 1 ,Y 2 . Φ(Y 1 , Y 2 , U) → ∃x. K j=1 S∈S j Y 1 S (x) ∧ ¬XS(x) CriticalSection Ξ (X, U) def = ∃x∃y . S,S ∈ Ξ XS(x) ∧ X S (y) ∧ ¬x = y
Intuitively, DeadLock Φ (X, U) defined the deadlock markings, in which no transition of the behavior is enabled and CriticalSection Ξ (X, U) states that no two components are at the same time in a state from a given set Ξ ⊆ K i=1 Si of state types. It is worth mentioning that these sets of error markings are closed under permutations of component indices4 , which makes them suitable for safety checking using our encoding of trap and mutex invariants (with variables mapped to the nodes of the rewriting tree where they occur instantiated, as in Fig. 3).

The Flow of a Behavioral Term

The previous definition of structural invariants relied on the existence of a flow formula Φ(X, X , U), stating that σ X ν and σ X ν are the pre-and post-sets of some transition from the behavior (i.e. marked PN) N (T U ν ), whenever ν is a model of RTree(U)∧Φ(X, X , U) (Def. 5). In this section, we describe the flow formula. In the following, we assume w.l.o.g. that the inductive rules in R are of the form:

A(x1, . . . , x #(A) ) ← νy1 . . . νym . m k=1 P k1 (x k1 ) • . . . • P kr k (x kr k ) (t1, . . . , tn) Φ(X, X , U) def = N =1 π∈Inter(r ) Ψ ,π (X, X , U) (12)
Ψ ,{P 1 (x 1 ),...,Pn(xn)} (X, X , U)

def = ∃y0 . . . ∃yn . U (y0) ∧ (13)
n i=1 r =(A (y i )←B(y i )) Path x i ,y i r ,r (y0, yi, U) ∧ (14)
∀x.

S∈ K j=1 S j XS(x) ↔ • P k =S x = y k ∧ X S (x) ↔ P k • =S x = y k (15)
Fig. 5. Definition of the Flow Formula for the Rewriting System R = {r1, . . . , rN }.

if necessary, by applying the flattening relation [START_REF] Bozga | Checking deadlock-freedom of parametric component-based systems[END_REF] to each rule of R. We denote by Inter(r)

def = {P ki (x ki ) | i ∈ [1, r k ]} | k ∈ [1, m]
the set of sets of port atoms P ki (x ki ), corresponding to the interactions (i.e. the monomials from the architecture) from r.

The flow formula Φ(X, X , U) is given in Fig. 5. Essentially, the formula ( 12) is split into a disjunction of formulae Ψ ,{P 1 (x 1 ),...,Pn(xn)} [START_REF] Kesten | Symbolic model checking with rich assertional languages[END_REF], one for each rule r ∈ R and each set of port atoms {P1(x1), . . . , Pn(xn)}, denoting an interaction (monomial) from r . To understand the formulae [START_REF] Kesten | Symbolic model checking with rich assertional languages[END_REF], recall that each of the variables x1, . . . , xn is mapped to the (unique) node of the rewriting tree containing an instance atom Bi(xi). In order to find this node, we must track the variable xi from the node labeled by the rule r, to the node where this instance atom occurs. This is done by the Path x i ,y i r ,r (y0, yi, U) formulae [START_REF] Khoussainov | Automata Theory and its Applications[END_REF], that holds whenever T U ν is a rewriting tree, uniquely encoded by the interpretation ν of the U variables, and y0, yi are mapped to the source and the destination of a path from a node w ∈ nodes(T U ν ), with label T U ν (w) = r to a node w ∈ nodes(T U ν ), with label T U ν (w ) = r , such that xi and yi are variables that occur in the bodies of r and r , respectively, mapped to the same variable in the characteristic term of T U ν (Def. 4). We describe these paths by an automaton and define Path x i ,y i r ,r (y0, yi, U), by translating this automaton into a WSκS formula.

But first, let us define paths in a tree formally. Given a κ-ary tree T , a path is a finite sequence of nodes ρ = n1, . . . , n ∈ nodes(T ), such that, for all

i ∈ [1, -1], ni+1 is either the parent (ni = ni+1αi) or a child (ni+1 = niαi) of ni, for some αi ∈ [1, κ].
The path is determined by the source node and the sequence (α1, d1) . . .

(α -1 , d -1 ) of directions (αi, di) ∈ [1, κ] × {↑, ↓}, with the following meaning: di =↑ if ni+1αi = ni and di =↓ if ni+1 = niαi.
Given two distinct nodes w1, w2 ∈ nodes(T ), there is a unique minimal path from w1 to w2, labeled by a sequence denoted as ρ(w1, w2). This path climbs from w1 to the greatest common prefix w of w1 and w2, before descending from w to w2.

A path automaton is a tuple A = (Q, I, F, δ), where Q is a set of states, I, F ⊆ Q are the sets of initial and final states, respectively, and

δ ⊆ Q × [1, κ] × {↑, ↓} × Q is a set of transitions q (α,d)
---→ q , with α ∈ [1, κ] being a direction and d ∈ {↑, ↓} indicating whether the automaton moves up or down in the tree. A run of A over ω = (α1, d1) . . . (αn-1, dn-1) is a sequence of states q1, . . . , qn ∈ Q such that q1 ∈ I and qi

(α i ,d i ) ----→ qi+1 ∈ δ, for all i ∈ [1, n -1].
The run is accepting if and only if qn ∈ F . The language L(A) of A is the set of sequences over which A has an accepting run.

A path automaton A = (Q, I, F, δ) corresponds (Lemma 2) to the formula in Figure 6, that can be effectively built from the description of A. Here Q = {q1, . . . , qL} is the

∆A(x, y, Y) def = 1≤i =j≤L ∀z. ¬Yi(z) ∨ ¬Yj(z) ∧ q i ∈I Yi(x) ∧ q j ∈F Yj(y) ∧ (16) L i=1 ∀z . z = y ∧ Yi(z) → j:q i (α,↓) ---→q j Yj(z.α) ∨ j:q i (α,↑) ---→q j ∃z . z .α = z ∧ Yj(z ) ∧ (17) L j=1 ∀z . z = x ∧ Yj(z) → i:q i (α,↓) ---→q j ∃z . z .α = z ∧ Yi(z ) ∨ i:q i (α,↑) ---→q j Yi(z.α) (18)
Fig. 6. Definition of the Path Automaton formula ∆A(x, y, Y) set of states of A and Y = Y1, . . . , YL are second order variables interpreted as the sets of tree nodes labeled by the automaton with q1, . . . , qL, respectively. Intuitively, the first three conjuncts of the above formula ( 16) encode the facts that Y are disjoint (no tree node is labeled by more than one state during the run) and that the run starts in an initial state with node x and ends in a final state with node y. The fourth conjunct [START_REF] Mavridou | Configuration logics: Modeling architecture styles[END_REF] states that, for every non-final node on the path, if the automaton visits that node by state qi, then either the node has a (α, ↓)-child or a (α, ↑)-parent visited by state qj, where qi (α,↓)

---→ qj and qi (α,↑)

---→ qj are transitions of the automaton. The fifth conjunct [START_REF] Reynolds | Separation logic: A logic for shared mutable data structures[END_REF] is the reversed flow condition on the path, needed to ensure that the sets Y do not contain useless nodes, being thus symmetric to the fourth. The following result stems from the classical automata-logic connection5 [14, §2.10]: Lemma 2. Given a tree T with nodes(T ) ⊆ [1, κ] * and a sequence ω ∈ ([1, κ]×{↑, ↓}) * from w1 ∈ nodes(T ) to w2 ∈ nodes(T ), for each valuation ν such that ν(x) = w1 and ν(y) = w2, we have ω ∈ L(A) ⇐⇒ ν |= ∃Y . ∆A(x, y, Y) .

Our purpose is to define path automata that recognize the paths between the node where a bound variable is introduced and the node where the variable is instantiated, in a given rewriting tree. This automaton is directly inferred from the syntax of the rules in R. For each pair of rules r1, r2 ∈ R and variables z1, z2 ∈ V1 that occur in the bodies of r1 and r2, respectively, we define the path automaton

A z 1 ,z 2 r 1 ,r 2 def = (Q, I z 1 r 1 , F z 2 r 2 , δ):
-We associate a state q d r,z to each rule r = A(x1, . . . , x #A ) ← b , each variable z occurring (free or bound) in b and each direction d ∈ {↑, ↓}. The intuition is that the automaton visits the state q d r,z while going up or down, as indicated by the direction d, currently tracking variable z in rule r. -The sets of initial and final states are

(b) (a) (2, ↓) q ↓ 2,x 1 q ↓ 1,y 2 (2, ↓) (1, ↓) q ↓ 1,y 1 q ↓ 4,x (1, ↓) q ↓ 3,x 1 (2, ↓) q ↓ 3,x 2 q ↓ 2,x 2 q ↓ 4,x (2, ↓) (1, ↓) (1, ↓)
I z 1 r 1 def = {q d r 1 ,z 1 | d =↑, ↓} and F z 2 r 2 def = {q ↓ r 2 ,z 2 }.
In other words, the automaton starts to track z1 in r1, moving either up or down and it ends tracking z2 in r2, while moving down.

-The transitions are q ↓ r 1 ,y j

(α,↓) ---→ q ↓ r 2 ,x j , q ↑ r 2 ,x j (α,↑)
---→ q ↑ r 1 ,y j and q ↑ r 2 ,x j (α,↑)

---→ q ↓ r 1 ,y j , for any two distinct rules ri = (Aj(x1, . . . , x #(A) ) ← bi), i = 1, 2, all α ∈ [1, # pred (b1)], such that pred α (b1) = A2(y1, . . . , y #(A 2 ) ) and all j ∈ [1, #(A2)]. Intuitively, if r1 labels the parent of the node labeled by r2 in the rewriting tree, the automaton can move either: (i) down from tracking yj in r1 to tracking xj in r2, (ii) up from tracking xj in r2 to tracking yj in r1, or (iii) change direction from moving up tracking xj in r2 to moving down tracking yj in r1. In particular, the last case might be needed to accept a path that only goes up in the tree.

Note that a run of a path automaton A z 1 ,z 2 r 1 ,r 2 may have at most one change of direction, by a rule of the form q ↑ r 2 ,x j (α,↑) ---→ q ↓ r 1 ,y j .

Example 4. The paths that track the instantiations of the variables y1 and y2 in a rewriting tree for the term Ring() are depicted in dashed lines in Fig. 3. The path automata that recognize these paths are given in Fig. 7a (y1) and Fig. 7b (y2). The initial states are q ↓ 1,y 1 and q ↓ 1,y 2 , respectively, and the final state is q ↓ 4,x in both cases, where the labels (1-4) of the rewriting rules are the ones from Example 1.

The lemma below shows that these automata recognize exactly the labels of the minimal paths between two nodes: Lemma 3. Let T ∈ TR b be a rewriting tree and wi ∈ nodes(T ) be nodes labeled with the rules T (wi) = Ai(xi,1, . . . , x i,#(A i ) ) ← bi = ri, for i = 1, 2. Then, for all ki ∈ [1, #(Ai)], i = 1, 2, the following are equivalent:

1. x 1,k 1 and x 2,k 2 are substituted by the same variable during the construction of

C [T ] (Def. 4), 2. ρ(w1, w2) ∈ L(A x 1,k 1 , x 2,k 2 r 1 ,r 2 ). The path automata A x 1,k 1 , x 2,k 2 r 1 ,r 2 are used to define the Path z 1 ,z 2 r 1 ,r 2 formulae: Path z 1 ,z 2 r 1 ,r 2 (x, y, U) def = ∃Y . ∆ A z 1 ,z 2 r 1 ,r 2 (x, y, Y) ∧ Υ (Y, U) Υ (Y, U) def = d=↑,↓ i:r i =(A (x 1 ,...,x #(A ) )←b ) z∈fv(b ) ∀x . Y d r,z (x) → Ui(x)
The formula Υ (Y, U) above states that all nodes labeled with a state q d r,z during the run must be also labeled with r in the rewriting tree given as input to the path automaton. The lemma below proves that Φ(X, X , U) (12) is indeed a flow formula (Def. 5): Lemma 4. For each model ν of RTree(U), we have ν |= Φ(X, X , U) if and only if σ X ν = • t and σ X ν = t • for some transition t of N (T U ν ). Together with Lemma 1, this ensures that the trap and mutex invariant of the parametric system described by b and R are defined by the TrapInv Φ (X, U) and MutexInv Φ (X, U) formulae, respectively. Hence a sufficient condition that proves a safety property of the parametric system described by b and R is the unsatisfiability of a WSκS formula, obtained from the syntax of b and R: Theorem 1. Let b be closed behavioral term, R be a rewriting system and E(X, U) be a WSκS formula. The behavior

N (T U ν ) is safe w.r.t. the set {σ X µ | µ |= E(X, U), µ(U) = ν(U)}, for any valuation ν, if the formula RTree(U)∧TrapInv Φ (X, U)∧MutexInv Φ (X, U)∧ E(X, U) is unsatisfiable.
In particular, we have experimented with error sets defined by the DeadLock Φ (X, U) and CriticalSection Ξ (X, U) formulae, for some critical section given by Ξ ∈ K i=1 Si.

Experimental Evaluation

We implemented the structural invariant synthesis in a prototype tool 6 . Table 1 shows the results of checking deadlock freedom in all test cases and absence of critical section violations, for those test cases where a critical section was defined (otherwise marked n/a). The 2nd column gives the number of states in the system, in the form n1×. . .×nK , where ni is the number of states in the i-th component type and K is the number of component types. The number of rewriting rules and interactions in the specification are given in the 3rd and 4th columns, respectively. The 5th and 7th columns report the results of the satisfiability check ( means that the formula is unsatisfiable and × means that a counterexample has been found, in which case safety could not be proved using our method) for deadlock freedom and absence of critical section violations, using the Mona v1.4-18 tool [START_REF] Henriksen | Mona: Monadic second-order logic in practice[END_REF]. The 6th and 8th columns show the total running times (in seconds) on an iMac 3,4 GHz with 32 GB of RAM, respectively (∞ means that Mona has run out of memory). The 9th column gives the branching degree κ ∈ {1, 2} of trees in the WSκS logic. Note that star and token ring systems require κ = 1, whereas the tree-structured systems require κ = 2. The test cases we consider are grouped according to the architectural pattern. Token rings (Fig. 1a) consist of instances of the same component type, such that the out port of a component is connected to the in port of the next component in the ring. Dining philosophers are special cases of token rings, consisting of alternating philosopher and fork instances. Stars consists of a single controller (master) sending requests and receiving replies from one or more slaves connected to it. Concerning trees, the tree-dfs example models a binary tree architecture traversed by a token in depth-first order, while tree-back-root and tree-linked-leaves(-generic) go beyond trees, modeling hierarchical systems with parent-children communication on top of which the nodes communicate with the root and the leaves are linked in a token-ring, respectively. These examples could not have been described using first order logic, as in [START_REF] Bozga | Structural invariants for the verification of systems with parameterized architectures[END_REF]. The verification problems considered could be solved in less than 1 second, with the exception of the critical section violations for the tree-linked-leaves(-generic) examples, that require mutex, in addition to trap invariants. In particular, in the examples marked with -generic, the initial state of the components is arbitrary. Consequently, all these examples violate the critical section initially. Traditionally, verification of unbounded networks of parallel processes considers known architectural patterns, typically cliques or rings [START_REF] German | Reasoning about systems with many processes[END_REF][START_REF] Browne | Reasoning about networks with many identical finite state processes[END_REF]. Because the price for decidability is drastic restrictions on the shape of architectures [START_REF] Bloem | Decidability of Parameterized Verification[END_REF], more recent works propose practical semi-algorithms, e.g. regular model checking [START_REF] Kesten | Symbolic model checking with rich assertional languages[END_REF][START_REF] Abdulla | Regular model checking without transducers (on efficient verification of parameterized systems)[END_REF] or automata learning [START_REF] Chen | Learning to prove safety over parameterised concurrent systems[END_REF].

Here the architectural pattern is implicitly determined by the class of language recognizers: word automata encode pipelines or rings, whereas tree automata describe trees.

A first attempt at specifying architectures by logic is the interaction logic of Konnov et al. [START_REF] Konnov | Parameterized systems in BIP: design and model checking[END_REF], which is a combination of Presburger arithmetic with monadic uninterpreted function symbols, that can describe cliques, stars and rings. More structured architectures (pipelines and trees) can be described using a second-order extension [START_REF] Mavridou | Configuration logics: Modeling architecture styles[END_REF]. As such, these interaction logics are undecidable and have no support for automated verification. Recently, interaction logics that support the verification of safety properties by structural invariant synthesis have been developed. These logics use fragments of first order logic with interpreted function symbols that implicitly determine the shape of the architecture [START_REF] Bozga | Checking deadlock-freedom of parametric component-based systems[END_REF][START_REF] Bozga | Structural invariants for the verification of systems with parameterized architectures[END_REF].

Conclusions and Future Work

We present a formal language for the specification of distributed systems parameterized by the number of replicated components and by the shape of the coordinating architecture. The language uses inductive definitions to describe systems of unbounded size. We propose a verification method for safety properties based on the synthesis of structural invariants able to prove deadlock freedom for a number of non-trivial models.

  only if w ∈ nodes(T ) and wj ∈ nodes(T ) for all j ∈ [1, i -1]. The root of T is the empty sequence , the children of a node w ∈ nodes(T ) are {wi ∈ nodes(T ) | i ∈ [1, κ]} and the parent of a node wi, i ∈ [1, κ], is w. The leaves of T are leaves(T ) def = {w ∈ nodes(T ) | w.1 ∈ nodes(T )}. The subtree of T rooted at w is defined by nodes(T ↓ w ) def = {w | ww ∈ nodes(T )} and T ↓ w (w ) def = T (ww ), for all w ∈ nodes(T ↓ w ).

P 2 -

 2 → S 2 , if P 1 = P 2 then S 1 = S 2 and S 1 = S 2 . For a transition rule S P -→ S ∈ ∆, let • P def = S and P • def = S denote the pre-and post-state type of the unique transition rule whose label is the port type P . The replicas of a component type are indexed (distinguished) by tree nodes 2 . Given a component type B = P, S, I, ∆ and a tree node w ∈ [1, κ] * , we define the component B(w) def = {P (w) | P ∈ P}, {S(w) | S ∈ S}, I(w), {S(w) P (w) ---→ S (w) | S P -→ S ∈ ∆} . Note that the sets of ports {P (w) | P ∈ P} (resp. states {S(w) | S ∈ S}) of different replicas of the same component type are disjoint, because the port (state) types are required to have disjoint ranges. We slightly abuse notation by writing • (P (w)) def = • (P )(w) and (P (w))

1 r⇐ b 2

 12 b size(b). Given behavioral terms b 1 and b 2 , we denote by b the rewriting step that obtains b 2 by replacing a predicate atom A(y 1 , . . . , y #(A) ) in b 1 with b[y 1 /x 1 , . . . , y #(A) /x #(A) ], where r = (A(x 1 , . . . , x #A ) ← b) is a rule of R and all bound variables in b are renamed to avoid clashes with the variables from b 1 . We write [b] R for the set of predicateless terms obtained from b by exhaustively applying the rewriting rules from R to it.

  1 and, for any t ∈ T , we have |θ ∩ • t| = |θ ∩ t • | ≤ 1. The structural invariants of N are the trap and mutex invariants, repectively: A. Θ(N ) def = {m marking of N | |m ∩ θ| ≥ 1, for each trap θ of N } B. Ω(N ) def = {m marking of N | |m ∩ θ| = 1, for each mutex θ of N }.

Definition 4 .

 4 Given a rewriting tree T ∈ T R b , the characteristic term C [T ] and characteristic valuation ν [T ] are defined inductively on the structure of T : if nodes(T ) = { }, then C [T ] def = B(x) and ν [T ] (x) def = , for T ( ) = (A(x) ← B(x)), else, let 1, . . . , m be the children of the root of T and let:

  and w ∈ nodes(T U ν ). As said, a rewriting tree T ∈ T R b defines a behavior (i.e. a marked PN) denoted by N (T ) def = B t ν (6), where t = C [T ] is the characteristic term and ν = ν [T ] is the characteristic valuation of T (Def. 4). An invariant of N (T ) is a set of markings, i.e. a set of sets of marked places from different components.

Fig. 4 .

 4 Fig. 4. The Definition of Rewriting Trees

Fig. 7 .

 7 Fig. 7. Path Automata Recognizing the Instantiation Paths from Example 1

  It is known that R(N ) is the least inductive invariant of N , thus N is safe w.r.t E if it has an inductive invariant M disjoint from E. Components In this paper we are concerned with systems consisting of an unbounded number of components that are replicas of a fairly small set of patterns, called component types. Let P = {a, b, . . .} and S = {s, t, . . .} be countably infinite sets of ports and states, respectively. An injective function P (resp. S) mapping tree nodes to ports (resp. states) is called a port type (resp. state type). A component type is a tuple B = P, S, I, ∆ , where P ⊆ [1, κ] * → P and S ⊆ [1, κ] * → S are finite sets of port and state types, I ∈ S is the initial state type, and ∆ is a finite set of transition rules S

	and only if m 0 ∈ M and for each m	t -→ m such that m ∈ M, we have m ∈ M.
			P -→ T , where S, T ∈ S and P ∈ P.
	In addition, we require that (i) the elements of P (resp. S) have pairwise disjoint
	ranges and (ii) for any two transition rules S 1	P 1 -→ S 1 , S 2
			t. E if and only if
	R(N ) ∩ E = ∅. A set of markings M is an inductive invariant of N = (N, m 0 ) if

Table 1 .

 1 Experimental Results

	Example	#states	#rules #interaction deadlock time critical time κ
				types	freedom (secs) section (secs)
	token-ring	2 × 2	3	3		0.66		0.63 1
	token-ring-generic	2 × 2	5	4		0.75	×	0.72 1
	sync-philo	2 × 2	3	6		0.69		0.67 1
	alt-philo-sym	3 × 2	3	9	×	0.75		0.77 1
	alt-philo-asym	3 × 2	3	9		0.84		0.78 1
	alt-philo-generic	3 × 2	4	12		0.91		0.87 1
	star	2 × 2	3	4		0.58	n/a	-	1
	star-ring	2 × 3 × 3	3	9		0.75		0.76 1
	star-ring-generic	2 × 3 × 3	5	12		0.84	×	0.88 1
	tree-dfs	2 × 6 × 2	4	6		0.70	n/a	-	2
	tree-back-root	2 × 2	3	5		0.60	n/a	-	2
	tree-linked-leaves	2 × 2 × 4 × 3	4	10		1.05		1.21 2
	tree-linked-leaves-generic 2 × 2 × 4 × 3	7	16		1.31	×	1.73 2
	6 Related Work

First and last are understood here in the order of unfolding of the rewriting rules.

We identify components by tree nodes in preparation of the ground for the verification technique from §4. However, these definitions can be given in general, for any countably infinite set of identifiers.

∃1x . φ(x) is a shorthand for ∃x . φ(x) ∧ ∀x∀y . φ(x) ∧ φ(y) → x = y.

This is the case for every WSκS formula consisting of equality and membership atoms, without successor functions.

A similar conversion of tree walking automata to MSO has been described in[START_REF] Iosif | The tree width of separation logic with recursive definitions[END_REF].

https://github.com/raduiosif/rtab


S Tkachenko

P Arhipov

I Gerasymov

E Galenin

A Shaposhnyk

O Hryshyna

P Mateychenko

Y Boyarintseva

O Zelenskaya

K Lebbou

B Grynyov

O Sidletskiy
email: sidletskiy@isma.kharkov.ua

Crystal growth of ortho-and pyrosilicates from W and Mo crucibles

Ir-consuming expensive growth technology is the main obstacle at widening the area of ortho-and pyrosilicate crystals application. Possibilities to grow silicate single crystals from melt using Mo or W crucibles in crystallizers with graphite heaters are evaluated. Such feasibility is shown on the examples of Y 2 SiO 5 :Ce (YSO:Ce) and La 2-x Gd x Si 2 O 7 :Ce (LaGPS:Ce) scintillation crystals. Application of Edge-defined film-fed growth (EFG) method for silicates growth is limited owing to non-stoichiometry because of the interaction of CO-containing atmosphere with the melt and crystals. The bulk YSO:Ce and LaGPS:Ce crystals are grown by the Bridgman and Czochralski methods for the first time using much cheaper (compared to Iridium) molybdenum (Mo) or tungsten (W) crucibles. The optical and scintillation parameters of the obtained crystals are determined and compared to the counterparts grown by the conventional Czochralski process in Ir crucibles. The ways of further optimization of technological processes are discussed.

Introduction

Crystals of rare-earth silicate complex oxides are widely used in scintillator and laser applications. Ce-doped orthosilicates Lu 2 SiO 5 (LSO:Ce), Lu 1-x Y x SiO 5 (LYSO:Ce), Y 2 SiO 5 (YSO), Gd 2 SiO 5 (GSO) Lu 1-x Gd x SiO 5 (LGSO:Ce) are very popular scintillation materials with the density of up to 7.4 g/cm 3 , high light yield up to 38000 phot/MeV, a good energy resolution (7 -9% at the 662 keV energy), and short luminescence decay time of 35 -80 ns [1][2][3]. The main areas of orthosilicates application are medical PET tomographs [4] and high energy physics experiments [5]. Recently, Ce-doped disilicates (pyrosilicates) such as Gd 2 Si 2 O 7 (GPS), La 2-

x Gd x Si 2 O 7 (LaGPS) have been developed. Despite the lower density and stopping power compared to the orthosilicates they provide even higher light yield of up to 40000 phot/MeV and better energy resolution up to 4.4 % [6]. Orthosilicates doped with Yb 3+ were proposed as laser media [7], and Dy 3+ and Sm 3+ -doped LSO, GSO and their solid solutions are promising white light emitters [8,9].

The melting points of the Ln 2 O 3 -SiО 2 compounds (Ln -lanthanide, or Y) are high -Т m =1900 -2100 С in orthosilicates Ln 2 SiО 5 and Т m = 1740 -1860 С in pyrosilicates Ln 2 Si 2 O 7 [10].

Large LSO, LYSO, GSO, LGSO crystals with the diameters up to 100 mm are successfully grown by the Czochralski method under inert atmosphere of Ar or N using Ir crucibles [11 -15], whereas the crystallizers are constructed from Al 2 O 3 or Y 2 O 3 thermal insulating ceramics. High Ir cost and limited crucible lifetime have a significant impact on crystal cost and limit scaling up of their production. Most the attempts of using cheap Mo and W crucibles were not successful.

Few works are known on the melting and crystallization of yttrium silicates in W crucibles [16].

Interaction of orthosilicate and rare earth garnet melts with Mo was studied in [17]. It was shown that Y 3 Al 5 O 12 (YAG) and Lu 3 Al 5 O 12 (LuAG) melts weakly interact with Mo that was supported by the growth of shaped plates with the length up to 320 mm by the EFG method. Orthosilicate and Ga-containing garnet crystals were not obtained owing to the melt interaction with Мо [17].

The mechanisms of orthosilicate and pyrosilicate melts interaction with Mo and W were not discussed.

The intensity of silicate melt interaction with the crucible material depends on their stability under certain conditions. The stability of melted Y 2 O 3 and SiO 2 under Ar, Ar+O 2 , and wet conditions in equilibrium with their vapours was studied in [18] at temperatures up to 1700 К based on thermodynamic calculations. Under Ar atmosphere, evaporation of Y 2 O 3 and SiO 2 leads to the formation of gaseous YO, О, SiO 2 , O, О 2 and SiO compounds. Partial pressures of these substances in equilibrium above Y 2 O 3 is by 5 orders of magnitude lower than that above SiO 2 . So, Y 2 O 3 is much stable than SiO 2 in Ar atmosphere. In Ar+O 2 (n Ar = 0,8 mole, n O2 = 0,2 mole, note the similar oxygen concentration in air) the volatility of Y 2 O 3 and SiO 2 leads to the formation of gaseous YO 2 , SiO 2 and SiO. YO 2 partial pressure in equilibrium with Y 2 O 3 is by several orders higher than those of SiO 2 and SiO. Therefore, Y 2 O 3 is less stable in air than SiO 2 .

Finally, in the wet conditions (n Ar = 0,4 mole, n O2 = 0,1 mole, n H2O = 0,5 mole) the reactions of evaporating of Y 2 O 3 and SiO 2 with water vapour lead to the formation of gaseous YOOH, Y(ОН) 3 , YO 2 , Si(OH) 4 , SiO(ОН) 2 , SiO 2 , and SiO. At 1300-1700 C temperatures in the wet conditions SiO 2 is more stable than Y 2 O 3 . Therefore, interactions of the lanthanide oxides and SiO 2 with W and Mo should be evaluated in the conditions of current experiment.

Silicate melts themselves can be the origin of W and Mo oxidation, namely excessive oxygen is formed at non-equilibrium dissociation of silica. The literature data collected in Table 1 show that the Р О and Р О2 partial pressures at SiO 2 dissociation are higher than equilibrium pressure above the W -WO 3 system (Table 1), and YSO melt should react with tungsten leading to its oxidation.

Table 1. Calculated pressure and equilibrium dissociation constants of silicon oxides, and Mo and W-containing compounds.

Metallic tungsten is inevitably formed in melt at the presence of WO 2 , because the upper limit of WO 2 thermal stability is 1530 °С [START_REF] Samsonov | The Oxide Handbook[END_REF][START_REF] Giraudon | [END_REF]. Additionally, metallic tungsten may form by the disproportionation (Eq . 1), or as the result of interaction between the oxides [START_REF] Giraudon | [END_REF] (Eq. 2):

1.5 WO 2(g)  WO 3(g) + 0.5W (s) (1) WO 2(g) + WO (g)  WO 3(g) + W (s) ( Mo crucibles of 50 mm in diameter were filled with 50-330 g of raw materials. The reducing atmosphere was formed due to the interaction between graphite and residual oxygen in the growth camera, as well as oxygen formed at dissociation of oxides in raw material. In the Czochralski process the pulling rates were 0.5-1.5 mm/hour and the crystal rotation rates were 6-12 rpm, whereas in the Bridgman the crucible translation rate was 1-2 mm/hour, and in the Edge-Defined Film-Fed Growth (EFG) the pulling rates were 5-15 mm/hour. The seeding in Czochralski method was made on W wire, a crystalline seed with random orientations were used in EFG method, while no seed was used in the Bridgman process.

CrystEngComm Accepted Manuscript

Published on 12 November 2020. Downloaded by Université Claude Bernard Lyon on 11/16/2020 8:41:27 AM.

View Article Online DOI: 10.1039/D0CE01128B

Determination of crystalline structure and composition

Crystalline structures were determined by the X-ray diffraction method. The FullProf&WinPLOTR program [START_REF] Rodriguez-Carvajal | Commission for Powder Diffraction[END_REF] was used for the Rietveld refinement of powder pattern. The Al 2 O 3 plate (NIST SRM1976) was used as external standard to determine the instrumental profile function.

Morphology and element composition of sample surfaces were controlled by a JSM-6390LV scanning electron microscope (SEM) with AZtechEnergy X-max n 50 microanalysis system (EDS). Structure and phase composition were determined with a Siemens D500 diffractometer. Admixture content was controlled by an ElvaX Light X-Ray Fluorescence Spectrometer.

Optical and scintillation characterization

Absorption spectra in UV-VIS regions were recorded by a SPECORD 40 (Analytic Jena) spectrophotometer. X-ray luminescence spectra were measured in reflection mode with X-ray tube and photodetector Hamamatsu R1926A located at the same side from the samples under a steady-state X-ray excitation (Ag anode, 40 kV, 40 μA). Emitted light was dispersed with a monochromator (grating 1200 grooves/mm). Obtained spectra were not corrected for the spectral sensitivity of the detection system.

Light yield (LY) and energy resolution (R) were measured under irradiation with a 662 keV 137 Cs gamma source. A R1307 Hamamatsu PMT ran at 800 V and HV with linear dynode voltage divider were used for registration of YAG:Ce,C parameters. The shaping time was 2 µs.

PMT output was connected to the charge-sensitive preamplifier BUS 2-94 and BUI-3K shaping amplifier. Signal from preamplifier was shaped by a shaping amplifier with 2 µs shaping times.

In order to collect the whole scintillation light the samples together with open part of PMT photocathode were covered with Teflon reflector. No optical contact between samples and PMT window was provided. For absolute light yield determination the yields were compared to Bi 4 Ge 3 O 12 (BGO) produced by a standard technology by the Czochralski method. Energy resolution was determined as FWHM of the 137 Cs 662 keV photopeak at pulse-height spectra by its approximation with the Gaussian function.

Results and Discussion

Growth of orthosilicates

To evaluate the interaction of YSO melt with tungsten, chunks of crystals obtained from Ir crucibles were melted in W crucible under the Ar+CO atmosphere (Р Ar+CO = 1.02 atm). An opaque grayish-metallic film was formed at melt surface in 40 min after melting as shown in Fig. 1. XRD showed that this film is tungsten (JCPDS#04-0806) with few unidentified admixtures (Fig. 2a). Therefore, tungsten was oxidized, melted, reduced at melt surface, and stuck to the grown crystal. The W film thickness reached 2 µm, and W overall concentration in crystallized melt was 0.1 wt.%. In some experiments W crystallized at the melt-gas boundary in the form of hexagonal stepped cavities (Fig. 1b). In the crystallized melt the gas bubbles were partially covered with metallic tungsten. Additinally, tungsten dendrite branches and inclusions were observed at crystal surfaces (Figure 1c,d SiO 2(l) + CO (g)  SiO (g) + CO 2(g) (3).

Transport of SiO and СО 2 to the graphite heater results in formation of SiC films at graphite surfaces and increase of CO concentration.

SiO (g) + C (s)  SiC (g) + CO (g) (4) CO 2 (g) + C (s)  2CO(g) (5)
СО also interacts with the seed and growing crystal resulting in depletion of their surface layer with SiO 2 . This creates non-stoichiometry in the layer and decreases its melting temperature. The surface layer melts earlier than the bulk and drains off. This is not important in Czochralski method, but critical for EFG growth, because even inessential non-stoichiometry in melt meniscus changes its properties and hinders crystal growth. In our experiments the composition of the depleted surface layer was Y 2,46 Si 0,66 O 5 . Therefore, stoichiometric YSO growth under CO atmosphere is practically impossible.

During Czochralski growth, the crystal is exposed to high temperatures for a long time (up to several days) due to the low pulling rate. This results in a heavy depletion of silica from the surface near the dendrites (see Figure 1c,d) to the Y 3,2 Si 0,1 O 5 (i. e. almost Y 2 O 3 ) composition during 6 hours. There are no available conditions preventing or limiting CO concentration in the YSO-W-C system that strongly complicates the crystal growth. In addition, SiO 2 dissociation is another obstacle at YSO growth from W crucibles.

To reduce the interaction of С and СО with the YSO melt, the crucible with raw material was tightly covered with W lid. Despite no visible inclusions were observed after YSO melting and keeping during 40 minutes the crystallized melt contained 0.01 wt% of W. According to XRD, the melt crystallized into the Y 2 SiO 5 single phase with the I2/a space group (Fig. 2b) and corresponded to the ICSD#28021. Therefore, one may avoid W film formation at the surface and decrease W concentration in bulk by preventing the melt interaction with C and CO. A W crucible with the 18 mm diameter and 30 mm height and with a mechanically fit lid still allowing some reduced gas exchange was fabricated for YSO:Ce growth by the Bridgman method. The chunks of YSO:Ce crystal grown from Ir crucible were used as the raw material.

The crucible translation rate was 2 mm/h. The crystal stuck to the crucible and cracked (Figure 3a). A characteristic Ce 3+ blue phosphorescence in YSO:Ce was observed under UV light (Figure 3b). No W film was observed on the crystal surface. This example illustrates the significant effect of C and CO gas in the tungsten film formation. The role of dissociation decreased under these conditions, because the equilibrium of vapours was reached faster in the closed volume. The concentration of W in the crystal was 0.002 % wt.

Growth of pyrosilicates

Using W crucibles in growth of pyrosilicates is more promising, because the latter possess approximately 200 С lower melting points compared to those in orthosilicates, as well as lower vapour pressure and dissociation rates [START_REF] Kulikov | Thermal dissociation of compounds[END_REF]. Gadolinium-lanthanum pyrosilicate Gd 1.2 La 0.8 Si 2 O 7 was grown by the Czochralski method in W crucible. Mo wire was used as a seed, and the raw material weight was 60 g. The obtained crystal (Figure 4a) contained a lot of bubbles, and its surface became milky after the interaction with CO. No signs of metal at the melt surface were observed after 24 hours of crystal growth (Figure 4b). However, the concentration of W dissolved in the crystallized melt and in crystal reached 0.05 and 0.01 wt%, respectively.

Lowering of melting temperature reduced the W dissolving that excluded the formation of a uniform metal film, but metal particles were observed between the grains in the crystallized melt (Figure 4c). The lower melting temperature of pyrosilicates (1800С) enables usage of Mo crucibles.

Mo crucibles are preferable, because the vapour pressure of Mo oxides is by several orders higher than that of W [START_REF] Alcock | [END_REF], and the Mo vapour pressure is by four orders higher than that of W [28]. The intensive evaporation of Mo and its oxidation decrease the probability of metal film formation at the melt surface. The quantity of dissolved and reduced metal directly depends on the dissociation and the quantity of the loaded raw material into the crucible, and process duration. Then the crucible was loaded with 330 g of raw material and Ce activator was added.

The resulting chemical formula was Ce 0.02 Gd 1.48 La 0.5 Si 2 O 7 . The growth rate was in the range of 0.5 -1 mm/hour. After 100 hours the Mo island remained at the melt surface and most of Mo stuck to crystal surface in the form of wires and spots (Figure 5a). The SiO 2 dissociation continued during the crystal growth, but its intensity was not critically high. Continuous Mo film at the melt surface was not formed; however, the crystal contained a lot of visible macroscopic inclusions (Figure 5b). The characteristic Ce 3+ violet phosphorescence was observed under UV light (Figure 5c). The measured crystal density was 5.274 g/cm 3 . It is comparable with the density of 5.5 g/cm 3 in La 0.2 -Ce 0.05 Gd 1.75 Si 2 O 7 [29] (but note the lower La concentration leading to the density increase in our case). The silicon-depleted milky surface layer reached the thickness of 0.3 mm as the result of interaction with CO. Mo concentrations in the crystallized melt and crystal were 0.04 and 0.013 wt%, respectively. As one can see, the crucible metal concentrations in the melts and crystals are significantly higher in the Czochralski grown La-

Optical and Scintillation parameters

Absorption spectra of LaGPS contain a series of Ce 3+ absorption bands in the UV range. Some of them are not resolved due to the high Ce 3+ concentration. The sharp peaks around 275 nm are attributed to the 8 S 7/2 → 6 I J transitions in Gd 3+ , the same as observed in GSO:Ce [30]. No other distinct bands were observed in the visible and near-IR ranges up to 1100 nm. Absorption YSO:Ce grown from W crucible possesses a typical luminescence band peaked at 425 nm related to 5d-4f radiative transitions in Ce 3+ . The strong long-wavelength shoulder of this peak around 500 nm can be ascribed to oxygen vacancies in the vicinity of Ce 3+ in LYSO:Ce crystal grown under oxygen-poor atmosphere [31], or, as proposed recently [32] to Ce 3+ -Ce 3+ dimers.

X-ray luminescence spectrum of LaGPS:Ce is typical for rare-earth pyrosilicates with the triclinic structure [28,[START_REF] Jary | Channel number BGO LaGPS:Ce[END_REF] and consists of the two bands peaked around 370 and 390 nm ascribed to the same 5d-4f (5d to 2 F 5/2 and 2 F 7/2 states, respectively) radiative transitions in Ce 3+ [START_REF] Jary | Channel number BGO LaGPS:Ce[END_REF]. phot/MeV. Meanwhile, light output of the LaGPS:Ce was 360-370% in respect to a BGO standard that corresponds to 22150 phot/MeV following the light quantum efficiencies at registration with a R1307 PMT. The energy resolution at 662 keV energy was 13.9 % for YSO:Ce and 17.3 % for La-GPS. The demonstrated scintillation parameters are worse than the best values obtained with crystals grown in Ir crucibles: up to 26700 phot/MeV and 6.8% in YSO:Ce [3] and 39000 phot/MeV and 5.4 % in La-GPS [6]. Obviously such results are called by the presence of scattering centres and point defects, which nature should be determined in further work.

Summarizing, in this work the crystals were obtained by the Czochralski and Bridgman -the essential methods of industrial crystal growth from melt. Basically, the Czochralski method would be preferable as it provides no contact of crystal with the crucible, good melt convection, growth on a seed, and simple scaling up. We have succeeded in growing LaGPS:Ce crystals by the Czochralski, whereas this process process was hardly possible with YSO:Ce possessing the higher melting temperature. The intense interaction of silicon oxide in YSO:Ce melt with the CO-containing reducing atmosphere results in crucible oxidation and formation of metal film at the melt surface. In the Bridgman method, the melt was protected from the environment by crucible covering with W lid that minimized silicon oxide interaction with the atmosphere. This is confirmed by the order of magnitude lower Mo and W concentrations in the Bridgman-grown crystals (0.002 vs. 0.01-0.013 wt%). However, YSO:Ce ingots grown by the Bridgman without a seed were mainly polycrystalline, and stuck to the crucible after crystallization.

This study is a starting point for further assessment of growth conditions and materials for which the issues could be mitigated. Meanwhile it shows the feasibility to obtain bulk ortho-and pyrosilicate crystals from melt without using expensive Ir crucibles and heat shields. There is a room for improvement of scintillation parameters by minimizing scattering centres and point defect concentrations. For example, La-GPS crystals contain a lot of gas bubbles that definitely deteriorate the luminescence yield. Additionally, the peculiarities of carbon incorporation into these crystals at growth under CO-containing atmosphere should be elucidated. Further work will be devoted to the tuning gaseous atmosphere composition and/or crucible sealing procedure to minimize the light scattering in crystals. The crystal quality eventually may be also improved by using crystalline chunks as raw materials instead of powders.

Conclusions

A feasibility of growing rare earth silicate oxides using W and Mo crucibles with graphite heaters and thermal heat insulation was shown. The process is complicated by the low thermodynamic stability of SiO 2 at temperatures around 2000С and its interaction with CO gas.

The SiO 2 dissociation results in liberation of excessive oxygen and crucible surface oxidation that leads to dissolving of crucible material in the melt and its reduction at the melt surface. The metal film formed at the melt surface constitutes a main barrier for a steady crystal growth under such conditions.

EFG growth technique is practically not implementable using Mo or W crucibles and shapers because of the precise requirements to melt stoichiometry, which are difficult to sustain under critical conditions of melt dissociation and its interaction with CO. We have not succeeded in growing any shaped ortho-or pyrosilicate crystal.

The Czochralski method is less sensitive to the deviations of melt stoichiometry. However, it also suffers from the interaction between SiO 2 and CO, crucible oxidation, as well open melt surface that promotes its interaction with atmosphere. Our experiments showed that bulk pyrosilicate crystals can be grown by the Czochralski from Mo crucibles. Formation of metal film on the melt surface can be avoided by reducing CO content in the growth atmosphere.

The Bridgman growth in closed crucibles is advantageous as it reduces melt dissociation and its interaction with CO. However, this method not provides a visual control over crystallization process, and the problem of crystal sticking to crucible walls is not resolved. The similar approach can be applied as well in other methods of crystal growth in closed or sealed crucibles, such as Temperature Gradient, or Vertical Gradient Freeze Techniques. Meanwhile, all these methods do not exclude the introduction of crucible material and gaseous inclusions into crystals.

YSO:Ce and LaGPS:Ce crystals obtained by the Czochralski and Bridgman methods under the specified conditions show low-to-moderate scintillation parameters owing to the presence of gas bubbles and oxygen vacancies formed in the oxygen-poor atmosphere conditions. There is a good opportunity for the improvement of crystal quality by optimizing technological parameters of the process. For example, La-GPS crystals contain a lot of gaseous bubbles that definitely serve as light scattering centres deteriorate the luminescence yield. Tuning the gaseous atmosphere composition and/or crucible sealing procedure should be helpful in this context.

Figure 1 .

 1 Figure 1. W film on the side surface of the crystal grown on a YSO crystalline seed (a), crystallized tungsten (b), tungsten dendrite branches on a crystallized melt surface (c), (d).

Figure 2 .Figure 3 .

 23 Figure 2. XRD of W film at the surface of crystallized YSO melt (a), and crystallized YSO melt after its heating in W crucible covered with W lid (b).

Figure 4 .

 4 Figure 4. LaGPS:Ce crystal grown from W crucible (a), W crucible with remnants of LaGPS:Ce melt after crystallization (b), fragment of its surface with Mo inclusions (c).

GPS:Figure 5 .

 5 Figure 5. As-grown LaGPS:Ce crystal grown from Mo crucible (a), its parts under illumination with daylight (b) and UV-light (c).

Figure 6 .

 6 Figure 6. (a) Absorption spectra of LaGPS:Ce (in the inset -enlarged view of the UV band), (b) Normalized XRL spectra of the obtained YSO:Ce and LaGPS:Ce crystals. Pulse height spectra of the obtained crystals in comparison with BGO standard 9x9x1.5 mm: (c) 10x3x2 mm size YSO sample and (d) 8x8x1.75 mm La-GPS sample. The difference in BGO spectra in (c) and (d) is related to various amplification coefficients and dynode voltages.

  Published on 12 November 2020. Downloaded by Université Claude Bernard Lyon on 11/16/2020 8:41:27 AM.

	Page 11 of 17	CrystEngComm
	spectra were not measured, because YSO:Ce samples contained a lot of inclusions and
		View Article Online
	scattering centres.	DOI: 10.1039/D0CE01128B
		CrystEngComm Accepted Manuscript

Published on 12 November 2020. Downloaded by Université Claude Bernard Lyon on 11/16/2020 8:41:27 AM. View Article Online

Acknowledgements

The work was performed in the frame of the project "Carbon" of the National Academy of Sciences of Ukraine, Reg. No. 0119U100791.

Notes and references

atmospheres. Master's thesis, Norwegian University of Science and Technology, Department of Materials Science and Engineering. Trondheim, 2015, 89 p.


Jie Xu

Qingsong Song

Jian Liu

Kaiting Bian

Wen Lu

Dongzhen Li

Peng Liu

Xiaodong Xu

Yuchong Ding

Jun Xu
email: xujun@mail.shcnc.ac.cn

Kheirreddine Lebbou
email: kheirreddine.lebbou@univ-lyon1.fr

The micro-pulling-down growth of Eu 3+ -doped Y 3 Al 5 O 12 and Y 3 ScAl 4 O 12 crystals for red luminescence

Keywords: Eu:YAG, Eu:Y 3 ScAl 4 O 12, Micro-pulling-down technique, Spectral property

We report on the comparative growth and spectroscopy of Eu 3+ -doped Y 3 Al 5 O 12 (YAG) and Y 3 ScAl 4 O 12 crystals grown by the micro-pulling-down (μ-PD) method. The structure of the as-grown crystals was determined by X-ray diffraction (XRD) and Raman spectroscopy. The spectra of the crystals are dominated by a strong line centered at 395 nm, matching well with the emission of commercial ultraviolet laser diodes. The Eu:YAG and Eu:Y 3 ScAl 4 O 12 crystals exhibit strongest red emission centered at 710 nm and the full width at half maximum (FWHM) was calculated to be 2.03 and 3.19 nm, respectively. The fluorescence decay curves of 5 D 0 levels were measured and discussed. All the results indicate that the Eu:YAG and Eu:Y 3 ScAl 4 O 12 crystals are promising candidates for red luminescent/laser materials.

Introduction:

In recent years, the red luminescent materials have attracted much attention because of their potential applications in white light-emitting diodes (W-LEDs), field emission display (FED), vacuum fluorescent displays (VFDs), plasma display panels (PDP) [START_REF] Zhong | Eu 3+ -doped double perovskite-based phosphor-in-glass color converter for high-power warm w-LEDs[END_REF][START_REF] Ravichandran | Fabrication of Y 3 Al 5 O 12 :Eu thin films and powders for field emission display applications[END_REF][START_REF] Ruan | Synthesis of Y 3 Al 5 O 12 :Eu phosphor by sol-gel method and its luminescence behavior[END_REF][START_REF] Sharma | Performance of YAG:Eu 3+ , YAG:Tb 3+ and BAM:Eu 2+ plasma display nanophosphors[END_REF]. As one of the most popular used red emitting activators, the trivalent europium ion (Eu 3+ ) exhibits characteristic emissions which are associated to the f-f transitions form the excited level 5 D 0 to lower levels 7 F J (J=0, 1, 2, 3, 4). Up to now, the Eu 3+ -doped phosphors, such as Eu:YAG [START_REF] Su | Phase transition, structure and luminescence of Eu:YAG nanophosphors by co-precipitation method[END_REF], Eu:Sr 3 Bi(PO 4 ) 3 [START_REF] Dong | Synthesis and photoluminescence properties of the high-brightness Eu 3+ -doped Sr 3 Bi(PO 4 ) 3 phosphors[END_REF], Eu:Ca 9 ZnK(PO 4 ) 7 [START_REF] Cao | Study on the photoluminescence properties of a color-tunable Ca 9 ZnK(PO 4 ) 7 :Eu 3+ phosphor[END_REF], Eu:Na 3 Sc 2 (PO 4 ) 3 [START_REF] Guo | Synthesis and photoluminescence properties of novel highly thermal-stable red-emitting Na 3 Sc 2 (PO 4 ) 3 :Eu 3+ phosphors for UV-excited white-light-emitting diodes[END_REF], and Eu:Ca 3 Y(AlO) 3 (BO 3 ) 4 [START_REF] Guo | High-efficiency and thermal-stable Eu 3+ -activated Ca 3 Y(AlO) 3 (BO 3 ) 4 red-emitting phosphors for near-UV-excited white LEDs[END_REF] have merited considerable attention due to potential applications in red emission. However, it is well known that phosphors have many drawbacks, such as lower uniformity, deficiency of red emission, light scattering and encapsulation difficulty. Therefore, in order to overcome the above disadvantages, search for new red luminescent materials which have better optical properties and chemical stability become an urgent task. The preparation and spectral properties of Eu:YAG ceramics [START_REF] Liu | Preparation and properties of transparent Eu:YAG fluorescent ceramics with different doping concentrations[END_REF], Eu:Gd 3 Sc 2 Ga 3 O 12 nanocrystalline [START_REF] Shao | Preparation, structure and luminescence properties of nanocrystalline Eu:Gd 3 Sc 2 Ga 3 O 12[END_REF], Eu:CaGdAlO 4 crystal [START_REF] Li | Crystal characterization and optical spectroscopy of Eu 3+ -doped CaGdAlO 4 single crystal fabricated by the floating zone method[END_REF], Eu:YAl 3 (BO 3 ) 4 crystal [START_REF] Ben Amar | Optical spectroscopy of Eu 3+ ions doped in YAl 3 (BO 3 ) 4 crystal[END_REF], Er:KGd(WO 4 ) 2 crystal [START_REF] Dashkevich | Quasi-continuous wave and continuous wave laser operation of Eu:KGd(WO 4 ) 2 crystal on a 5 D 0 → 7 F 4 transition[END_REF] and Eu:Bi 4 Ge 3 O 12 crystal [START_REF] Li | Spectroscopic properties of Eu:Bi 4 Ge 3 O 12 single crystal grown by the micro-pulling-down method[END_REF] have been reported for exploring new luminescent/laser materials.

Y 3 ScAl 4 O 12 belongs to the disordered material in which the Sc 3+ and Al 3+ ions randomly occupy the same lattice site, which leads to inhomogeneous broadening of absorption and emission spectra [START_REF] Sato | Spectral parameters of Nd 3+ -ion in the polycrystalline solid-solution compared of Y 3 Al 5 O 12 and Y 3 Sc 2 Al 3 O 12[END_REF][START_REF] Ma | Generation of sub-100-fs pulses from a diode-pumped Yb:Y 3 ScAl 4 O 12 ceramic laser[END_REF][START_REF] Feng | Dual-wavelength synchronously mode-locked laser of a Nd:Y 3 ScAl 4 O 12 disordered crystal[END_REF][START_REF] Xu | Spectroscopic characteristics of Dy 3+ -doped Y 3 Al 5 O12 (YAG) and Y 3 ScAl 4 O 12 (YSAG) garnet single crystals grown by the micro-pulling-down method[END_REF]. Y 3 ScAl 4 O 12 has been realized as a valuable material thanks to its high optical, excellent chemical and mechanical characteristics. To the best of our knowledge and in spite of the possibilities to crystalize this material from the melt, up to now there has no research about the growth and performance of Eu:Y 3 ScAl 4 O 12 crystal.

In this paper, we select to study two Eu 3+ -doped garnet hosts (YAG and Y 3 ScAl 4 O 12 ). They crystallize in Ia3d of the cubic crystal system. In these two materials, Y 3+ and Al 3+ can be substituted by different types of cations with different sizes and valences up to certain concentration. In this work, attention was focused to grow Eu 3+ -doped YAG and Y 3 ScAl 4 O 12 crystals were by the micro-pulling-down (μ-PD) technique for the first time. The structure of two crystals were studied by X-ray diffraction (XRD). The spectroscopic properties of two crystals were also investigated.

Experimental

The Eu 3+ -doped YAG and Y 3 ScAl 4 O 12 single crystals were grown by the μ-PD method [START_REF] Xue | Spectroscopic and laser properties of Tm:CNGG crystals grown by the micro-pulling-down method[END_REF][START_REF] Song | Laser operation in a Tm:LuAG crystal grown by the micro-pulling-down technique[END_REF][START_REF] Song | Structure and white LED properties of Ce-doped YAG-Al 2 O 3 eutectics grown by the micro-pulling-down method[END_REF][START_REF] Wang | High-performance Ho:YAG single-crystal fiber laser in-band pumped by a Tm-doped all-fiber laser[END_REF] , respectively, and then ground and mixed thoroughly in an agate mortar. The mixtures were shaped into a rod and pressed by cold isostatic at 160 MPa for 2 min, then sintered at 1300 ℃ for 20 h in air. A <111> oriented YAG crystal was used as seed, the pulling rate was 0.3 mm/min and the growth atmosphere was high-purity flowing argon. A small portion of as-grown crystals were ground into powders and the powders were carried out in the 2θ range of 20°-90° by X-ray diffraction method (XRD, Bruker-D2, Germany) at room temperature. The Raman spectra were obtained with a laser Raman spectrometer (Omni-λ 300i, Zolix) in the range of 16-900 cm -1 at 30 MV with a 785 nm excitation light source. The absorption spectra of Eu:YAG and Eu:Y 3 ScAl 4 O 12 crystals were recorded with a UV-VIS-NIR spectrophotometer (Lambda 900, Perkin -Elmer UV-VIS-NIR) in the range of 300-450 nm. The fluorescence spectra, as well as the lifetime were recorded using Edinburgh Instruments FLS980 spectrophotometer under 394 nm excitation. All the measurements were taken at room temperature. The samples were cut from the as-grown crystals and two surfaces perpendicular to the <111>-growth axis was polished for spectral measurements. The spectral measurements were detected in the core (diameter of 0.5 mm) of the samples.

Results and discussions 3.1 Crystal growth

After growth the crystals were cooled to room temperature during 3 h. As shown in Fig. 1, as-grown Eu:YAG and Eu:Y 3 ScAl 4 O 12 crystals with diameter of about 2 mm were crystallized. We obtain blue transparent Eu 3+ -doped YAG crystal (Fig. 1a) and slightly dark brown Eu 3+ -doped Y 3 ScAl 4 O 12 crystal (Fig. 1b), with homogeneous diameter and free of macroscopic defects. During the growth process, the melt meniscus thickness under the capillary die did not exceed 250 µm, it is considered a good value for a stable growth. The length of the grown fibers reached 10 cm while 100% of the melt in the crucible was crystallized. We did not record any macro-scale shift from the <111> initial orientation.

Crystal structure

The corresponding XRD patterns are shown in Fig. 2. All the diffraction peaks matched well with the standard card of YAG (PDF#88-2048), and no impurity peaks were found in the patterns, indicating that the Eu 3+ ions were well diffused in the host lattices and did not change the crystalline structure. The Eu 3+ is expected to substitute Y 3+ into the distorted dodecahedral site and to be coordinated to eight O 2-ions because of their comparable ionic size. The calculated cell parameters of Eu 3+ -doped YAG and Y 3 ScAl 4 O 12 single crystals were a=11.957 Å, and a= 12.053 Å, respectively. The increase in the lattice parameter of YSAG is attributed to the larger ionic radius of Sc 3+ (0.75 Å) compared to Al 3+ ions (0.39 Å). The Raman spectra of Eu 3+ -doped YAG and Y 3 ScAl 4 O 12 single crystals are shown in Fig. 3. The Raman spectra are in consistent with the spectra of Yb:YAG [START_REF] Chen | Raman scattering investigation of Yb:YAG crystals grown by Czochralski method[END_REF] and Nd:Y 3 Sc 2 Al 3 O 12 crystal [START_REF] Ding | 1 micrometer high-efficient radiation resistant laser crystal: Nd:YSAG[END_REF]. The Raman peaks position and intensity are changed after the introduction of Sc 3+ ions in YAG crystal. However, no distinct changes in the modes are observed, which suggests that the crystal structure remains the same. Additionally, the maximum phonon energy of Eu:Y 3 ScAl 4 O 12 was determined to be 768 cm -1 from the Raman spectra, which is lower than that of Eu:YAG (780 cm -1 ).

Optical characterization

The room temperature absorption spectra of Eu 3+ -doped YAG and Y 3 ScAl 4 O 12 crystals in the range from 300 to 450 nm are shown in Fig. 4. The corresponding transitions from the 7 F 0 , 7 F 1 ground state to excited state were assigned and marked. The absorption spectra of Eu:YAG and Eu:Y 3 ScAl 4 O 12 crystals are dominated by a strong line occurring at 395 nm, corresponding to the 7 F 0 → 5 L 6 transition, matching well with the emission of commercial ultraviolet laser diodes. In addition, the absorption coefficient at 395 nm of Eu:YAG and Eu:Y 3 ScAl 4 O 12 was calculated to be 1.07 and 1.12 cm -1 , and the full width at half maximum (FWHM) of absorption band at 395 nm was calculated to be 1.89 and 2.21 nm respectively, which is higher than that of Eu:CaGdAlO 4 (1.62 nm) [START_REF] Li | Crystal characterization and optical spectroscopy of Eu 3+ -doped CaGdAlO 4 single crystal fabricated by the floating zone method[END_REF], but smaller than that of Eu:Bi 4 Ge 3 O 12 (3.1 nm) [START_REF] Li | Spectroscopic properties of Eu:Bi 4 Ge 3 O 12 single crystal grown by the micro-pulling-down method[END_REF]. 5. It's clear that emission bands centered around 591 nm, 610 nm, 650 nm, 710 nm, 743 nm are corresponding to transitions from 5 D 0 excited level to 7 F 1 , 7 F 2 , 7 F 3 , 7 F 4 and 7 F 5 energy level, respectively, and these peaks split into some stark components. The emission in the range (580-600 nm) of Eu 3+ due to the magnetic dipole transition of 5 D 0 → 7 F 1 is not affected much by the site symmetry, because they are partly allowed, while the red emission (605-630 nm) due to the electric dipole transition of 5 D 0 → 7 F 2 is sensitively affected by the site symmetry of Eu 3+ .In Eu:CaGdAlO 4 crystal, the emission of 5 D 0 → 7 F 2 transition is dominant because Eu 3+ ions are located at a non-inversion symmetry position in CaGdAlO 4 crystal [START_REF] Li | Crystal characterization and optical spectroscopy of Eu 3+ -doped CaGdAlO 4 single crystal fabricated by the floating zone method[END_REF]. However, in Eu:YAG and Eu:Y 3 ScAl 4 O 12 crystals, Eu 3+ ions occupy a site with inversion symmetry, which induces the relative weak emission of the 5 D 0 → 7 F 2 transition at 610 nm. Furthermore, the ratio between the integrated intensity of 5 D 0 → 7 F 2 and 5 D 0 → 7 F 1 transitions ( 5 D 0 → 7 F 2 / 5 D 0 → 7 F 1 ) is called asymmetric ratio (R 21 ), which gives information about the surrounding and environmental changes around the Eu 3+ ions. The higher the asymmetric ratio is, the more apart from a centrosymmetric geometry luminescent center is located [START_REF] Ooman | Europium (III) in oxide glasses: Dependence of the emission spectrum upon glass composition[END_REF]. The asymmetric ratio R 21 of Eu:YAG and Eu:Y 3 ScAl 4 O 12 was calculated to be 0.49 and 0.48, which is much higher than that of Eu-doped SnO 2 xerogels with low concentration (0.01 [START_REF] Morais | Photoluminescence of Eu 3+ ion in SnO 2 obtained by sol-gel[END_REF]), but smaller than that of Y 0.7 BO 3 :Eu 0.3 3+ @SiO 2 nanophosphors (6.71 [START_REF] Rambabu | Luminescence optimization with superior asymmetric ratio (red/orange) and color purity of MBO 3 :Eu 3+ @SiO 2 (M = Y, Gd and Al) nano down-conversion phosphors[END_REF]), Eu:YAG microcrystals (1.0 [START_REF] Kolesnikov | Asymmetry ratio as a parameter of Eu 3+ local environment in phosphors[END_REF]) and Eu:YAG nanocrystals (average value 0.75 [START_REF] Kolesnikov | Asymmetry ratio as a parameter of Eu 3+ local environment in phosphors[END_REF]). The observed difference can be explained with more symmetric local environment in Eu:YAG monocrystals compared with Eu:YAG nanocrystals and microcrystals.

The intense emission of the 5 D 0 → 7 F 4 transition at 710 nm suggests that Eu:YAG and Eu:Y 3 ScAl 4 O 12 crystals have potential application in red emission. Besides, The full width at half maximum (FWHM) of emission band at 710 nm was calculated to be 2. To further investigate the fluorescence mechanism, the room temperature fluorescence decay curves of the 5 D 0 level excited by 394 nm were presented in Fig. 7. The measured decay curves showed a single exponential decaying behavior, and the fluorescence lifetimes of Eu:YAG and Eu:Y 3 ScAl 4 O 12 crystals were measured to be 3.19 and 2.97 ms, respectively, which is much longer than that of Eu:CaGd 4 O 7 phosphors (700 μs) [START_REF] Pavitra | Synthesis and luminescent properties of novel red-emitting CaGd 4 O 7 :Eu 3+ nanocrystalline phosphors[END_REF]. The incorporation of Sc 3+ in YAG decrease the life time of the excited state ( 5 D 0 ) in Eu-doped YSAG around 7%. The incorporation of Sc in Eu-doped YAG can slightly affect lattice parameter inducing lattice defects, which can strongly affect the life time. The Sc environment influence the lifetime of Eu 3+ in garnet structure. Eu:tellurite glasses (0.93 ms) [START_REF] Stambouli | Optical and spectroscopic properties of Eu-doped tellurite glasses and glass ceramics[END_REF], Eu:CaGdAlO 4 crystal (1.02 ms) [START_REF] Li | Crystal characterization and optical spectroscopy of Eu 3+ -doped CaGdAlO 4 single crystal fabricated by the floating zone method[END_REF] and Eu:Bi 4 Ge 3 O 12 crystal (1.51 ms) [START_REF] Li | Spectroscopic properties of Eu:Bi 4 Ge 3 O 12 single crystal grown by the micro-pulling-down method[END_REF]. The result shows that Eu:YAG and Eu:Y 3 ScAl 4 O 12 crystals are promising candidates for red luminescent/laser materials.

Fig. 1 .

 1 Photographs of the as-grown Eu:YAG (a) and Eu:Y 3 ScAl 4 O 12 (b) crystals.

Fig. 2 .

 2 Fig. 2. XRD patterns of Eu:YAG and Eu:Y 3 ScAl 4 O 12 crystals with a standard pattern of YAG (PDF#88-2048).

Fig. 3 .

 3 Fig. 3.The Raman spectra of Eu:YAG and Eu:Y 3 ScAl 4 O 12 crystals.

Fig. 4 .

 4 Fig. 4. The absorption spectra of Eu:YAG and Eu:Y 3 ScAl 4 O 12 crystals.

Fig. 5 .

 5 Fig. 5. The emission spectra of Eu:YAG and Eu:Y 3 ScAl 4 O 12 crystals under 394 nm excitation

Fig. 6 .

 6 Fig. 6. CIE-1931 chromaticity diagram of Eu:YAG and Eu:Y 3 ScAl 4 O 12 crystals.

Fig. 7 .

 7 Fig. 7. Decay curves of 5 D 0 level of Eu:YAG and Eu:Y 3 ScAl 4 O 12 crystals.

  In this work, Eu 3+ -doped YAG and Y 3 ScAl 4 O 12 single crystals have been successfully grown by the μ-PD method for the first time. The optical properties including absorption spectra, fluorescence spectra and fluorescence decay curves of Eu:YAG and Eu:Y 3 ScAl 4 O 12 were characterized and compared. The FWHM of absorption band at 395 nm was calculated to be 1.89 and 2.21 nm for Eu:YAG and Eu:Y 3 ScAl 4 O 12 , respectively. The most intense red emission centered at 710 nm corresponding to the transition 5 D 0 → 7 F 4 , and the FWHM of emission band at 710 nm was calculated to be 2.03 and 3.19 nm for Eu:YAG and Eu:Y 3 ScAl 4 O 12 , respectively. The lifetime of Eu:YAG and Eu:Y 3 ScAl 4 O 12 crystals was measured to be 3.19 and 2.97 ms, respectively. All the results show that the Eu:YAG and Eu:Y 3 ScAl 4 O 12 crystals are potential media for red luminescent emission.

  . The Eu 2 O 3 , Sc 2 O 3 , Y 2 O 3 and Al 2 O 3 powders with high purity of 99.999% were used as raw materials. The starting materials were weighed according to the formula (Eu 0.02 Y 0.98 ) 3 Al 5 O 12 , (Eu 0.02 Y 0.98 ) 3 ScAl 4 O 12

Acknowledgements

This work is partially supported by National Key Research and Development Program of China (No. 2016YFB0701002) and National Natural Science Foundation of China (No. 61621001).