Petr Jančar
email: petr.jancar@upol.cz

Jérôme Leroux
email: jerome.leroux@labri.fr

Grégoire Sutre
email: gregoire.sutre@labri.fr

Co-Finiteness and Co-Emptiness of Reachability Sets in Vector Addition Systems with States

published or not. The documents may come   L'archive ouverte pluridisciplinaire

Introduction

Context. Analysis of behavioural properties of (models of) systems is a natural and wide area of study; the decidability and complexity questions for respective properties are an important part of such research. As the most relevant for us we recall the reachability and liveness problems for Petri nets.

A concrete source of motivation for us has been the recent paper [START_REF] Jančar | Deciding structural liveness of Petri nets[END_REF] that answered the decidability question for structural liveness in Petri nets positively; the open status of this question was previously recalled, e.g., in [START_REF] Best | Existence of home states in Petri nets is decidable[END_REF]. It is natural to continue with studying the computational complexity of this problem. Here we contribute indirectly to this topic by studying some related naturally arising problems concerning reachability sets.

The algorithm in [START_REF] Jančar | Deciding structural liveness of Petri nets[END_REF] reduces the structural liveness problem to the question if a Petri net with a downward closed set of initial markings is "universal", in the sense that every marking is reachable from the initial ones. This question has been solved by using the involved result proved in [START_REF] Leroux | Presburger vector addition systems[END_REF], namely that there is an algorithm that halts with a Presburger description of the reachability set when this set is semilinear. Since this approach is not constructive, it does not provide any complexity upper bound. This led us to consider the universality problem, which we call the co-emptiness problem, on its own. There is also a naturally related co-finiteness problem asking if a set of initial markings allows to reach all but finitely many markings; this problem can be thus seen as dual to the well-known boundedness problem that asks if the reachability set is finite.

Contributions. We formulate the co-emptiness and co-finiteness problem generally for semilinear sets of initial markings. We show that the co-emptiness problem is decidable using a reduction to [START_REF] Leroux | Presburger vector addition systems[END_REF] that is similar to the above-mentioned approach used in [START_REF] Jančar | Deciding structural liveness of Petri nets[END_REF] to decide the structural liveness problem. As before, no complexity upper bound can be derived from that approach. In the case of the co-finiteness problem we are even not sure with decidability, but we formulate a conjecture under which the problem is decidable.

We then consider restrictions to the case with finite sets of initial markings and then in particular to the case with singleton sets of initial markings.

In the case of finite initial sets we show that the co-emptiness problem reduces in logarithmic space to the reachability problem. The converse reduction (reachability to co-emptiness) is left open.

In the case of singleton initial sets we show EXPSPACE-completeness for both co-emptiness and co-finiteness. This is the main technical result of the paper. While the lower bound is obtained by an easy reduction from the coverability problem (a well known EXPSPACE-complete problem, similarly as boundedness), getting the upper bound is more involved. Using the bound obtained for reversible reachability by Leroux in [9], we reduce the co-emptiness problem (with a single initial marking) to a large number of coverability questions in a large Petri net. The latter is bounded in such a way that the questions can be still answered in exponential space, using Rackoff's technique [START_REF] Rackoff | The covering and boundedness problems for vector addition systems[END_REF].

Though our results do not improve our knowledge about the complexity of structural liveness directly, we show that a related problem, namely the structural deadlock-freedom problem is tightly related (interreducible in polynomial time) with the co-emptiness problem in the case of downward closed sets of initial markings.

We have found more convenient to present our results on the model of vector addition systems with states, or shortly VASSs. This model is equivalent to Petri nets and all our results, while proved for VASSs, also hold for Petri nets.

Outline. In Section 2 we recall some preliminary notions, such as vector addition systems with states and semilinear sets. Section 3 defines the co-emptiness problem and the co-finiteness problem, and presents our partial decidability results for the general case and for the restriction to finite sets of initial configurations. The main result is contained in Section 4 where we show the EXPSPACEcompleteness of co-emptiness and co-finiteness in the case with singleton sets of initial configurations. Section 5 presents two applications of the co-emptiness problem: we recall the structural liveness, and show the tight relation of structural deadlock-freedom to the co-emptiness problem with downward closed sets of initial configurations. We conclude the paper by Section 6.

Preliminaries

By Z we denote the set of integers, and by N the set {0, 1, 2, . . . } of nonnegative integers. By [i, j], where i, j ∈ Z, we denote the set {i, i+1, . . . , j} (which is empty when i > j).

For a vector v ∈ Z d (d ∈ N), by v(i) we denote the i-th component of v. On Z d we define the operations +, -and the relations ≥, ≤ componentwise. For

v 1 , v 2 ∈ Z d we thus have v 1 + v 2 = w where w(i) = v 1 (i) + v 2 (i) for all i ∈ [1, d]; we have v 1 ≤ v 2 iff v 1 (i) ≤ v 2 (i) for all i ∈ [1, d]. For k ∈ N and v ∈ Z d we put k • v = (k • v(1), k • v(2), • • • , k • v(d)); we also write kv instead of k • v.
Slightly abusing notation, by (v 1 , v 2 , . . . , v m ) where v i ∈ Z di for i ∈ [1, m] we do not denote an m-tuple of vectors but the corresponding vector of dimension

d = i∈[1,m] d i . The norm v of a vector v ∈ Z d is max{|v(i)|; i ∈ [1, d]}, and the norm V of a finite set V ⊆ Z d is max{ v ; v ∈ V }; here we stipulate max ∅ = 0.
When the dimension d is clear from context, by 0 we denote the zero vector (0(i) = 0 for all i ∈ [1, d]), and by e i (i ∈ [1, d]) the vector satisfying e i (i) = 1 and e i (j) = 0 for all j ∈ [1, d] {i}.

For a set A, by A * we denote the set of finite sequences of elements of A, and by ε we denote the empty sequence. For w ∈ A * , |w| denotes its length.

Vector addition systems with states (VASSs). A vector addition system with states (a VASS ) is a tuple V = (d, Q, A, T ) where d ∈ N is the dimension, Q is the finite set of (control) states, A ⊆ Z d is the finite set of actions, and T ⊆ Q × A × Q is the finite set of transitions. We often present t ∈ T where t = (q, a, q ) as q a -→ q or t :

q a -→ q . The set of configurations of V = (d, Q, A, T ) is the set Q × N d ; we rather present a configuration (q, v) as q(v) (where q ∈ Q, v ∈ N d ). For actions a ∈ A we define relations a -→ V on the set Q × N d of configurations by putting q(v) a -→ V q (v ) if q a -→ q is a transition in T and v = v + a.
Hence for a transition q a -→ q and v ∈ N d we have q(v) [1,m] a i . We also note the monotonicity:

a -→ V q (v +a) iff v +a ≥ 0. Relations a -→ V are naturally extended to relations α -→ V for α ∈ A * ; we write just α -→ instead of α -→ V when V is clear from context. The extension is defined inductively: we put q(v) ε -→ q(v); if q(v) a -→ q (v ) and q (v ) α -→ q (v ), then q(v) aα --→ q (v ). We note that q(v) α -→ q (v ) where α = a 1 a 2 • • • a m implies that v = v + i∈
if q(v) α -→ q (v ), then for any v ≥ v we have q(v) α -→ q (v + v -v). Reachability sets. Given a VASS V = (d, Q, A, T ), by q(v) * -→ V q (v ), or by q(v) * -→ q (v
) when V is clear from context, we denote that q (v ) is reachable from q(v), i.e., that q(v) α -→ q (v ) for some α ∈ A * . The reachability set for an (initial) configuration q(v) is the set

q(v) V = {q (v ) | q(v) * -→ V q (v )}.
For a set C ⊆ Q × N d of (initial) configurations we put

C V = q(v)∈C q(v) V .
We also write just q(v) and C when V is clear from context.

We write q(v)

* -→ C if there is q (v ) ∈ C such that q(v) * -→ q (v ); similarly C * -→ q(v) if there is q (v ) ∈ C such that q (v ) * -→ q(v). Semilinear sets of configurations. A set C ⊆ Q × N d is linear if C = {q(b + n 1 p 1 + • • • + n k p k ) | n 1 , . . . , n k ∈ N} for some q ∈ Q, k ∈ N, and b, p 1 , . . . , p k ∈ N d . A set C ⊆ Q × N d is semilinear if C = L 1 ∪ L 2 ∪ • • • ∪ L m for some m ∈ N and linear sets L j , j ∈ [1, m].
We recall that semilinear sets correspond to the sets definable in Presburger arithmetic [START_REF] Ginsburg | Semigroups, Presburger formulas, and languages[END_REF].

Vector addition systems (VASs). A vector addition system (VAS ) is a VASS (d, Q, A, T ) where Q is a singleton. In this case the single control state plays no role, in fact; it is thus natural to view a VAS as a pair U = (d, A) for a finite set A ⊆ Z d . The configurations are here simply v ∈ N d , and for a ∈ A we have

v a -→ v iff v = v + a (for any v, v ∈ N d ).
We write v U , or just v , for the reachability set of v. For a VAS the terms "action" and "transition" are identified.

Binary and unary presentations. Instances of the problems that we will consider comprise VASSs and (presentations of semilinear sets of) configurations. We implicitly assume that the numbers in the respective vectors are presented in binary. When giving a complexity lower bound, we will explicitly refer to a unary presentation to stress the substance of the lower bound.

Co-Finiteness and Co-Emptiness of Reachability Sets

Now we introduce the two main problems considered in this paper.

Co-finiteness. The co-finiteness problem:

Instance: a VASS V = (d, Q, A, T ) and a (presentation of a) semilinear set C ⊆ Q × N d . Question: is C co-finite, i.e., is the set (Q × N d )
C finite ?

Co-emptiness (or universality). By narrowing the co-finiteness question we get the co-emptiness problem:

Instance: a VASS V = (d, Q, A, T ) and a (presentation of a) semilinear set C ⊆ Q × N d . Question: is C co-empty, i.e., is C = Q × N d ?
We note that co-emptiness can be also naturally called universality.

Decidability of the General Problems

We recall the classical reachability problem, defined as follows:

Instance: a VASS V and two configurations q(v), q (v ).

Question: is q(v) * -→ V q (v ) ?
The problem is decidable [START_REF] Mayr | An algorithm for the general Petri net reachability problem[END_REF] but its complexity remains elusive; the problem is known to be EXPSPACE-hard [START_REF] Lipton | The reachability problem requires exponential space[END_REF], and the best known upper bound is nonprimitive recursive [START_REF] Leroux | Demystifying reachability in vector addition systems[END_REF].

By adding the acceleration techniques in [START_REF] Leroux | Presburger vector addition systems[END_REF], and decidability of Presburger arithmetic, it is straightforward to derive decidability of the co-emptiness problem. We first recall a crucial fact.

Theorem 1 (reformulation of Lemma XI.1 of [START_REF] Leroux | Presburger vector addition systems[END_REF]). Given a VASS V = (d, Q, A, T ) and a semilinear set C of configurations, for every semilinear set D ⊆ C V there is a sequence α 1 , . . . , α k of words in A * such that for every q(v) ∈ D we have

C α n 1 1 ...α n k k ------→ V q(v)
for some n 1 , . . . , n k ∈ N.

We thus deduce that the co-emptiness problem can be decided by the following two procedures that are executed concurrently:

-One procedure systematically searches for some configuration q(v) such that q(v) ∈ C which is verified by using an algorithm deciding (non)reachability; this search succeeds iff C is not co-empty.

-The other procedure systematically searches for some words α 1 , . . . , α k such that for every configuration q(v) there are n 1 , . . . , n k in N such that

C α n 1 1 ...α n k k ------→ q(v)
. This property (of α 1 , . . . , α k ) can be formulated in Presburger arithmetic and is thus decidable. The search succeeds iff C is coempty.

However, the complexity of the co-emptiness problem is still open. In fact, we even have no reduction from or to the reachability problem.

The decidability status of the co-finiteness problem is not clear. We show how to solve the problem under a conjecture. Let us first introduce the notion of inductive set. A set of configurations D of a VASS V = (d, Q, A, T ) is inductive if for every configuration q(v) in D and every transition t : q a -→ q in T such that v + a ≥ 0, we have q (v + a) ∈ D. We observe that if an inductive set D contains a set of initial configurations C then C ⊆ D. Moreover, we can effectively decide if a semilinear set D is inductive. We introduce the following conjecture.

Conjecture 2. Given a VASS V and a semilinear set

C of configurations, if C V is co-infinite (i.e., not co-finite), then there is an inductive semilinear set D such that C ⊆ D (hence also C V ⊆ D) and D is co-infinite.
Under that conjecture, the co-finiteness problem can be also decided by two algorithmic procedures executed concurrently:

-One procedure systematically searches for some inductive co-infinite semilinear set D that contains C; this search succeeds iff C is co-infinite (under the conjecture). -The other procedure systematically searches for some words α 1 , . . . , α k and a natural number n, such that for every configuration q(v) with v ≥ n there

are n 1 , . . . , n k in N satisfying C α n 1 1 ...α n k k ------→ q(v)
. This property (of α 1 , . . . , α k and n) can be formulated in Presburger arithmetic, and is thus decidable. The search succeeds iff C is co-finite thanks to Theorem 1. Indeed, when the reachability set C is co-finite then it is semilinear, and we can apply Theorem 1 with D = C .

Hence we have derived:

Theorem 3. The co-emptiness problem is decidable. The co-finiteness problem is decidable when assuming validity of Conjecture 2.

Finitely Many Initial Configurations

As already mentioned, we have no complexity upper bound for the (decidable) co-emptiness problem in our general form. In the rest of this section we focus on the FMIC co-emptiness problem, and the FMIC co-finiteness problem, where "FMIC" refers to "Finitely Many Initial Configurations". We give the result captured by Theorem 5.

Lemma 4. Given a VASS

V = (d, Q, A, T ) and any set C ⊆ Q × N d , we have C = Q × N d iff C ⊇ D 1 ∪ D 2 where D 1 = {q(v+e i ) | q(v) ∈ C, i ∈ [1, d]} and D 2 = {q(0) | q ∈ Q}. Proof. If C = Q × N d , then we trivially have C ⊇ D 1 ∪ D 2 .
Let us now assume C ⊇ D 1 . We show that

q(v) ∈ C implies q(v+e i ) ∈ C (1)
(for all q ∈ Q, v ∈ N d , i ∈ [1, d]). Indeed, if q 0 (v 0 ) * -→ q(v) for some q 0 (v 0 ) ∈ C, then C q 0 (v 0 +e i ) since C ⊇ D 1 and q 0 (v 0 +e i ) * -→ q(v+e i ) by monotoni- city; hence q(v+e i ) ∈ C . If, moreover, C ⊇ D 2 , then by (1) we get q(v) ∈ C for all q ∈ Q, v ∈ N d .
Theorem 5. The FMIC co-emptiness problem is logspace reducible to the reachability problem.

Proof.

Given a VASS V = (d, Q, A, T ) and a finite set C ⊆ Q × N d , deciding if C = Q × N d boils down to verifying if each configuration in the finite set D 1 ∪ D 2 = {q 1 (v 1 ), . . . , q k (v k )}
defined in Lemma 4 is reachable from (a configuration in) C. Let V arise from V by adding a fresh control state q 0 and transitions q 0 v -→ q for all q(v) ∈ C. Hence

C V ⊇ D 1 ∪ D 2 iff q 0 (0) * -→ V q j (v j ) for all j ∈ [1, k].
Let us now consider a VASS V of dimension kd comprising k disjoint copies of V (each copy works on its own counters); let (q, j) denote the control state q of V in the j-th copy (j ∈ [1, k]).

Finally, we let V arise from V by adding transitions (q j , j)

0 -→ (q 0 , j+1), for j ∈ [1, k-1]. We observe that q 0 (0) * -→ V q j (v j ) for all j ∈ [1, k] iff (q 0 , 1)(0) * -→ V (q k , k)(v 1 , . . . , v k ).
We have thus shown the claimed logspace reduction.

We leave open the question if the FMIC co-finiteness problem can be similarly reduced to the reachability problem. Another open question is if reachability can be reduced to FMIC co-finiteness or FMIC co-emptiness. In the next section, we characterize the complexity of both problems for the case of single initial configurations.

In this section we restrict our attention to the SIC co-emptiness problem and the SIC co-finiteness problem where SIC refers to "Single Initial Configuration"; the problem instances are thus restricted so that the given sets C are singletons (C = {q 0 (v 0 )}). In the rest of this section we prove the following theorem. Theorem 6. Both the SIC co-finiteness problem and the SIC co-emptiness problem are EXPSPACE-complete.

We recall that the integers in the problem instances are presented in binary. Nevertheless the lower bound will be shown already for unary VASs (hence with no control states and with a unary presentation of integers).

We first recall two well-known EXPSPACE-complete problems for VASSs where the lower bound also holds for unary VASs.

Coverability. The coverability problem:

Instance: a VASS V = (d, Q, A, T ), q 0 , q 1 ∈ Q, v 0 , v 1 ∈ N d ; Question: is q 0 (v 0 ) * -→ q 1 (v 1 ) for some v1 ≥ v 1 ?
Boundedness. The boundedness problem:

Instance: a VASS V = (d, Q, A, T ), q 0 ∈ Q, v 0 ∈ N d ; Question: is q 0 (v 0 ) finite ?
The EXPSPACE-hardness results follow from [START_REF] Lipton | The reachability problem requires exponential space[END_REF] (see also, e.g. [START_REF] Esparza | Decidability and complexity of Petri net problems -an introduction[END_REF]), the upper bounds follow from [START_REF] Rackoff | The covering and boundedness problems for vector addition systems[END_REF]. A generalization of [START_REF] Rackoff | The covering and boundedness problems for vector addition systems[END_REF], extending a class of problems known to be in EXPSPACE, was given in [START_REF] Yen | A unified approach for deciding the existence of certain Petri net paths[END_REF], which was later corrected in [START_REF] Atig | On Yen's path logic for Petri nets[END_REF].

EXPSPACE-hardness

Showing the hardness part of Theorem 6 is relatively straightforward; we reduce coverability in unary VASs (which we recalled as an EXPSPACE-complete problem) to both SIC co-finiteness and SIC co-emptiness by the following lemma.

Lemma 7. Given a unary VAS U = (d, A) and v 0 , v 1 ∈ N d , there is a logspace construction yielding a unary VAS U = (d+1, A ) and v 0 ∈ N d+1 such that:

a) if v 0 * -→ U v1 for some v1 ≥ v 1 , then v 0 U = N d+1 ; b) otherwise (when v 0 * -→ U w implies w ≥ v 1 ) the set N d+1 v 0 U is infinite.
Proof. Let us assume a unary VAS U = (d, A) and vectors v 0 , v 1 ∈ N d . We consider U = (d+1, A ) and v 0 = (v 0 , 0) where

A = {(a, 0) | a ∈ A} ∪ {b 1 , b 2 } ∪ {c j | j ∈ [1, d]} ∪ {-e j | j ∈ [1, d]} for b 1 = (-v 1 , 2), b 2 = (v 0 , -1), c j = e j -e d+1 .
It suffices to verify that the points a) and b) are satisfied (for U and v 0 ):

a) Suppose v 0 α -→ U v1 for some v1 ≥ v 1 and α = a 1 a 2 • • • a m . For α = (a 1 , 0)(a 2 , 0) • • • (a m , 0), in U we then have (v 0 , 0) α -→ (v 1 , 0) b1 -→ (v 1 -v 1 , 2) b2 -→ (v 0 +v 1 -v 1 , 1).
By monotonicity, for any k ∈ N we have

v 0 = (v 0 , 0) (α b1b2) k ------→ w k = (v 0 +k(v 1 -v 1 ), k); hence w k (d+1) = k. For any w ∈ N d+1 and the sum k = j∈[1,d+1] w(j)
we have w k * -→ w; indeed, in w k we can first empty (i.e., set to zero) all components j ∈ [1, d] by using actions -e j (j ∈ [1, d]), and then distribute the k tokens from component d+1 by the actions c j so that w is reached.

Hence v 0 U = N d+1 . b) Suppose there is no v1 ≥ v 1 such that v 0 * -→ U v1 .
Then for any w ∈ v 0 U we have w ≥ (v 1 , 0) and w(d+1) = 0, since the actions b 1 , b 2 , c j are dead (they cannot get enabled from v 0 ); indeed, by monotonicity the actions -e j cannot help to cover (v 1 , 0) from v 0 . Hence the set N d+1 v 0 U is infinite.

EXPSPACE-membership.

We now prove the EXPSPACE-membership claimed by Theorem 6. This is more involved; besides a closer look at the results in [START_REF] Rackoff | The covering and boundedness problems for vector addition systems[END_REF], we will also use the following result from [9], from which we derive Lemma 9.

Theorem 8 ([9]

). Given a VASS V = (d, Q, A, T ) and two configurations q 0 (v 0 ) and q 1 (v 1 ) reachable one from the other (i.e., q 0 (v 0 ) *

-→ q 1 (v 1 ) * -→ q 0 (v 0 )), there is a word α ∈ A * such that a) q 0 (v 0 ) α -→ q 1 (v 1 ), and b) |α| ≤ 6 • (d + 3) 2 • x 45(d+3) d+5 where x = 1 + 2|Q| + 2 A + 2 v 0 + v 1 .
Proof. Theorem 10.1 of [9] states that for every pair (v 0 , v 1 ) of configurations of a VAS (p, A ) that are reachable one from the other there is a word α ∈ (A ) * such that:

v 0 α -→ v 1 and |α | ≤ 17p 2 y 15p p+2 where y = (1 + 2 A )(1 + v 0 + v 1 -v 0 )
. We extend this result to a VASS (d, Q, A, T ) by encoding it as a VAS (p, A ) using [6, Lemma 2.1]. With this encoding, p = d+3, A ≤ max{ A , |Q|•(|Q|-1)} and the encodings of q 0 (v 0 ) and

q 1 (v 1 ) provide vectors v 0 , v 1 satisfying v 0 ≤ v 0 + |Q| and v 1 -v 0 = v 1 -v 0 ≤ v 1 + v 0 . It follows that (1 + 2 A ) ≤ x 2 and (1 + v 0 + v 1 - v 0 ) ≤ x.
Thus y is bounded by x 3 . Finally, since the effect of an action of the VASS is simulated by three actions of the simulating VAS, we deduce that there exists a word α ∈ A * such that q 0 (v 0 ) α -→ q 1 (v 1 ) and such that |α| ≤ 1 3 |α |. We derive the bound on |α| by observing that 17 3 ≤ 6.

Pumpability of components. Given a VASS V = (d, Q, A, T ), we say that

component i ∈ [1, d] is pumpable in q(v) if q(v) * -→ q(v+ke i ) for some k ≥ 1.
Lemma 9. For any VASS V = (d, Q, A, T ) and any

q ∈ Q, v ∈ N d , i ∈ [1, d] where component i is pumpable in q(v) there is α ∈ A * such that a) q(v) α -→ q(v+ke i ) for some k ≥ 1, and b) |α| ≤ 6 • (d + 3) 2 • x 45(d+3) d+5 where x = 2 + 2|Q| + 2 A + 3 v .
The trivial fact k ≤ |α| • A thus also yields a double-exponential bound on k.

Proof. We consider a VASS V = (d, Q, A, T ) and assume q(v) * -→ V q(v+ke i )

where k ≥ 1. For the VASS V arising from V by adding (action -e i and) the transition q -ei --→ q we get

q(v) * -→ q(v+ke i ) -ei --→ • • • -ei --→ q(v+e i ) -ei --→ q(v);
hence q(v) and q(v+e i ) are reachable one from the other (they are in the reversible-reachability relation) in V . Using Theorem 8, we derive that

q(v) α -→ V q(v+e i ) (2)
for some α

∈ (A ∪ {-e i }) * that is bounded as in the point b) of the claim. If α in (2) is a 1 a 2 • • • a m ,
then there are states q 1 , q 2 , . . . , q m-1 such that

q(v) a1 -→ q 1 (v 1 ) a2 -→ q 2 (v 2 ) a3 -→ • • • q m-1 (v m-1 ) am --→ q(v+e i ) (3)
for the corresponding v j (j ∈ [1, m-1]). We can view (3) as a sequence of transitions; let ≥ 0 be the number of occurrences of the transition q -ei --→ q in (3). Due to monotonicity, we can omit these occurrences and keep performability: we get q(v)

ai 1 ai 2 •••ai m- ---------→ V q(v+( +1)e i ) (4)
for the sequence a i1 a i2 • • • a i m-arising from a 1 a 2 • • • a m by omitting the respective occurrences of -e i . The proof is thus finished.

We derive the following important corollary:

Corollary 10. There is an exponential-space algorithm that, given a VASS V = (d, Q, A, T ) and q(v), decides if all components i ∈ [1, d] are pumpable in q(v), and in the positive case provides an (at most double-exponential

) number n ≥ 1 such that q(v) * -→ q(v+ne i ) for each i ∈ [1, d].
Proof. It suffices to consider a nondeterministic algorithm trying to find, for each i ∈ [1, d] separately, α i with length bounded as in Lemma 9 such that q(v) αi -→ q(v+k i e i ) for some k i ≥ 1. The algorithm just traverses along (a guessed bounded) α i , keeping only the current configuration in memory; hence exponential space is sufficient.

By monotonicity, q(v) * -→ q(v+k i e i ) implies that q(v) * -→ q(v+xk i e i ) for all x ≥ 1. Hence if k i ≥ 1 for all i ∈ [1, d] are found, then the least common multiple (or even simply the product) of all k i , i ∈ [1, d], can be taken as the claimed number n.

Before giving the algorithm deciding SIC co-emptiness we introduce some useful natural notions, namely a notion of "reversing a VASS" (letting its computations run backwards), and a notion of "transforming a VASS modulo n" (where the component-values are divided by n while the remainders are kept in the control states).

Reversed VASS. To a VASS V = (d, Q, A, T ) we associate its reversed VASS

V ← = (d, Q, -A, T ← ) where -A = {-a | a ∈ A} and T ← = {q -a --→ q | q a -→ q is in T }.
The next proposition can be easily verified by induction on m. Proposition 11. For any VASS V and m ≥ 1, we have

q 0 (v 0 ) a1 -→ q 1 (v 1 ) a2 -→ q 2 (v 2 ) a3 -→ • • • q m-1 (v m-1 ) am --→ q m (v m ) in V iff q m (v m ) -am ---→ q m-1 (v m-1 ) -am-1 -----→ • • • q 1 (v 1 ) -a1 --→ q 0 (v 0 ) in V ← . Modulo-n VASS. Given a VASS V = (d, Q, A, T ) and n ≥ 1, we put V (n) = (d, Q × {0, 1, . . . , n-1} d , A , T (n) )
where T (n) arises as follows: each transition q a -→ q in T and each u ∈ {0, 1, . . . , n-1} d determines the transition (q, u)

a -→ (q , u ) in T (n)
where u and a are the unique vectors such that u + a = u + na and u ∈ {0, 1, . . . , n-1} d . The set A is simply {a | ((q, u)

a -→ (q , u )) ∈ T (n) }.
The next proposition is again easily verifiable by induction on m. Proposition 12. For any VASS V, n ≥ 1, and m ≥ 1, we have

q 0 (v 0 ) a1 -→ q 1 (v 1 ) a2 -→ q 2 (v 2 ) a3 -→ • • • q m-1 (v m-1 ) am --→ q m (v m ) in V iff (q 0 , u 0 )(v 0 ) a 1 -→ (q 1 , u 1 )(v 1 ) a 2 -→ • • • a m --→ (q m , u m )(v m ) in V (n)
where u j + nv j = v j for every j ∈ [0, m] (and u j-1 + a j = u j + na j for every j ∈ [1, m]).

Algorithm deciding SIC co-emptiness. We define the following algorithm.

Algorithm Alg-Co-Empt

Input: a VASS V = (d, Q, A, T ) and a configuration q 0 (v 0 ).

Output: YES if q 0 (v 0 ) = Q × N d , and NO otherwise. 1. Check if each component i ∈ [1, d]
is pumpable in q 0 (v 0 ), and in the positive case compute an (at most double-exponential) number n as described in Corollary 10 (hence q 0 (v 0 ) * -→ q 0 (v 0 +ne i ) for each i ∈ [1, d]). In the negative case (when some component is not pumpable

) return NO. 2. Let V be the VASS V = (V ← ) (n) = (d, Q × {0, 1, . . . , n-1} d , A , T ) {i.e.,
the reversed VASS modulo n, where n is computed in the point 1}.

Create the configuration (q 0 , u 0 )(v 0 ) of V corresponding to the configuration q 0 (v 0 ) of V (hence v 0 = u 0 + nv 0 ). 3. For each control state (q, u) of V check if (q, u)(0) covers (q 0 , u 0 )(v 0 ) (in V ), i.e., if (q, u)(0) * -→ V (q 0 , u 0 )(v) for some v ≥ v 0 . If the answer is negative for some (q, u), then return NO, otherwise (when all (q, u)(0) cover (q 0 , u 0 )(v 0 )) return YES.

Correctness and exponential-space complexity of Alg-Co-Empt. Lemma 13. Algorithm Alg-Co-Empt satisfies its specification (i.e., returns YES if q 0 (v 0 ) = Q × N d , and NO otherwise).

Proof. If Alg-Co-Empt, when given V = (d, Q, A, T ) and q 0 (v 0 ), returns NO in the point 1, then for some i ∈ [1, d] we have q 0 (v 0 ) * -→ q 0 (v 0 +xe i ) for all x ≥ 1; therefore the set (Q × N d ) q 0 (v 0 ) V is nonempty and even infinite. Suppose now that the test in the point 1 has been positive, and a respective number n has been computed.

Assume first that q 0 (v 0 ) V = Q × N d and let us show that the algorithm returns YES. Let (q, u) be a control state of V = (V ← ) (n) . Since q 0 (v 0 ) V = Q × N d , we have q 0 (v 0 ) * -→ V q(u). It follows that (q, u)(0) * -→ V (q 0 , u 0 )(v 0 ), which also entails that (q, u)(0) covers (q 0 , u 0 )(v 0 ) in V . We have proved that the algorithm returns YES.

Conversely, we assume that the algorithm returns YES and we prove that q 0 (v 0 ) V = Q × N d . Let q(v) be a configuration of V and let (q, u)(v ) be the corresponding configuration in V , i.e., v = u + nv . Since (q, u)(0) covers (q 0 , u 0 )(v 0 ), there exists v 0 ≥ v 0 such that (q, u)(0) * -→ V (q 0 , u 0 )(v 0 ). It follows that q 0 (u 0 + nv 0 ) * -→ V q(u). By monotonicity, we derive that

q 0 (u 0 + nv 0 + nv ) * -→ V q(u + nv ) = q(v).
By the definition of n, we get

q 0 (v 0 ) * -→ V q 0 (v 0 + n(v 0 -v 0 ) + nv ) = q 0 (u 0 + nv 0 + nv ).
We have proved that q 0 (v 0 ) * -→ V q(v), and thus q 0 (v 0

) V = Q × N d .
We still need to show that Alg-Co-Empt works in exponential space (Lemma 15). We first give a straightforward extension to VASSs of a result formulated in [START_REF] Rackoff | The covering and boundedness problems for vector addition systems[END_REF] for VASs. Proposition 14. For any VASS V = (d, Q, A, T ) and any configurations q 0 (v 0 ) and q 1 (v 1 ), if q 0 (v 0 ) * -→ q 1 (v 1 ) then q 0 (v 0 ) α -→ q 1 (v 1 ) for some v1 ≥ v 1 and α ∈ A * such that |α| < x (d+1)! , where x = |Q| • (1 + A + v 1 ).

Proof. The bounds given in [START_REF] Rackoff | The covering and boundedness problems for vector addition systems[END_REF] for VASs are easily extended to VASSs. Instead of giving a full proof, we only explain how to adapt the proof of [START_REF] Rackoff | The covering and boundedness problems for vector addition systems[END_REF] to deal with control states.

The notions of paths, of i-bounded sequences and of i-covering sequences from [13, pages 224-225] are extended with control states in the obvious way. For each q ∈ Q and v ∈ Z d , define m(i, q, v) to be the length of the shortest i-bounded, i-covering path in V starting from q(v), with the convention that m(i, q, v) = 0 if there is none. Now define

f (i) = max{m(i, q, v) | q ∈ Q, v ∈ Z d }.
With the same reasoning as in [START_REF] Rackoff | The covering and boundedness problems for vector addition systems[END_REF]Lemma 3.4], we get that

f (0) ≤ |Q| and f (i+1) ≤ |Q| • (max{ A , v 1 } • f (i)) i+1 + f (i). It follows that f (i+1) ≤ (xf (i)) i+1 . An immediate induction on i yields that f (i) ≤ x (i+1)! . In particular, we get that m(d, q 0 , v 0 ) ≤ f (d) ≤ x (d+1)! . Now, if q 0 (v 0 ) * -→ q 1 (v 1 ) then 0 < m(d, q 0 , v 0 ). This entails that q 0 (v 0 ) α -→ q 1 (v 1 ) for some v1 ≥ v 1 and α ∈ A * such that |α| = m(d, q 0 , v 0 ) -1 < x (d+1)! .
Lemma 15. Algorithm Alg-Co-Empt works (i.e., can be implemented to work) in exponential space.

Proof. The point 1 of Alg-Co-Empt, including the binary presentation of the computed number n, can be performed in exponential space, w.r.t. the size of the binary presentation of the input V = (d, Q, A, T ) and q 0 (v 0 ); this follows by Corollary 10.

The VASS V = (V ← ) (n) in the point 2 is not needed to be constructed explicitly. The algorithm creates the configuration (q 0 , u 0 )(v 0 ) and then stepwise generates the control states (q, u) (q ∈ Q, u ∈ {0, 1, . . . , n-1} d ) of V and checks if (q, u)(0) covers (q 0 , u 0 )(v 0 ) in V .

It thus suffices to show that checking if (q, u)(0) covers (q 0 , u 0 )(v 0 ) (i.e., if (q, u)(0) * -→ V (q 0 , u 0 )(v) for some v ≥ v 0 ) can be done in exponential space (w.r.t. the binary presentation of V = (d, Q, A, T ) and q 0 (v 0 )). By Prop. 14, it is enough to search for witnesses of coverability (q, u)(0)

α -→ (q 0 , u 0 )(v) of length |α| < x (d+1)! , where x = |Q|n d • (1 + A + v 0 ).
Since n is at most double-exponential, x (d+1)! is also at most double-exponential. As in the proof of Corollary 10, the algorithm just traverses along (a guessed bounded) α, keeping only the current configuration in memory; so exponential space is sufficient.

Algorithm deciding SIC co-finiteness. We will adjust the algorithm Alg-Co-Empt so that, given V = (d, Q, A, T ) and q 0 (v 0 ), it answers YES iff the set (Q × N d ) q 0 (v 0 ) is finite; this can happen even if some (q, u)(0) does not cover (q 0 , u 0 )(v 0 ) in V . Informally speaking, it suffices to check if (q, u)(0) covers (q 0 , u 0 )(v 0 ) whenever we "ignore" one-component of 0, making it "arbitrarily large".

By ω we denote an "infinite amount", satisfying z < ω and z+ω = ω+z = ω for all z ∈ Z. Given V = (d, Q, A, T ), by the set of extended configurations we mean the set Q×(N∪{ω}) d ; the relations q(v) a -→ q (v ), q(v) α -→ q (v ) (α ∈ A * ), and q(v) * -→ q (v ) are then naturally extended to the relations on Q×(N∪{ω}) d . (Hence, e.g., if q(v)

α -→ q (v ) then v(i) = ω iff v (i) = ω, for any i ∈ [1, d].)
Let us now consider the following algorithm.

Algorithm Alg-Co-Finit

Input: a VASS V = (d, Q, A, T ) and a configuration q 0 (v 0 ).

Output: YES if (Q × N d )
q 0 (v 0 ) is finite, and NO otherwise.

1. As in Alg-Co-Empt.

As in

Alg-Co-Empt. 3. For each control state (q, u) of V and each i ∈ [1, d] check if (q, u)(ωe i ) covers (q 0 , u 0 )(v 0 ) (in V ), i.e., if (q, u)(ωe i ) * -→ V (q 0 , u 0 )(v) for some v ≥ v 0 ;
by ωe i we denote the d-dimensional vector where the i-th component is ω and the other components are zero. If the answer is negative for some (q, u) and i ∈ [1, d], then return NO, otherwise (when all (q, u)(ωe i ) cover (q 0 , u 0 )(v 0 )) return YES.

Correctness and exponential-space complexity of Alg-Co-Finit.

Lemma 16. Algorithm Alg-Co-Finit satisfies its specification (i.e., returns YES if (Q × N d ) q 0 (v 0 ) is finite, and NO otherwise).

Proof. We reason analogously as in the proof of Lemma 13. We have already noted that if NO is returned in the point 1, then (Q × N d ) q 0 (v 0 ) is infinite. Assume first that q 0 (v 0 ) V is co-finite and let us show that the algorithm returns YES. Let (q, u) be a control state of V and let i ∈ [1, d]. Since q 0 (v 0 ) V is co-finite, there is a number x ≥ 1 such that q 0 (v 0 ) * -→ V q(u+nxe i ). It follows that (q, u)(xe i ) * -→ V (q 0 , u 0 )(v 0 ), which also entails that (q, u)(ωe i ) covers (q 0 , u 0 )(v 0 ) in V . We have proved that the algorithm returns YES.

Assume now that the algorithm returns YES and let us prove that q 0 (v 0 ) V is co-finite. Since (q, u)(ωe i ) covers (q 0 , u 0 )(v 0 ) in V for every control state (q, u) of V and for every i ∈ [1, d], there is a (large enough) number x such that (q, u)(xe i ) covers (q 0 , u 0 )(v 0 ) for every control state (q, u) and every i ∈ [1, d]. Below we prove that every configuration q(v) of V such that v ≥ nx is reachable from q 0 (v 0 ); this will entail that q 0 (v 0 ) V is co-finite (i.e., (Q

× N d ) q 0 (v 0 ) V is finite).
We thus fix an arbitrary q(v) and i ∈ [1, d] such that v(i) ≥ nx. Let (q, u)(v ) be the configuration of V corresponding to q(v); hence v = u + nv . Since (q, u)(xe i ) covers (q 0 , u 0 )(v 0 ) in V , there is v 0 ≥ v 0 such that (q, u)(xe i ) * -→ V (q 0 , u 0 )(v 0 ); this entails q 0 (u 0 +nv 0 ) * -→ V q(u+nxe i ).

Since v(i) ≥ nx, we have v -xe i ≥ 0. By monotonicity we derive

q 0 (u 0 +nv 0 +n(v -xe i )) * -→ V q(u+nxe i +n(v -xe i )) = q(v).
By the definition of n, we get

q 0 (v 0 ) * -→ V q 0 (v 0 +n(v 0 -v 0 )+n(v -xe i )) = q 0 (u 0 +nv 0 +n(v -xe i )).
Hence we indeed have q 0 (v 0 ) * -→ V q(v).

Lemma 17. Algorithm Alg-Co-Finit works (i.e., can be implemented to work) in exponential space.

Proof. This is analogous to the proof of Lemma 15. We just note that deciding if (q, u)(ωe i ) covers (q 0 , u 0 )(v 0 ) is even easier than deciding if (q, u)(0) covers (q 0 , u 0 )(v 0 ), since the i-th component can be simply ignored.

Applications of the Co-Emptiness Problem

A motivation for the study in this paper has been the decidability proof for structural liveness in [START_REF] Jančar | Deciding structural liveness of Petri nets[END_REF], which is based on a particular version of the co-emptiness problem. We now give more details (in the framework of VASSs, which is equivalent to the framework of Petri nets used in [START_REF] Jančar | Deciding structural liveness of Petri nets[END_REF]), and some partial complexity results. The main aim is to attract a further research effort on this topic, since the complexity of various related problems has not been answered. In particular, we have no nontrivial complexity bounds for the structural liveness problem (besides its decidability).

Assuming a VASS V = (d, Q, A, T ), we are now particularly interested in the co-emptiness of D V for downward closed sets D ⊆ Q × N d , which constitute a subclass of semilinear sets. We use the notation

↓ C = {q(v) | v ≤ v for some q(v ) ∈ C} for the downward closure of a set C ⊆ Q × N d (of configurations of V). We say that C ⊆ Q × N d is downward closed if ↓ C = C.
We write just ↓ q(v) instead of ↓ {q(v)}. Downward closed sets are semilinear since each such set can be presented as

↓ q 1 (v 1 ) ∪ ↓ q 2 (v 2 ) ∪ • • • ∪ ↓ q m (v m )
for some m ∈ N and vi ∈ (N ∪ {ω}) d (i ∈ [1, m]), where we put

↓ q(v) = {q(v) | v ≤ v, v ∈ N d }.
(Recall that k < ω for each k ∈ N.) Later we use another natural presentation of downward closed sets: for each q ∈ Q we provide a constraint in the form of a (finite) conjunction of disjunctions of atomic constraints of the form v(i) ≤ c where i ∈ [1, d] and c ∈ N (then q(v) ∈ Q × N d is in the set iff v satisfies the constraint associated with q). The DCIS co-emptiness problem where "DCIS" stands for "Downward Closed Initial Sets of configurations" (i.e., given V = (d, Q, A, T ) and a downward closed set

D ⊆ Q × N d , is D V = Q × N d ?
) is decidable by Theorem 3 (and the fact that D is semilinear). The complexity is open, even the reductions to/from the reachability problem are unclear. Now we explain the previously mentioned motivation for such studies.

Liveness of transitions and configurations. We recall some standard definitions and facts. Given a VASS V = (d, Q, A, T ), a transition t ∈ T is enabled in a configuration q(v) if t is of the form t : q a -→ q and v + a ≥ 0; a transition t is live in q(v) if for every q(v) ∈ q(v) there is q (v ) ∈ q(v) such that t is enabled in q (v ); a transition t is dead in q(v) if there is no q (v ) ∈ q(v) such that t is enabled in q (v ).

We note that t is not live in q(v) iff t is dead in some q (v ) ∈ q(v) . The next proposition (which also defines D t,V and D V ) is obvious, due to monotonicity.

Proposition 18. Given a VASS V = (d, Q, A, T ), for each t ∈ T the set

D t,V = {q(v) | t is dead in q(v)}
is downward closed. Hence also the set

D V = {q(v) | some t ∈ T is dead in q(v)} = t∈T D t,V is downward closed. Given a VASS V = (d, Q, A, T ), a configuration q(v) is live if each t ∈ T is live in q(v), i.e., if q(v) * -→ V D V . A VASS V is structurally live if it has a live configuration, hence if the set L V = {q(v) | q(v
) is a live configuration of V} is nonempty. While the membership problem for (D t,V or) D V is essentially a version of the (non)coverability problem, which also allows to construct a natural presentation of the (downward closed) sets D t,V and D V , the membership problem for L V is close to the reachability problem as was already noted by Hack [START_REF] Hack | The recursive equivalence of the reachability problem and the liveness problem for Petri nets and vector addition systems[END_REF] long time ago.

The set L V is indeed more involved than D V ; it is obviously not downward closed but it is not upward closed either (in general), and it can be even nonsemilinear; we can refer to [START_REF] Jančar | Deciding structural liveness of Petri nets[END_REF] for a concrete example, as well as for the following idea of decidability.

The structural liveness can be decided as follows. We recall the reversed VASS V ← , and note that V is not structurally live iff D V V ← is co-empty:

Proposition 19. For any VASS V = (d, Q, A, T ) we have D V V ← = (Q × N d ) L V . Hence V is not structurally live iff D V V ← = Q × N d . Proof. We recall that q(v) is not live iff q(v) V ∩ D V = ∅ (i.e., iff q(v) * -→ V q (v )
where some t ∈ T is dead in q (v )). Hence q(v) is not live iff q (v ) * -→ V ← q(v) for some q (v ) ∈ D V (using Proposition 11).

Therefore

D V V ← = (Q × N d ) L V .
Proposition 19 allows us to decide structural liveness of a given VASS V = (d, Q, A, T ) by a reduction to the co-emptiness problem, using the abovementioned constructability of D V .

Structural deadlock-freedom and DCIS co-emptiness. We have shown that the complementary problem of the structural liveness problem (hence "non structural liveness") can be reduced to the DCIS co-emptiness problem (with downward closed sets of initial configurations). However, we have no reduction from the latter problem to the former.

We now show that a special form of structural liveness, namely structural deadlock-freedom, is closely related to the DCIS co-emptiness problem. We use the previously mentioned presentation of downward closed sets by conjunctions of disjunctions of atomic constraints of the form v(i) ≤ c (for each q ∈ Q).

Given a VASS V = (d, Q, A, T ), a configuration q(v) is deadlock-free if every configuration in q(v) enables some transition. A VASS V is structurally deadlock-free if it has a deadlock-free configuration. The structural deadlockfreedom problem asks, given a VASS V, if V is structurally deadlock-free.

In the rest of this section we prove the following theorem.

Theorem 20. The complementary problem of the structural deadlock-freedom problem is polynomially interreducible with the DCIS co-emptiness problem. This entails that the structural deadlock-freedom problem is decidable.

We have already noted that the DCIS co-emptiness problem is decidable. The interreducibility claimed in Theorem 20 is proven in the rest of this section. We first define the set

S V = {q(v) | no t ∈ T is enabled in q(v)}
of "sink configurations" or "deadlocks" (hence S V = t∈T D t,V ). It is obvious that S V is the downward closed set described so that to each q ∈ Q we attach the constraint

(q a -→q )∈T i∈[1,d] a(i)<0 v(i) ≤ -a(i) -1 .
This presentation of S V can be clearly constructed in polynomial time, when given a VASS V. Hence Proposition 21 entails the "left-to-right" reduction in Theorem 20 (recall that V ← denotes the reversed VASS of V). The other reduction is shown by Proposition 22.

Proposition 21. A VASS V is not structurally deadlock-free iff S V V ← is coempty.

Proof. We consider a VASS V = (d, Q, A, T ), and observe that q(v) is not deadlock-free iff q(v) V ∩ S V = ∅. Hence q(v) is not deadlock-free iff q(v) ∈ S V V ← (using Proposition 11). It follows that V is not structurally deadlockfree iff

S V V ← = Q × N d .
Proposition 22. Given a VASS V and a downward-closed set D of configurations, we can construct, in polynomial time, a VASS V such that D V is co-empty iff V is not structurally deadlock-free.

Proof. Let us assume a VASS V = (d, Q, A, T ) and a downward-closed set D of configurations given, for each q ∈ Q, by conjunctions of disjunctions of atomic constraints of the form v(i) ≤ c. By negating these formulas, we derive, in polynomial time, a collection (B q ) q∈Q of finite subsets of N d such that

(Q × N d ) D = {q(v) | v ≥ b for some b ∈ B q }.
(Hence (B q ) q∈Q represents the upward closed complement of D.)

We now define the VASS V = (d, Q, Â, T ) as follows:

a) Q = Q ∪ {(q, b) | q ∈ Q, b ∈ B q }.
b) T consists of the following transitions:

i. q -b --→ (q, b) and (q, b) b -→ q for all q ∈ Q, b ∈ B q , and ii. (q, b) a+b --→ q for all (q a -→ q ) ∈ T and b ∈ B q .

c) Â = {â | q â -→ q ∈ T for some q, q ∈ Q}.

It is obvious that for all configurations q(v) and q (v ) of V we have that q(v) * -→ V q (v ) implies q(v) * -→ V q (v ) but the converse does not hold in general. We will show that

D V ← = Q × N d iff V is not structurally deadlock-free.
The proof will be finished, by taking V = V ← (and noting that (V ← ) ← = V).

(⇒) Assume D V ← = Q×N d . Observe that (q, b)(v) b -→ q(v+b) in V for every (q, b) ∈ Q and v ∈ N d . We now show that no configuration q(v) with q ∈ Q is deadlock-free in V, which clearly entails that V is not structurally deadlock-free.

Let us fix some q(v) ∈ Q × N d . Since q(v) ∈ D V ← , there are a 1 , . . . , a m ∈ A and q 0 (v 0 ), . . . , q m (v m ) ∈ (Q × N d ) such that q(v) = q 0 (v 0 ) Proposition 11). Moreover, we may assume w.l.o.g. that q i (v i ) ∈ D for all i ∈ [0, m-1]. So for each i ∈ [0, m-1] there is b i ∈ B qi such that v i ≥ b i . We derive that

a1 -→ q 1 (v 1 ) a2 -→ • • • q m-1 (v m-1 ) am --→ q m (v m ) ∈ D in V (recall
q i (v i ) -bi --→ (q i , b i )(v i -b i ) ai+1+bi -----→ q i+1 (v i+1 ) in V
for all i ∈ [0, m-1]. It follows that q(v) * -→ q m (v m ) in V. Since q m (v m ) ∈ D then v m ≥ b for all b ∈ B qm ; hence no transition of V is enabled in q m (v m ), and q(v) is thus not deadlock-free in V.

(⇐) Assume that V is not structurally deadlock-free. We fix a configuration q(v) of V and prove that q(v) ∈ D V ← . Since q(v) is also a configuration of V, it is not deadlock-free in V. So there is a configuration q (v ) of V such that q(v) * -→ V q (v ) and no transition t ∈ T is enabled in q (v ). Since V contains the transition (q, b) b -→ q for every q ∈ Q and b ∈ B q , we get that q ∈ Q. No transition q -b --→ (q , b) of T is enabled in q (v ), so v ≥ b for every b ∈ B q . It follows that q (v ) ∈ D. Since q(v) * -→ V q (v ) implies q(v) * -→ V q (v ), we get q(v) * -→ V D, i.e., q(v) ∈ D V ← .

Conclusion

Motivated by the structural liveness problem for VASS, whose computational complexity is still open, we have introduced and studied in this paper the coemptiness problem and the co-finiteness problem for VASS. The complexity of the co-emptiness and co-finiteness problems in the case of single initial configurations has been clarified, but the complexity of general versions has been left open, even w.r.t. reductions to/from the reachability problem. This requires further work, in particular with an eye to the applications aiming to clarify structural liveness properties of VASSs, or equivalently of Petri nets.

This work was supported by the grant GA ČR:18-11193S of the Czech Grant Agency (P. Jančar) and by the grant ANR-17-CE40-0028 of the French National Research Agency ANR, project BraVAS (J. Leroux and G. Sutre)


Christophe Odin
email: christophe.odin@univ-rennes1.fr

Repetitive experiments of one or two-pulse sequences in NQR of spins I=3/2 : Liouville space, steady-state, Ernst angle and optimum signal

Keywords: Nuclear Quadrupole Resonance NQR, Liouville Space, Progressive Saturation, steady-state, Spins I=3/2, 35 Cl NQR, Ernst angle, chloranil

    Repetitive experiments of one or two-pulse sequences in NQR of spins I=3/2: Liouville space, steady-state, Ernst angle and optimum signal Christophe Odin

Introduction

Nuclear Quadrupole Resonance is a powerful resonance method that probes directly the splitting of the energy levels of the spins I ≥ 1 by the quadrupolar interaction [START_REF] Suits | Handbook of Applied Solid State Spectroscopy[END_REF], [START_REF] Wulfsberg | Nuclear Quadrupole Resonance (NQR) Spectroscopy[END_REF]. Since its discovery in the 1950s [START_REF] Dehmelt | Kernquadrupolfrequenzen in festem Dichlorathylen[END_REF], [START_REF] Dehmelt | Kernquadrupolfrequenzen in kristallinen Jodverbindungen[END_REF], [START_REF] Dehmelt | Quadrupolresonanzfrequenzen des kristallinen Broms[END_REF], [START_REF] Dehmelt | Quadrupol-Resonanzfrequenzen von Cl-und Br-Kernen in kristallinem Dichlorthylen und Methylbromid[END_REF], [START_REF] Bloom | Free magnetic induction in nuclear quadrupole resonance[END_REF], [START_REF] Das | Nuclear Quadrupole Resonance Spectroscopy[END_REF] , it is widely used in condensed-matter physics, for instance for the study of phase transitions or polymorphism, and has also biophysical or pharmaceutical applications [START_REF] Balchin | Potential of Nuclear Quadrupole Resonance in Pharmaceutical Analysis[END_REF], [START_REF] Latosinnska | Nuclear Quadrupole Resonance spectroscopy in studies of biologically active molecular systemsa review[END_REF], [START_REF] Perez | Utilization of pure nuclear quadrupole resonance spectroscopy for the study of pharmaceutical crystal forms[END_REF], [START_REF] Latosinnska | Applications of nuclear quadrupole resonance spectroscopy in drug development[END_REF], [START_REF] Limandri | Nuclear Quadrupole Resonance: A Technique to Control Hydration Processes in the Pharmaceutical Industry[END_REF], [START_REF] Chen | Authentication of Medicines Using Nuclear Quadrupole Resonance Spectroscopy[END_REF].

The experimental NQR set-up is identical to NMR, but no strong static external magnetic field is needed. NQR has advantages and drawbacks compared to NMR. In NMR, the Zeeman interaction is the dominant interaction, and all other interactions (dipolar, chemical shift, quadrupolar, etc...) should be treated as a perturbation to first or second order. Thus, the value of the resonance frequency is mainly given by the Zeeman interaction, and represents typically a few ppm of the main Larmor frequency. The frequency shift depends on the relative orientation of the Principle Axis System (PAS) of the interaction tensor with respect to the main static magnetic field, and powder samples lead to broad powder spectra with typical shapes that include steps and divergences. The excitation by the radio-frequency (RF) field may be orientation dependent if the RF power is not strong compared to the truncated dipolar, CSA or quadrupolar interactions.

In contrast to NMR, the quadrupolar interaction is the main interaction in NQR : dipolar and Zeeman interactions are small compared to the quadrupolar interaction. As the interaction is directly probed by the RF field, the splitting of the energy levels that depends on the mean quadrupolar interaction are strong function of temperature, pressure, or any small perturbation that affects the Electric Field Gradient (EFG) at the nuclei (bond lengths, strains, local defects, charge transfer etc...). This sensitivity that can be used to detect very small structural or electronic changes, is one of the main advantages of NQR. But it is also its main drawback because the NQR resonance frequency is not known a priori, and may be long to be found. In NQR, both excitation and detection depend on the relative orientation of the coil with respect to the PAS of the EFG. In particular, when a powder sample with a single quadrupolar site in NMR would give a broad spectrum because all PAS orientations with respect to the external static magnetic field have a different frequency, in NQR only one line is observed, because the energy splitting is not a function of orientation Experimentalist have always been concerned with the problem to determine the optimum conditions to obtain an improvement in signal to noise ratio in NMR and NQR experiments, because of their low sensitivity. The co-addition of signals from successive experiments imposes that the recycle time should be at least five times longer than the longest relaxation time of the system, to ensure that the initial state is at thermodynamical equilibrium. In NMR, the question of whether experiments could be performed with shorter recycle times has been addressed as early as 1958 [START_REF] Carr | Steady-State Free Precession in Nuclear Magnetic Resonance[END_REF], in particular the importance of the steady-state that results of the competition between the pulses of the sequence that create and mix-up populations and coherences, and the free evolution periods where populations and coherences relax back to their equilibrium values.

The theory of progressive saturation experiments developed by Ernst and

Anderson [START_REF] Ernst | Application of Fourier transform spectroscopy to magnetic resonance[END_REF] for isolated spins I=1/2 calculated the effects on the NMR signal of the repetition of identical single pulses separated by a recycle time not long enough to allow the system to relax completely to its thermal equilibrium state. The theory considered the contribution of both longitudinal T 1 and transversal T 2 relaxation times [START_REF] Ernst | Application of Fourier transform spectroscopy to magnetic resonance[END_REF][START_REF] Freeman | Fourier transform study of NMR spin lattice relaxation by "progressive saturation[END_REF][START_REF] Freeman | Phase and intensity anomalies in Fourier transform NMR[END_REF][START_REF] Jones | Fourier transform nuclear magnetic resonance I.repetitive pulses[END_REF]. Simple results were obtained when the coherences have been irreversibly cancelled by some means (for instance with a strong field gradient pulse applied between two RF pulses), it was shown that the longitudinal magnetization attains a well defined steadystate during the recycle time.

For a hard pulse of angle β applied at resonance, the well known and celebrated Ernst-Anderson formula for I=1/2 are

M sst = 1 -e -T /T 1 1 -cos(β)e -T /T 1 M eq (1)
S NMR sst

(β) = 1 -e -T /T 1 1 -cos(β)e -T /T 1 sin(β)M eq ( 2
)
where M sst and S NMR sst are the steady-state magnetization and signal respectively, T is the recycle time. The signal at given recycle time T presents a maximum as a function of pulse length for the Ernst angle

cos(β) = e -T /T 1 (3)
The aim of this article is to consider the case of NQR of spins I=3/2. To the best of our knowledge, the steady-state of fast repetitive experiments in NQR was only considered for I=1 spins [START_REF] Ferrari | 14N pulsed nuclear quadrupole resonance. 3. Effect of a pulse train. Optimal conditions for data averaging[END_REF] for single pulse sequence and complete decay of the coherences during the recycle time, and compared to Recently, we calculated in the Liouville space the steady-state density vector of a system subjected to a train of single or two-pulse sequences ( [START_REF] Odin | Quadrupolar solid-state {NMR} and repetitive experiments: Some aspects in the Liouville space. Application to spins I=1[END_REF]),

with periodic repetition at the recycle time rate. The formula were obtained as a function of the pulse and free-evolution super-operators with a few hypothesis, and can also be applied to NQR. By combining these formal solutions to a formalism that we developed for NQR of spins 3/2 [START_REF] Odin | Calculations of Multipulse Sequence in NQR of Spins 3/2[END_REF], [START_REF] Odin | Broadband Echo Sequence Using a π Composite Pulse for the Pure NQR of a Spin I = 3/2 Powder Sample[END_REF], it is shown in this article that explicit formula for the signal, in the hypothesis that the coherences have decayed during the recycle time, can be obtained.

Theory of repetitive experiments in NQR of spins I=3/2

The continuous excitation of a system by periodic pulse sequences, with a period given by the recycle time T , will produce a steady-state that is independent of the initial conditions. However, the resulting steady-state depends on both the pulse sequence and how the recycle time compares to the population and coherence relaxation times. Recently, we calculated a general solution for a one and two-pulse sequence in the Liouville space ( [START_REF] Odin | Quadrupolar solid-state {NMR} and repetitive experiments: Some aspects in the Liouville space. Application to spins I=1[END_REF]), from rather general hypothesis. Moreover, we developed a simplified formalism of NQR of spins I=3/2 ([23], [START_REF] Odin | Broadband Echo Sequence Using a π Composite Pulse for the Pure NQR of a Spin I = 3/2 Powder Sample[END_REF]), that can be directly used in the Liouville space. The aim of this section is to present a summary of the steady-state solutions obtained in the Liouville space, and to apply them to NQR of spins I=3/2.

Steady-state in the Liouville space

In the Liouville space, the density vector |ρ obeys equation

∂|ρ ∂t = L(|ρ(t) -|ρ eq ) ( 4 )
with L = (-iH l + R) the Liouvillian. H l is the Liouville super-operator associated to the interaction hamiltonian, and R is the relaxation superoperator. |ρ eq is the equilibrium density vector.

The formal solution of Eq. [START_REF] Dehmelt | Kernquadrupolfrequenzen in kristallinen Jodverbindungen[END_REF] for free-evolution is

|ρ(t) = E t |ρ(0) + (I -E t ) |ρ eq with E t = e L t ( 5
)
where I is the identity operator. The free evolution propagator operator E t is non unitary because relaxation is an irreversible process. The two superoperators H l and R do not commute in general, so that the free evolution propagator is not the product of two exponential super-operators.

Given a pulse sequence that consists of pulses of rectangular shape, RF power and phase, and free evolution periods of fixed duration, a repetitive experiment is the repetition of this pulse sequence followed by a free evolution period of duration T. The repetition is periodic with a period of length close to T.

Such experiments are illustrated in Fig. 1(left), for a single pulse or solidecho repetitive experiments. The pulses mix populations and coherences, while the free evolution period mix coherences of same order, and drives them back to equilibrium. At equilibrium, the coherences have decayed to zero, and the populations are fixed by thermodynamical equilibrium. When the recycle time is much longer than the largest relaxation time, the density matrix before each sequence is the equilibrium value and each sequence starts with the same initial density vector. On the other hand, when the recycle time has not allowed the system to relax back to equilibrium during the recycle time, a competition arises between the pulses and the free evolution periods that leads to a steady-state due to a dynamical equilibrium.

| n > | n+1 > T T | n+2 > | n > | n+1 > T T | n+2 > Y X X X Y Y x PAS y PAS z PAS n Coil
The steady-state solutions were calculated in [START_REF] Odin | Quadrupolar solid-state {NMR} and repetitive experiments: Some aspects in the Liouville space. Application to spins I=1[END_REF]. For a one pulse sequence, we obtained

|ρ sst = (I -EP) -1 (I -E)|ρ eq ( 6
)
where the free evolution (including relaxation) of duration T is represented by the super-operator E = E T , and P is the pulse super-operator. Equation.6

is the super-operator generalization for a general spin I≥1/2 of the Ernst-Anderson equation obtained for NMR of an isolated spin I=1/2. The steadystate is independent of the initial conditions.

For a two pulse sequence

(P 1 ) -τ 2 -(P 2 ) -T -, |ρ sst = (I -EP 2 E τ 2 P 1 )) -1 (I -E + EP 2 (I -E τ 2 ))|ρ eq (7)

NQR of spins 3/2

In NQR, the quadrupolar interaction is considered as being much larger than other interactions : dipolar interactions, Zeeman interaction if a small static magnetic field is present, and the Radio-Frequency (RF) field Hamiltonian when a pulse is applied. Exact solutions for NQR of spins I=3/2 were obtained by Pratt et al. [START_REF] Pratt | Transient response of a quadrupolar spin system in zero applied field[END_REF]. In this section, we summarize the principal equations of the formalism that we developed in [START_REF] Odin | Calculations of Multipulse Sequence in NQR of Spins 3/2[END_REF] for the special case of spins I=3/2. The Zeeman and dipolar interactions are neglected, to treat only the case of a spin subjected to a strong quadrupolar interaction and a RF field in the coil direction.

The principal axis system PAS of the Electric Field Gradient (EFG) is oriented with its z axis along the eigenvector corresponding to the largest eigenvalue of the EFG in absolute value. The spin operators are defined in this PAS. In the PAS, the quadrupolar hamiltonian is then

H q = eM Q V zz 12 3I 2 z -I(I + 1) + η 2 (I 2 + + I 2 -) (8)
where

M Q is the quadrupole moment, η = Vxx-Vyy Vzz the EFG asymmetry parameter 0 ≤ η ≤ 1 with the convention |V xx | ≤ |V yy | ≤ |V zz |, and V zz = eq
the EFG at the nucleus under study.

During a pulse of rectangular shape, at irradiation frequency ω, and amplitude ∝ ω RF , the Hamiltonian is written has

H T = H q + H RF = H q + 2ω RF cos(ωt + ϕ)I.n (9)
with n = (sin(θ) cos(φ), sin(θ) sin(φ), cos(θ)) the unit vector giving the coil axis direction in the PAS (Fig. 1(left)).

When I = 3 2 , the quadrupolar hamiltonian has two twofold eigenvalues of opposite sign ±

e 2 qM Q 2 1 + η 2 3
, giving the corresponding NQR angular resonance frequency :

ω q = e 2 qM Q 2 1 + η 2 3 ( 10
)
From the Cayley-Hamilton theorem, we deduce that the quadrupolar Hamiltonian is proportional to an operator Q that is its own inverse :

H q = ω q 2 Q Q 2 = I 4
with I 4 the 4x4 identity matrix.

From this formal property, we derived a formalism to calculate the evolution of the operators during a free evolution period, and during a rectangular pulse. Some interesting analogies with the case of spins I=1/2 can be derived [START_REF] Odin | Calculations of Multipulse Sequence in NQR of Spins 3/2[END_REF].

The equilibrium density operator is :

ρ eq = e -Hq kT T r(e -Hq kT ) = I 4 4 -tanh ω q 2kT Q 4 ( 11
)
In the interaction representation, the Hamiltonian during a pulse becomes :

H = ΔωQ λ z + λ (θ, φ) ω RF [cos(ξ)Q λ x + sin(ξ)Q λ y ] (12)
where λ (θ, φ) is a directional parameter (see below). The normalized oper-

ators Q λ x , Q λ y , Q λ z (T r((Q λ α ) 2 ) = 1
) fulfil the usual commutation relations as Cartesian spin operators

[Q λ x , Q λ y ] = iQ λ z and cyclic permutations Q λ x , Q λ y , Q λ z is an orthonormal basis, T r(Q λ α Q λ β ) = δ αβ . Note that Q λ z = Q/2
does not depend on the directional parameter, as expected on physical grounds. In this basis, and forgetting all irrelevant factors and the identity matrix that do not contribute to the signal,

ρ eq ∼ Q λ z ∼ Q z . Angle ξ = π/2 + ϕ, Δω = ω -ω q
is the difference between the angular irradiation frequency and the quadrupolar frequency, and the directional parameter λ (θ, φ) is defined by

λ (θ, φ) = 1 3 + η 2 4η 2 cos 2 (θ) + sin 2 (θ)[9 + η 2 + 6η cos(2φ)] (13)
The minimum and maximum value of the directional parameter are :

λ min = η 3 + η 2
coil along zPAS axis

λ max = 3 + η 3 + η 2 coil along xPAS axis
It is interesting to note that the directional parameter λ averaged over all orientations is a slightly increasing function of η, that varies from < λ > (η=0) ≈ 1.3598 to < λ > (η=1) ≈ 1.3804, while its standard deviation decreases as

< (Δλ ) 2 (η=0) > ≈ 0.3877 to < (Δλ ) 2 (η=1) > ≈ 0.
3087. For a given direction of the coil with respect to the PAS of the EFG, the signal is

S(t, λ ) = λ T r(Q λ + ρ(t)) (14)
where

Q λ + = Q λ x + i Q λ y .
Equations.12 and 14 show that in NQR, although the resonance frequency is independent of the relative orientation of the coil with respect to the EFG PAS, the intensity is a strong function of the direction. The intensity depends on parameter λ (θ, φ) from both the excitation (through an effective radiofrequency power λ ω RF ) and the detection with a factor λ .

Note the analogy with NMR of spins I=1/2, if we assume an effective radiofrequency power λ ω RF , and a detection factor of λ . In pure NMR, we would have λ = 1.

All results given above are valid for a single orientation of the coil with respect to the PAS, that is for a single crystal. When the sample is an isotropic powder, the signal is the average other all orientations θ et φ. In fact, it is easier, either analytically or numerically, to perform the average over λ using the probability density g(λ ) :

S(t) =< S(t, λ ) >= λ max λ min S(t, λ )g(λ )dλ (15)
An analytical expression of g(λ ) as a function of the complete elliptic integral can be found in [START_REF] Odin | Calculations of Multipulse Sequence in NQR of Spins 3/2[END_REF]. From the numerical point of view, it is much easier to perform the average in Eq.15 using a Monte-Carlo integration method, than to use the analytic expression of g(λ ), because it contains a divergence, and the numerical evaluation of complete elliptic integrals is quite computer demanding.

Steady-state in repetitive experiments of NQR of spins 3/2

Using the results of the previous subsections, we see that for a given directional parameter λ , a Liouville space L λ can be defined, of dimension 3. Density vectors can be defined as :

|ρ λ (t) = ⎛ ⎜ ⎜ ⎜ ⎝ ρ λ z (t) ρ λ x (t) ρ λ y (t) ⎞ ⎟ ⎟ ⎟ ⎠ |ρ eq = ⎛ ⎜ ⎜ ⎜ ⎝ ρ eq z 0 0 ⎞ ⎟ ⎟ ⎟ ⎠ |ρ λ + = ⎛ ⎜ ⎜ ⎜ ⎝ 0 λ i λ ⎞ ⎟ ⎟ ⎟ ⎠ |ρ o = ⎛ ⎜ ⎜ ⎜ ⎝ ρ z 0 0 ⎞ ⎟ ⎟ ⎟ ⎠ (16)
The first vector is a general density vector, the second one corresponds to the equilibrium value, the third one corresponds to the detection vector, and the last one to a density vector with only the z component not zero. The scalar product of a density vector with |ρ λ + gives the detected complex signal

s(t, λ ) = ρ λ + |ρ λ (t) = λ (ρ λ x (t) + iρ λ y (t)) ( 17
)
A|B is the scalar product between vectors |A and |B .

Explicit matrices of the super-operators corresponding to free evolution and pulse periods, that apply for one orientation of the crystallite with respect to the coil axis, that is for a given value of λ , are presented below. The superscript λ is no longer written for clarity. Definitions and abbreviations are given in Table .1.

β = ω RF t p v = ω N β Δx = Δω ω RF e qt = exp(-t/T 1q ) ω N = √ Δx 2 + λ 2 e 2t = exp(-t/T 2 ) c u = cos(u) = λ ω N c v = cos(v) s u = sin(u) = Δx ω N s v = sin(v)
ω N = λ , c u = 1, s u = 0, v = λ β.
The free propagator E t is

E t = ⎛ ⎜ ⎜ ⎜ ⎝ e qt 0 0 0 e 2t * cos(Δω t) -e 2t * sin(Δω t) 0 e 2t * sin(Δω t) e 2t * cos(Δω t) ⎞ ⎟ ⎟ ⎟ ⎠ (18)
The pulse super-operators are

P x = ⎛ ⎜ ⎜ ⎜ ⎝ c 2 u (c v -1) + 1 c u * s u (1 -c v ) c u * s v c u * s u (1 -c v ) c v + c 2 u (1 -c v ) -s u * s v -c u * s v s u * s v c v ⎞ ⎟ ⎟ ⎟ ⎠ (19)
and

P y = ⎛ ⎜ ⎜ ⎜ ⎝ c 2 u (c v -1) + 1 -c u * s v c u * s u (1 -c v ) c u * s v c v -s u * s v c u * s u (1 -c v ) s u * s v c v + c 2 u (1 -c v ) ⎞ ⎟ ⎟ ⎟ ⎠ (20)
As an example, the signal recorded after a P x pulse when the system is initially with a density vector that has only its z component not equal to zero |ρ o T ∼ (ρ z , 0, 0), like for instance the equilibrium density vector, is calculated as follows :

s P (t, λ ) = ρ λ + |E t P x |ρ o + ρ λ + |(I -E t )|ρ o = ρ λ + |E t P x |ρ o = ( 0 λ i λ ) E t P x ρz 0 0 = ρ z λ 2 Δx ω 2 N (1 -cos(ω N β)) -i λ 2 ω N sin(ω N β) e iΔωt e -t/T 2q (21)
From these super-operators, the steady-state density vector and acquisition signal can be readily calculated from Eq.6, 7 and 17. The solutions are valid for a single crystal experiment.

For a one pulse sequence, The steady-state signal recorded just after the last pulse of the sequence is

s sstP (t, λ ) = ρ λ + |E t P |ρ sst + ρ λ + |(I -E t )|ρ eq = ρ λ + |E t P |ρ sst ( 22
)
The steady-state signal of a two-pulse sequence is

s sstP P (t, λ ) = ρ λ + |E t (P 2 E τ 2 P 1 )|ρ sst + ρ λ + |(I -E t + E t P 2 (I -E τ 2 ))|ρ eq = ρ λ + |E t (P 2 E τ 2 P 1 )|ρ sst + ρ λ + |(E t P 2 (I -E τ 2 ))|ρ eq ( 23
)
The last contribution is the free induction decay due to the relaxation between the two pulses, and excited by the second pulse of the sequence. This

contribution is proportional to 1-exp(-τ 2 /T 1q ) ≈ τ 2 /T 1q because τ 2 /T 1q 1.
For a real echo sequence where τ 2 ∼ T 2q T 1q , this contribution is very small and can be neglected s P P (t, λ ) ≈ ρ λ + |E t (P 2 E τ 2 P 1 )|ρ sst . When a powder sample is used, a steady-state signal is calculated for each value of λ , the signal from Eq.22, 23 and the powder average is calculated from Eq.15. The results and comparison with experiments are described in the next section.

Results

In all this section, the case of a recycle time T that is large enough to let the coherences decay to zero (T 2q T ) is considered. In practice, it corresponds to most experimental conditions. But a word of caution should again be added with regards to the hypothesis of neglecting coherence refocussing.

If this is not verified, then the FID could be distorted in phase and intensity, and the theory presented in this section is no longer valid. How coherences spoil the signal in repetitive experiments is well documented for spins I=1/2 (see for instance [START_REF] Ernst | Principles of Nuclear Magnetic Resonance in One and Two Dimensions[END_REF]). From the theoretical point of view, all calculation are greatly simplified when T 2q T , because the free evolution propagator E T reduces to a very simple matrix which is zero everywhere except the compo-nent E T zz = e qT . The main results are compared to 35 Cl NQR experiments performed on chloranil.

Simulations, Sample and experimental methods

The numerical simulation were directly performed in the Liouville space, or with explicit formula, using home-made functions implemented in Matlab The NQR spectra were acquired after a number of dummy scans of 64 that ensures that the steady-state is reached. For variable pulse length experiments, the maximum pulse length (or pulse angle) was limited by probe arcing or electrical breakdown. Single pulse and two-pulse solid-state echo were used.

Steady-state of a one-pulse sequence

Within the hypothesis of a complete decay of the coherences during the recycle time, the steady-state vector is only along z, and was directly calculated from Eq.6

ρ sst,z = 1 -exp(-T /T 1q ) 1 -exp(-T /T 1q ) P zz ρ eq,z (24)
with P zz the zz component of the pulse super-operator. This formula is valid on or out of resonance, and is completely similar to the spin I=1/2 case and I=1 case [START_REF] Odin | Quadrupolar solid-state {NMR} and repetitive experiments: Some aspects in the Liouville space. Application to spins I=1[END_REF], as expected from the formal analogies described in the previous sections. The consequences of this formula are discussed for NQR, mainly for powder samples.

On resonance : optimum signal and SNR

On resonance, Eq.24 leads to : The corresponding signal is

ρ sst,z = 1 -exp(-T /T 1q ) 1 -exp(-T /T 1q ) cos(λ β) ρ eq,z (25
S(t) =< S(t, λ) >= λ 1 -exp(-T /T 1q ) 1 -exp(-T /T 1q ) cos(λ β) sin(λ β) ( 26
)
where < . > denotes an average over all orientations or λ values present in the sample. For a single crystal, only one λ value is needed. If λ ≡ 1, we recover the NMR case Eq.2 as expected.

For a single crystal, the angle β λ M that gives the maximum signal follows cos(λ β λ M ) = exp(-T /T 1q ), a relationship similar to the Ernst equation Eq.3. Typical nutation curves for a single crystal are presented in Fig. 3(Top).

For each η, three values of λ were considered, the minimum and maximum values, as well as the median. The maximum and nutation curve shape strongly depends on the orientation of the coil in the EFG PAS, and T /T 1q .

The question is now to determine the optimum angle for an isotropic powder, as a function of η. Simulated nutation curves for a powder sample are presented in Fig. 3(Bottom) for η=0, 0.5, 1. For a given η, both the angle giving the maximum signal β M (η) and the maximum values of the curve are decreasing functions of T /T 1q . As can be seen, the effect of the asymmetry parameter on the nutation curves is very small, and can be hardly distinguished by eye. It is a remarkable consequence of the powder average, and of some peculiar properties of the directional parameter λ whose mean and dispersion are almost η independent.

The powder averaged signal can be analytically differentiated as a function of pulse angle β, and the zero of this function will give the maximum signal angle. The result is a non-linear equation that can be solved numerically for each η and ratio T /T 1q :

(λ ) 2 cos(λ β) -exp(-T /T 1q ) [1 -exp(-T /T 1q ) cos(λ β)] 2 = 0 (27)
For completeness, we also studied the pulse angle β 0 that gives a zero signal. In NMR with hard pulses, it would correspond to a π or 180 • pulse.

The results for both angles are presented in Fig. 4(Top). In analogy with NMR, we looked for a relationship between the cosinus of this angle as a function of E = exp(-T /T 1q ). A good fit could be obtained . as cos(β M ) = a + bE for each η.

However, we also found that cos(f β M ) ≈ E whatever η to a good approximation when f = 1.52. These curves are plotted on Fig. 4 Thus, for a powder sample, the angle giving the maximum NQR signal for a one pulse steady-state experiment can be cast in a form analogous to the Ernst Formula :

cos(1.52β M ) ≈ exp(-T /T 1q ) ( 28
)
Following the analogy, we looked whether an NMR-like formula would For each η, the ratio T /T 1q is from top to bottom 5, 3, 1, 0.5, 0.1. Dots are the corresponding nutation curves from the simplified formula Eq.29.

represent the NQR powder averaged nutation curves

S a (t) = 1 -exp(-T /T 1q ) 1 -exp(-T /T 1q ) cos(1.52β) sin(1.52β) (29)
Figure .5 presents the superposition of real NQR nutation curves and simplifed formula as a function of nutation angle for three values of η. The nutation curves are well approximated by Eq.29 for angles less than the optimal angle Eq.28, and the discrepancy increases for larger pulse angles.

However, the overall behavior is well reproduced, and this formula can be used as a rule of thumb to estimate the expected NQR nutation curve from a powder sample.

In practical cases, the question is to obtain the maximum SNR for a given acquisition time, given a pulse angle that gives the maximum signal. The signal s(T /T 1q ) is a function of t q = T /T 1q , an a-dimensional variable. Given a number N of signal accumulations, the SNR will be SN R ∝ √ N s(t q ).

Using N ∼ 1/T with T the recycle time, leads to SN R(t q ) ∼ s(t q ) √ t q (30)

In NMR, Using the signal given by Eq.2, and the Ernst pulse angle, the normalized SNR is

snr(t q ) = SN R(t q ) SN R(0) = 2 t q (1 -e -tq ) (1 + e -tq ) (31)
where here, for NMR, t q = T /T 1 with T 1 the spin-lattice (longitudinal) relaxation time. The SNR was normalized to 1 for t → 0. snr(t q ) is a decreasing function of t q .

We numerically calculated SNR(tq) SNR(0) for NQR, by evaluating Eq.26 at β = β M (η), and the SNR from Eq.30.

After normalization, the results are reported on Fig. 4(bottom) for each η, as well as the NMR result. The NQR curves are practically independent of the asymmetry parameter, and almost overlap the NMR result. As in NMR, reducing the recycle time increases the SNR if the pulse angle is chosen to give the maximum signal. But the gain is quite small, snr ≈ 0.63 when T = 5T 1q and snr ≈ 0.97 when T = T 1q .

One pulse at resonance and out of resonance : comparison with experiments

The steady state density vector for a single pulse out of resonance was found as

ρ sst,z = 1 -exp(-T /T 1q ) 1 -exp(-T /T 1q ) 1 + [( λ ω N ) 2 (cos(λ β) -1)] ρ eq,z (32)
It is easy to verify that this expression reduces to Eq.25 when Δx = 0 because ω N = λ . The signal was then calculated from Eq.21, and averaged over all λ values. and experiment is good for on or out of resonance excitation.

Two pulse echo sequence at resonance

To avoid dead time problems, a solid-echo sequence β x -τ -β y sequence is often used to acquire NQR spectra. From Eq.7, the steady state z-component

ρ z reduces to ρ ∞,z = 1 -exp(-T /T 1q ) [1 -(1 -exp(-τ /T 1q )) cos(λ β)] 1 -exp(-T /T 1q ) exp(-τ /T 1q ) cos 2 (λ β) ρ eq,z (33)
Again, it is valid for a given orientation of the coil in the EFG PAS. This expression is slightly more complicated than for the single pulse because the interpulse delay τ contributes to population relaxation, and the two pulses give a contribution to the denominator. For an echo sequence, τ T , τ being chosen large enough to avoid the dead-time, but as small as possible with respect to T 2q to reduce the signal loss due to the e -2τ /T 2q factor.

That Eq.33 formula is consistent with the single pulse sequence steadystate can be seen by putting τ = T . In that case, the repetitive solid-echo pulse sequence reduces to the repetition of a single pulse, calculated over two periods instead of one. We thus expect to obtain the same formula as Eq.25.

When τ = T , Eq.33 reduces to (assuming ρ eq,z ≡ 1 for simplicity)

A comparison of Eq.34 with experiments is presented in Fig. 7. Again, the agreement of theory and experiments is good.

Conclusion

Explicit formula for the steady-state signal generated by one and twopulse sequences repetitive experiments were obtained and analysed for NQR of spins I=3/2, using a Liouville space approach combined with a specific formalism for NQR of spins I=3/2. The main hypothesis to obtain explicit simple formula is the decay to zero of the coherences during the recycle time.

The effect of powder averaging that affects the excitation and the detection in NQR is discussed in detail. For a single pulse experiment, Ernst-Anderson-like formula for the optimum pulse angle and SNR were obtained for single crystal and powder samples, and compared to the corresponding results in NMR of spins I=1/2. The solid-echo steady-state signal was also obtained. These theoretical results are compared and validated by 35 Cl NQR experiments with a chloranil powder sample.

All these results show that the Liouville-space formalism is an essential tool in deriving NMR/NQR results. From the practical point of view, this article show that recycle times as short as T ≈ T 1q can be used to acquire and accumulate NQR of spins I=3/2 signals.

Further work are in progress to apply this approach to quadrupolar NMR of spins I=3/2.

Figure 1 :

 1 Figure 1: (Left) NQR set-up with the orientation of the coil with respect to the PAS of the EFG tensor. (Right) Repetitive experiments sequences.(Top) Single pulse sequence ;(Bottom) Two-pulse sequence. After a large number of repetitions, the steady-state is independent of the initial conditions, whatever the recycle time. If the recycle time is long enough, typically larger than five times the largest relaxation time, then at each iteration, the density vector before the sequence relaxed to the equilibrium density vector |ρ n = |ρ eq .

[ 27 ]

 27 . Matlab was installed on a laptop Dell Precision M6600 with 8GB of memory, and running an Intel(R) Core(TM) i7-2820QM CPU 2.3GHz. The most efficient implementation of powder averaging other all directions is to generate a set of values of λ from an isotropic distribution of (θ, φ) angles (10 6 or 1.6 10 7 ), to calculate the signal S(t, λ ) for each λ , and to take the mean value at the end. The experiments were performed on chloranil powder (C 6 Cl 4 O 2 tetrachloro-1,4-benzoquinone) with a Bruker AVANCE I 300 spectrometer, using a static Bruker probe. At ambient temperature, the 35 Cl NQR of chloranil gives two lines around 36.8MHz and 36.87MHz Fig.2(Top), with asymmetry parameter of both lines η ≈ 0.2 ([28] [29] [30]). We only used the low frequency line LF. The RF power was ν RF =8 or 9.5 kHz. The spin-lattice relaxation time of the LF line was measured with an inversion-recovery sequence. The best least-square fit with the usual three parameter fit function S(τ ) = ab e -cτ where c = 1/T 1q leads to T 1q ≈15ms (see Fig.2(Bottom)). The coherence relaxation time T 2q was measured by varying the delay between the two pulses of a solid-echo sequence, giving T 2q ≈2.7ms.Since the theory applies only when the coherences have decayed, the minimum recycle time should not be smaller that typically 5 × T 2q ≈13.5ms, a value close to T 1q . It limits the minimum recycle time to T 1q . However, for experimental reasons due to our spectrometer electronics, the minimum recycle time that could be reached was T > 25ms. All experiments were performed for T /T 1q ≥ 2.

)Figure 2 :

 2 Figure 2: (Top) Typical 35 Cl NQR chloranil spectrum at ambient temperature ; (Bottom) Inversion-recovery experiment : LF line integral as a function of waiting time. The continuous line is the best least-square fit that gives a spin-lattice relaxation time T 1q ≈15 ms.

20 -Figure 3 :

 203 Figure 3: NQR nutation curves for a single pulse sequence at resonance for η =0, 0.5 and 1. (Top) Single crystal nutation curves for three values of λ : (dashed line) Maximum of λ , (solid line) Median of λ (1.5, 1.4, 1.32 for η =0, 0.5 and 1 respectively), (dotted line) Minimum of λ . (Bottom) Powder averaged nutation curves. For each η, the ratio T /T 1qis from top to bottom 5, 3, 1, 0.5, 0.1. All the nutation curves were normalized such that the powder nutation curve at η = 0 and T /T 1q =5 has a maximum equal to one.

Figure 4 :

 4 Figure 4: (Top) Angle β M that gives the maximum signal (β M ≤ 60 • ), and β 0 for the first zero of the nutation curve (from top to bottom, η= 0 to 1). Note that the x-axis is in logarithmic scale. ;(Middle) dotted line : cos(β Ernst ) = E for NMR where E = exp(-T /T 1 ) : this is the bisector. Colored continuous lines cos(1.52 β M ) vs E where E = exp(-T /T 1q ) for each η (from top to bottom, η= 0 to 1). ; (Bottom) Normalized SNR(T)/SRN(0) as a function of T /T 1q . The NMR optimal SNR is given by a dotted line.

Figure 5 :

 5 Figure 5: NQR powder averaged nutation curves for a single pulse sequence (solid lines).

Figure. 6

 6 Figure.6 compares the theoretical calcultations to experimental points obtained from 35 Cl NQR on chloranil powder. No free parameters are used for the theoretical calculation (T 1q , T 2q , ω RF and Δω are known), except that the signal amplitude was normalized to one when T /T 1q =5 for both theory and experiment. As shown by Fig.6 the agreement between theory

Figure 6 :

 6 Figure 6: Steady state signal for a one pulse sequence as a function of ratio T /T 1q and pulse angle for the LF line of chloranil. ω RF /(2π) = 9.5kHz. Points are experimental values while continuous lines are theoretical results with no free parameters. (Top) At resonance.From top to bottom, T /T 1q =5, 3, 2 ; (Bottom) Out of resonance with Δω=10kHz that is Δx = Δω/ω RF = 1.053. From top to bottom, T /T 1q =5, 2.

ρ ∞,z = 1 - 2 = ( 1 -

 121 e qT [1 -(1e qT ) cos(λ β)] 1e 2 qT cos 2 (λ β) = (1e qT )(1 + e qT cos(λ β)) 1 -(e qT cos(λ β)) e qT )(1 + e qT cos(λ β)) (1e qT cos(λ β))(1 + e qT cos(λ β)) = (1e qT ) (1e qT cos(λ β))This is exactly the formula obtained for a single pulse sequence.The echo amplitude, or spectrum, is proportional toS P P (t) =< S(t, λ) > = (1e qT ) [1 -(1e qτ ) cos(λ β)]1e qT e qτ cos 2 (λ β) λ sin(λ β) (1cos(λ β))

Figure 7 :

 7 Figure 7: Steady state signal for a two pulse solid echo (β x )-τ -(β y ) sequence at resonance as a function of ratio T /T 1q and pulse angle for the LF line of chloranil. Points are experimental values while continuous lines are theoretical results with no free parameters. ω RF /(2π) = 9.5kHz, τ = 50μs. From top to bottom, T /T 1q =5, 2.

Table 1 :

 1 Definitions and abbreviations used to write the super-operators for NQR of spins

I=3/2. At resonance, Δx = 0,

Table 2 :

 2 (Middle). First, the curves only slightly differ when η varies, and the relationship to E is almost linear. Although it is not perfectly linear, they are all very close to the bisector corresponding to the NMR Ernst formula, with square correlation factor larger than 0.98 as indicated by the last line of Table.2. This table also summarized the result of a linear fit of cos(1.52β) as a function of E, and the slopes are very close to one, with very small intercepts and large square correlation factor R 2 > 0.998. Results of a linear fit of cos(1.52β) as a function of E = exp(-T /T 1q ). The last line gives the correlation coefficients of the NQR results with respect to the bisector.

		η = 0	η = 0.25	η = 0.5	η = 0.75	η = 1
	slope	0.98211	0.98449	0.99014	0.99524	0.99708
	intercept	0.0084287 0.0048277 -0.0034242 -0.010632 -0.013159
	R 2	0.99957	0.99944	0.99912	0.9988	0.99868
	R 2 with bisector 0.98313	0.98373	0.98496	0.98591	0.98622

Acknowledgments : I would like to thank Doctor Bertrand Toudic for his support, and Claire Roiland and Laurent Le Polles for fruitfull discussions.

Funding : This research received FEDER financial support (FEDER 34722-Prin2Tan) for funding NMR spectrometers.