Michel Blockelet

Sylvain Schmitz
email: schmitz@lsv.ens-cachan.fr

Model Checking Coverability Graphs of Vector Addition Systems

Keywords: Vector Addition Systems, CTL, Coverability Properties, Complexity

A large number of properties of a vector addition system-for instance coverability, boundedness, or regularity-can be decided using its coverability graph, by looking for some characteristic pattern. We propose to unify the known exponential-space upper bounds on the complexity of such problems on vector addition systems, by seeing them as instances of the model-checking problem for a suitable extension of computation tree logic, which allows to check for the existence of these patterns. This provides new insights into what constitutes a "coverability-like" property.

Introduction

Vector addition systems (or equivalently Petri nets) are widely employed to reason about concurrent computations. Many decidable problems for vector addition systems are known to be ExpSpace-hard thanks to a proof originally due to Lipton [START_REF] Cardoza | Exponential space complete problems for Petri nets and commutative semigroups[END_REF]. Regarding complexity upper bounds, a key distinction arises between "reachability-like" problems on the one hand, for which no upper-bound is currently known in spite of continuous research on the subject [START_REF] Mayr | An algorithm for the general Petri net reachability problem[END_REF][START_REF] Kosaraju | Decidability of reachability in vector addition systems[END_REF][START_REF] Leroux | Vector addition system reachability problem: a short self-contained proof[END_REF], and "coverability-like" problems on the other hand, for which ExpSpace upper bounds have been derived after the work of [START_REF] Rackoff | The covering and boundedness problems for vector addition systems[END_REF]. The latter class of problems is known to encompass many questions for the analysis of vector addition systems (prominently linear-time model-checking [START_REF] Habermehl | On the complexity of the linear-time -calculus for Petri nets[END_REF]), and related models of concurrency (e.g. [START_REF] Ganty | Verifying liveness for asynchronous programs[END_REF][START_REF] Kaiser | Dynamic cutoff detection in parameterized concurrent programs[END_REF].

We promote in this paper a characterization of "coverability-like" properties as relying on the existence of some witness pattern in the coverability graph [START_REF] Karp | Parallel program schemata[END_REF][START_REF] Hack | Decision problems for Petri nets and vector addition systems[END_REF] of the system-this graph provides a finite abstraction of the system's possible behaviours. This stance is backed up by several results (see e.g. [START_REF] Valk | Petri nets and regular languages[END_REF][START_REF] Finkel | Reversal-bounded counter machines revisited[END_REF][START_REF] Chambart | Forward analysis and modelchecking for trace-bounded WSTS[END_REF] that rely on the same powerful technique: since the coverability graph is finite, the existence of a witness can be checked, yielding the decidability of the property at hand. As the coverability graph might have non primitive-recursive size [START_REF] Cardoza | Exponential space complete problems for Petri nets and commutative semigroups[END_REF], this technique comes however at a very high price-at least at first sight.

We show in this paper that a fragment of existential computation tree logic (ECTL) extended with Presburger constraints on paths enjoys a small model property when checked against runs in coverability graphs, and deduce an Ex-pSpace complexity upper bound for properties expressed in this fragment. These properties encompass many examples of properties testable in exponential space we found in the literature. We further believe the resulting formulae to be quite natural and intuitive (they can express branching properties and the existence of -markings directly), and illustrate this point with several examples.

On the technical side, the proof of this small model property is in the line of similar results shown by [START_REF] Rackoff | The covering and boundedness problems for vector addition systems[END_REF] for the coverability and the boundedness problems, and extended by [START_REF] Yen | A unified approach for deciding the existence of certain Petri net paths[END_REF]; [START_REF] Atig | On Yen's path logic for Petri nets[END_REF]; [START_REF] Demri | On selective unboundedness of VASS[END_REF] to more complex properties. These extensions rely on rather terse, ad-hoc logical formalisms, which are checked against the actual runs of the system-it is tempting to blame the complexity of Yen's logical formalism for the issue found in his proof by Atig and Habermehl. Thus a major contribution of the paper is the key insight that what should be checked are runs in coverability graphs instead of actual runs, and that a reasonably standard logic based on CTL is perfectly usable to this end. In more details, we define a notion of VAS coverability graphs that will constitute the models of our logic (Section 2) and investigate their simulation relations; we define an extension of CTL using Presburger constraints on path and atomic propositions testing for coverability (Section 3.1) before considering the decidability of VAS model-checking for some of its fragments (Section 3.2); we then consider a restricted fragment of eventually increasing formulae and prove its VAS model-checking problem to be ExpSpace-complete (Section 4).

Notations. Let ℤ = ℤ ⊎ { } be the set of integers completed with a limit element , which is larger than any finite in ℤ and verifies + = for all in ℤ. Whenever working on vectors in ℤ for some , we implicitly employ component-wise orderings. We consider throughout the paper rooted labeled transition systems (LTS) = ⟨ , →, ℓ, init ⟩ where, for some ≥ 1, is a set of states, ℓ is a state labeling function from to ℤ , init is the initial state in , and → is a labeled transition relation included in ×ℤ × . In our developments we ignore labels and define the size | | of a LTS as the cardinality of →, and for a set of vectors V ⊆ ℤ , ∥V∥ = max v∈V,1≤ ≤ ,v( )< (0, ⌈log 2 (|v( )|) + 1⌉). An LTS is called tree-shaped if any state has at most one predecessor by →, i.e. for all , |{ ′ ∈ | ′ → }| ≤ 1, and path-shaped if furthermore it has at most one successor by →, i.e. for all , |{ ′ ∈ | → ′ }| ≤ 1.

Coverability Graphs

Let us first recall the definition of coverability graphs for vector addition systems and how they can be used to decide various properties.

Vector Addition Systems. A -dimensional vector addition system ( -VAS) is a pair = ⟨V, x 0 ⟩ where V is a finite set of transitions in ℤ and x 0 an initial marking in ℕ [START_REF] Karp | Parallel program schemata[END_REF]. Formally, we can define the reachability graph of such a -VAS as the (generally infinite) LTS ( ) = ⟨ℕ , →, id , x 0 ⟩ with states (also called markings) in ℕ , the identity id as state labeling function, and transitions labels in V s.t. x a -→ x ′ iff x + a = x ′ (note that it implies x + a ≥ 0). In some proofs, we will consider generalized VAS, where x 0 can be taken from ℤ . We consider several parameters for VAS size, as do [START_REF] Rosier | A multiparameter analysis of the boundedness problem for vector addition systems[END_REF]: the size of the binary encoding of the largest difference a vector from the transitions set can induce ∥V∥, the cardinal of the transition relation |V|, and the dimension .

Canonical Coverability Graph. Coverability graphs are finite abstractions of VAS reachability graphs. In order to remain finite, they employ markings over the complete space (ℕ ⊎ { }) , noted ℕ . There are several possible definitions for coverability graphs, all based on the original Karp and Miller coverability tree construction [START_REF] Karp | Parallel program schemata[END_REF]; here is a particular flavour, as found for instance in [START_REF] Valk | Petri nets and regular languages[END_REF] Given a LTS ⟨ , →, ℓ, init ⟩ and given some 1 ≤ ≤ , let us first define a -antecedent of a pair ( , a) in × ℤ as a state ′ satisfying

init → * ′ -→ ∧ ℓ( ′ ) ≤ ℓ( ) + a ∧ ℓ( ′ )( ) < (ℓ( ) + a)( ) (1)
for some in (ℤ ) * . A -antecedent witnesses the fact that, by repeating the sequence of transitions a from ′ , we can obtain arbitrarily high values in coordinate -which will be represented symbolically by an value in the coverability graph.

The coverability tree of a -VAS = ⟨V, x 0 ⟩ is a tree-shaped LTS ( ) = ⟨ , →, ℓ, init ⟩ with state labels in ℕ and transition labels in V constructed by: basis initially = { init } with label ℓ( init ) = x 0 and init is flagged as unprocessed, step for every unprocessed state and every a in V

• if ℓ( ) + a ∕ ≥ 0: do nothing, as a is not firable in ℓ( ),

• otherwise, let ′ be a fresh state, update to be ⊎ { ′ }, add a transition a -→ ′ , and set the label of ′ in ℕ to

ℓ( ′ )( ) def = { if ∃ ′′ a -antecedent of ( , a) (ℓ( ) + a)( ) otherwise (2)
If there does not exist any state ′′ in with ℓ( ′ ) = ℓ( ′′ ) and init → * ′′ → * , flag ′ as unprocessed; ′ is otherwise a leaf of the tree.

The canonical coverability graph ( ) of a -VAS = ⟨V, x 0 ⟩ is obtained by identifying identically-labeled states in ( ), i.e. it is the quotient ( ) = ( )/≡ for the equivalence relation ≡ ′ iff ℓ( ) = ℓ( ′ ) (see e.g. Figure 1).

Examples of Coverability Properties. Coverability graphs allow to decide many properties on a -VAS ; for instance, coverability given a marking x in ℕ , whether a marking x ′ ≥ x is reachable in ( )-simply check whether a state with ℓ( ) ≥ x is reachable in ( ); for instance in Figure 1 we see that ⟨1, 5, 1⟩ is coverable but ⟨2, 1, 2⟩ is not-, boundedness whether the set of reachable markings in ( ) is finite-this occurs iff no value appears in the label of any state of ( ); for instance in Figure 1 the VAS is not bounded-, place boundedness given a coordinate 1 ≤ ≤ , whether the set of values x( ) for all reachable x in ( ) is finite-this occurs iff no value appears as ℓ( )( ) for some state of ( ); for instance in Figure 1, the second coordinate is unbounded but the other two are bounded, language regularity whether the language, i.e. the set of labels in V * of transition sequences 0 -→ in ( ), is regular-this occurs if no state with a cycle a1⋅⋅⋅a ----→ appears in ( ) s.t. there exists 1 ≤ ≤ , ℓ( )( ) = and ( ∑ =1 a ) ( ) < 0 [START_REF] Valk | Petri nets and regular languages[END_REF], Theorem 5); for instance in Figure 1 we find one such cycle ⟨1, , 1⟩ c -→ ⟨1, , 1⟩, and indeed the language of this VAS yields (ab) c ≤ when intersected with (ab) * c * , and is therefore non-regular.

⟨1, 0, 1⟩ ⟨2, 1, 0⟩ ⟨0, 0, 2⟩ ⟨2, 0, 0⟩ ⟨1, , 1⟩ ⟨2, , 0⟩ ⟨0
All these properties are decidable in exponential space; see [START_REF] Rackoff | The covering and boundedness problems for vector addition systems[END_REF] for the first two, and [START_REF] Demri | On selective unboundedness of VASS[END_REF] for the last two. Observe that we were able to characterize each property by the existence of some witness in the canonical coverability graph; we shall see in Section 3 that we can easily express those properties in a modal logic, and later in Section 4 that the exponential space upper bound applies to all properties expressed in this logic.

Partial Covers. In preparation of the technical developments of the following sections, we define structures related to the coverability graph that will serve as witnesses. The motivation is that later we will build small models for properties by induction on the dimension, thus it will be convenient to consider partial coverability graphs, which are "correct" only on the first coordinates out of .

Definition 2.1. A partial cover for a generalized -VAS ⟨V,

x 0 ⟩ is an accessible LTS ⟨ , →, ℓ, init ⟩ with transition labels in V s.t. ℓ( init ) = x 0 and, if a - → ′ , then for all 1 ≤ ≤ , either ℓ( )( ) + a( ) = ℓ( ′ )( ), or ℓ( )( ) < , ℓ( ′ )( ) =
, and on every path init = 0 a1 -→ ⋅ ⋅ ⋅ a -→ = , there exists 0 ≤ ≤ s.t. is a -antecedent of ( , a) (see ( 1)).

Thus a partial cover does not enforce positive values on the state labels, but guarantees transition labels to be compatible with state labels, and values to be introduced only when legal, i.e. when at least one -antecedent exists on every path from the initial state. Partial covers can also be seen as LTS withantecedency relations-in addition to the transition relation-from a state with a newly introduced value to each of its -antecedents. When constructing partial covers we will need to preserve the existence of at least one suchantecedent.

With the example of Figure 1, the system reduced to the initial marking

⟨1, 0, 1⟩ (3)
is a partial cover, the following are two more (path-shaped) partial covers of the same VAS:

⟨1, 0, 1⟩ a - → ⟨2, 1, 0⟩ a - → ⟨3, 2, -1⟩ (4) ⟨1, 0, 1⟩ a - → ⟨2, 1, 0⟩ b -→ ⟨1, , 1⟩ c - → ⟨1, , 1⟩ , (5)
and this last one is not a partial cover, as we cannot introduce an value at this point:

⟨1, 0, 1⟩ a - → ⟨2, , 0⟩ . (6)
Definition 2.2. Let 0 ≤ ≤ . A partial cover = ⟨ , →, ℓ, init ⟩ is -admissible if for all 1 ≤ ≤ and for all in , 0 ≤ ℓ( )( ).

Note that in particular the initial marking x 0 of a generalized -VAS also needs to satisfy x 0 ( ) ≥ 0 for 1 ≤ ≤ in order for a -admissible partial cover to even exist. Both the canonical coverability graph and the reachability graph of a -VAS are -admissible partial covers. Among the previous examples, (3) and (5) are 3-admissible, (4) is 2-admissible but not 3-admissible. Considering our examples of coverability properties, the LTS in (5) could be used as a witness of coverability of ⟨1, 5, 1⟩, unboundedness in the second coordinate, and non regularity of the language.

Covering Simulations. Among all the -admissible partial covers of a -VAS (Defs. 2.1 and 2.2), we find in particular its canonical coverability graph ( ). All these -admissible partial covers are in fact related to ( ) by a simulation relation (see App. A.1 for details):

Definition 2.3. Let ≥ 1 and 1 = ⟨ 1 , → 1 , ℓ 1 , 1 ⟩ and 2 = ⟨ 2 , → 2 , ℓ 2 , 2 ⟩ be two LTS. A covering simulation between 1 and 2 is a relation ⊆ 1 × 2 s.t. 1. 1 2 , 2. if ′ , then (a) ℓ 1 ( ) ≤ ℓ 2 ( ′ ) and (b) if a -
→ 1 for some a in ℤ and in 1 then there exists ′ in 2 with

′ a - → 2 ′ and ′ .
We say that 2 simulates 1 , noted 1 ≼ 2 , if there exists a covering simulation between 1 and 2 .

Lemma 2.4. Let = ⟨V, x 0 ⟩ be a -VAS and a -admissible partial cover of . Then ≼ ( ).

CTL Logics for Coverability Graphs

We first propose a very general logic based on CTL for model-checking coverability graphs (Section 3.1). Our purpose with this general logic is to motivate our choice of CTL fragment for the following sections: indeed, the full logic will turn out to be too powerful, and we will restrict ourselves to an existential fragment with a decidable model checking problem (Section 3.2).

An Extension of CTL

We define an extension PrCTL ≥ (U) of CTL specifically designed to express properties of VAS coverability graphs. It features coverability constraints ( ) ≥ , where is a constant in ℕ , as atomic formulae, allowing to express that the label in the current state has value greater or equal to in its th coordinate. These extend the usual coverability constraints (see e.g. [START_REF] Esparza | Decidability of model checking for infinite-state concurrent systems[END_REF] by also allowing to express ( ) = .

Presburger-refined temporal modalities U using Presburger formulae to constrain the allowed paths-this is similar to the regular modalities found for instance in [START_REF] Axelsson | Extended computation tree logic[END_REF], but what is constrained here is the effect of a transition sequence rather than its label.

Presburger Formulae. We restrict our attention to quantifier-free Presburger (QFP) formulae, since one such formula can be obtained from any Presburger formula at the expense of a worst-case triple exponential blowup (see e.g. Weispfenning, 1990, Theorem 2.1). More precisely, given an infinite countable set of variables , a QFP formula is defined through

::= ⊤ | ¬ | ∨ | , ::= ≥ | ≡ , ::= 0 | 1 | | + (7)
where is a variable from and ≥ 2.1 Given a vector x of values in ℤ and a formula with free variables 1 , . . . , , we write (x) for the closed formula with x( ) substituted for for each 1 ≤ ≤ . Given a closed Presburger formula , we write PA |= if the formula is valid.

Syntax of PrCTL ≥ (U). Formally, fix some in ℕ; a -formula of PrCTL ≥ (U) is a term defined by the abstract syntax

::= ⊤ | ¬ | ∨ | E( U ) | ( ) ≥
where denotes a QFP formula with free variables, 1 ≤ ≤ , and is a constant in ℕ . Note that a -formula is also a ′ -formula for all ′ ≥ . We can simulate the classical "next" modalities X (see the proof of Proposition 3.1). The classical, unrefined U modality can be defined by

E( U ′ ) def = E( U ⊤ ′ )
using the ⊤ formula of QFP. We also define as usual EF

| = . If a 1 ⋅ ⋅ ⋅ a is a sequence in (ℤ ) * (with = 0 for the empty sequence), then its effect is Δa 1 ⋅ ⋅ ⋅ a = ∑ =1 a in ℤ . A state in satisfies a PrCTL ≥ (U) formula , written |= , in the following inductive cases: |= ⊤ always, |= ¬ iff ∕ |= , |= 1 ∨ 2 iff |= 1 or |= 2 , |= E( U ′ ) iff ∃ = 0 a1 -→ 1 a2 -→ ⋅ ⋅ ⋅ ∈ Paths( ), ∃ ≤ | |, PA |= (Δa 1 ⋅ ⋅ ⋅ a ), |= ′ , and ∀ < , |= , |= ( ) ≥ iff ℓ( )( ) ≥ .
As usual, a LTS satisfies , written |= , if init |= . A -VAS ⟨V, x 0 ⟩ satisfies a PrCTL ≥ (U) -formula , written ⟨V, x 0 ⟩ |= , if there exists a -admissible partial cover of ⟨ , x 0 ⟩ such that |= . We will see later (Proposition 3.2) that for existential PrCTL ≥ (U) this boils down to model-checking the canonical coverability graph.

Examples of Formulae. Consider once more the coverability properties of Section 2: the coverability problem for a marking x can be checked by modelchecking these formulae against ( ):

cov,x def = EF ⋀ =1 ( ) ≥ x( ) ; (8)
unboundedness by

unb def = EF ⋁ =1 ( ) ≥ ; (9) place unboundedness in coordinate 1 ≤ ≤ by unb, def = EF ( ) ≥ ; (10)
non-regularity of the language by

unreg def = EF ⋁ ⊆ {1, . . . , } ∕ = ∅ ⋁ ⊆ ⊆{1,..., } ⎛ ⎝ ⋀ ∈ ( ) ≥ ∧ EF , ⊤ ⎞ ⎠ (11)
where

, ( 1 , . . . , ) def = ⋀ ∈ < 0 ∧ ⋀ ∕ ∈ ≥ 0 . ( 12
)
We can check that the 3-admissible partial cover ( 5) satisfies all these formulae (setting x = ⟨1, 5, 1⟩ for ( 8)), thus our example VAS satisfies all these formulae.

VAS Model Checking

We turn now to the VAS model checking problem: for a VAS = ⟨V, x 0 ⟩ and a PrCTL ≥ formula , does ⟨V, x 0 ⟩ satisfy ?

Undecidability of PrCTL ≥ (U).
When considering how general PrCTL ≥ is, its model-checking problem is rather unsurprisingly undecidable, even if restricted to EF modalities, i.e. for the PrCTL ≥ (F) fragment (the proof uses results by [START_REF] Esparza | Decidability of model checking for infinite-state concurrent systems[END_REF]

; see App. A.2): Proposition 3.1. The VAS model-checking problem for PrCTL ≥ (F) is unde- cidable.

Decidability of PrECTL ≥ (U).

The formulae used in the proof of Proposition 3.1 employ alternation in a crucial way in order to encode the VAS containment problem, and a natural question is whether the existential fragment PrECTL ≥ (U), with syntax

::= ⊤ | ⊥ | ∨ | ∧ | E( U ) | ( ) ≥ ,
is decidable. This is the case: it suffices to check whether the canonical coverability graph satisfies the formula, since by Lemma 2.4 it simulates any other -admissible partial cover. This is one of the benefits of considering CTL fragments rather than ad-hoc logics: the standard toolkit of modal logic is readily applicable, like the connection between simulations and existential CTL (see App. A.3 for details):

Proposition 3.2. The VAS model-checking problem for PrECTL ≥ (U) is de- cidable in nondeterministic polynomial time in | ( )| and | |.
The decidability of VAS model-checking for PrECTL ≥ (U) is encouraging, but our decision procedure relies on the construction of the canonical coverability graph ( ). As the latter can have non primitive-recursive size [START_REF] Cardoza | Exponential space complete problems for Petri nets and commutative semigroups[END_REF], who attribute the idea to Hack), this is not a very efficient algorithm: it yields an Ackermannian upper bound [START_REF] Figueira | Ackermannian and primitive-recursive bounds with Dickson's Lemma[END_REF], Section VII.C) on the complexity of VAS model-checking for PrECTL ≥ (U). This is a ridiculously high upper bound, but we actually suspect the VAS model-checking problem for PrECTL ≥ (U) to be Ackermann-complete. On the one hand, Proposition 3.2 implies the PrECTL ≥ (U) problem to be in NPTime for fixed VAS; on the other hand, small extensions within existential fragments quickly lead to undecidability (e.g. when allowing ( ) < or G ; see App. B.1 for a discussion).

The remainder of the paper is dedicated to a fragment of PrECTL ≥ (F) for which we demonstrate a small model property and deduce decision procedures working in exponential space. Although we use techniques adapted from Rackoff and his successors, several points make these contributions stand out: the simplicity of the logic, its ability to express branching properties directly, and its intuitive semantics in terms of coverability graphs.

Eventually Increasing Formulae

Let us consider the PrECTL ≥ (F) fragment. We are going to introduce a semantic restriction to PrECTL ≥ (F) formulae, inspired by a similar restriction employed by [START_REF] Atig | On Yen's path logic for Petri nets[END_REF] to fix Yen (1992)'s proof.

The PrECTL ≥ (F) Fragment

Eventually Increasing Formulae. We can restrict ourselves to finite treeshaped models for PrECTL ≥ (F) formulae; such a model has a root and a number of leaves 1 , . . . , , each satisfying some coverability constraint (CC) subformula , of form

::= ⊤ | ⊥ | ∧ | ∨ | ( ) ≥ , (13)
where 1 ≤ ≤ and is in ℕ . We call this model increasing if ℓ( ) ≥ ℓ( ) for all 1 ≤ ≤ . A formula of PrECTL ≥ (F) is increasing if all its tree-shaped models are increasing. An eventually increasing formula is a formula of form EF for some increasing formula . We denote the set of (eventually) increasing PrECTL ≥ (F) formulae by (e)iPrECTL ≥ (F). All our example formulae ( 8)-( 11) are eventually increasing. Such a semantic restriction naturally leads to the question: is it decidable whether a formula fits into the fragment? We first consider the related problem of PrECTL ≥ (F) satisfiability: given a -formula , does there exist a -VAS ⟨V, x 0 ⟩ s.t. ⟨V, x 0 ⟩ |= ? It turns out that this satisfiability problem reduces to the satisfiability of its QFP subformulae, which can be checked in NPTime (see App. A.4):

Proposition 4.1. The satisfiability problem for PrECTL ≥ (F) is decidable in NPTime.

Checking whether a formula is increasing is a bit more involved: we need to check whether the various QFP subformulae ensure every possible model is increasing, which we do by constructing a (universal) Presburger formula (see App. A.5): Proposition 4.2. Let be a -formula of PrECTL ≥ (F). Whether is aformula of iPrECTL ≥ (F) is decidable in NPTime.

Small Model Properties

The proof of the small model property for eiPrECTL ≥ (F) formulae follows the general design of Rackoff's proof: first a small model property on models with bounded values (Lemma 4.3) using results on the existence of small solutions for linear integer programming, and then a proof of existence of a small model in general by induction on the dimension (Lemma 4.4).

Bounded Models. Define as usual with Rackoff's approach an ( , )-bounded LTS as an -admissible one where no finite value on the first coordinates is larger than : for all and every 1 ≤ ≤ , ℓ( )( ) ≥ implies ℓ( )( ) = .

If ≤ , the -projection of a formula is a formula | where every ( ) ≥ term of with > and < has been replaced by ⊤. Adapting the proof of (Rackoff, 1978, Lemma 4.5) to our case, we obtain (see App. A.6 for details):

Lemma 4.3 (Small Models for Bounded LTS). Let ⟨V, x 0 ⟩ be a generalized -VAS with > 1, be a PrECTL ≥ (F) formula, and 0 ≤ ≤ and ≥ 0. If there exists an ( , )-bounded partial cover of ⟨V, x 0 ⟩ s.t. |= | , then there exists a tree-shaped ( , )-bounded partial cover ′ of ⟨V, , , , and ).

x 0 ⟩ with ′ |= | and | ′ | ≤ (2 ∥V∥ ) ( +| |) for some constant (independent of V, x 0 ,
General Models. We prove now a general small model property for eiPrECTL ≥ (F) formulae. It borrows several elements from earlier research, prominently (Rackoff, 1978, Lemma 4.6 & 4.7), but also crucially the use of an increasing condition to allow "replaying" a model at a leaf [START_REF] Atig | On Yen's path logic for Petri nets[END_REF]. Given V ⊆ (ℤ ) , a -coverability formula , and some 0 ≤ < , let

(0) def = (2 ∥V∥ ⋅ |V|) ( +| |) ( + 1) def = ( 2 ∥V∥ ⋅ (2 ∥V∥ ( ) + | |) ) ( +| |) + 1 + ( )
where is the constant of Lemma 4.3. We finally obtain our small model property (see App. A.7 for a proof): Lemma 4.4 (Small Model Property). Let ⟨V, x 0 ⟩ be a generalized -VAS and = EF ′ be a -eventually increasing formula. Let | be satisfiable. Then there exists a tree-shaped -admissible partial cover of ⟨V, x 0 ⟩ that models | and of size ≤ ( ). Lemma 4.4 results in a doubly exponential bound on the size of a -admissible model for an eventually increasing formula, from which an ExpSpace algorithm can be designed, which is optimal considering the ExpSpace lower bound [START_REF] Cardoza | Exponential space complete problems for Petri nets and commutative semigroups[END_REF]:

Theorem 4.5 (Complexity of VAS model checking). The VAS model-checking problem for eiPrECTL ≥ (F) formulae is ExpSpace-complete.
See App. A.8 for details. Note that the different parameters on the size of the VAS and of the formula influence this complexity differently: for fixed the obtained algorithm works in PSpace. A matching PSpace lower bound on the place coverability problem is given by Rosier and Yen (1986, Corollary 3.1) for fixed ≥ 4.

Another interesting consequence of our bounds is that bounds for model checking vector addition systems with states (VASS) are easy to derive; for instance by encoding a -VASS with state-space into a ( + 2⌈log 2 | |⌉)-VAS: this is not as tight as the ( + 3)-VAS encoding of [START_REF] Hopcroft | On the reachability problem for 5dimensional vector addition systems[END_REF], but allows to test in which control state we are in an eiPrECTL ≥ (F) formula using coverability constraints ( ) ≥ 1. Thus the number | | of states only influences polynomially the complexity of VASS model checking for eiPrECTL ≥ (F).

Related Work

The first attempt at unifying ExpSpace upper bounds on VAS problems was proposed by [START_REF] Yen | A unified approach for deciding the existence of certain Petri net paths[END_REF]. This provided ExpSpace upper bounds for many problems (boundedness, coverability, self-coverability, etc.; see Section 4 in [START_REF] Yen | A unified approach for deciding the existence of certain Petri net paths[END_REF]). For instance, we can consider the place boundedness problem: a path formula for it has to guess nondeterministically a sequence of introductions of -values leading to the desired unboundedness of place . Let Π be the set of repetition-free sequences over {1, . . . , }∖{ } and |Π| = ; write ( ) for the set of elements appearing in and [ .. ] for the factor of between indices and (inclusive):

∃ 1 , . . . , 2 +2 , ∃ 1 , . . . , 2 +2 ( 0 1 -→ 1 2 -→ ⋅ ⋅ ⋅ 2 +2 ----→ 2 +2 ) ∧ ⋁ ∈Π ⎛ ⎝ 2 +1 ( ) < 2 +2 ( ) ∧ ⋀ ∕ ∈ ( ) 2 +1 ( ) ≤ 2 +2 ( ) ⎞ ⎠ ∧ | | ⋀ =1 ⎛ ⎝ 2 -1 ( [ .. ]) < 2 ( [ .. ]) ∧ ⋀ ∕ ∈ ( [1.. ]) 2 -1 ( ) < 2 ( ) ⎞ ⎠ .
The first main conjunct under the scope of the choice of checks that anvalue can appear in place . The second main conjunct verifies the same for each element of in sequence.

The proof of [START_REF] Yen | A unified approach for deciding the existence of certain Petri net paths[END_REF] was flawed, and corrected by [START_REF] Atig | On Yen's path logic for Petri nets[END_REF] who introduced the increasing restriction to Yen's logic to characterize formulae for which the ExpSpace bound held. Nevertheless, this restriction meant that some of the bounds claimed by Yen did not hold any longer, for instance for the regularity problem, and the above formula for place unboundedness is another instance of a non-increasing formula. [START_REF] Demri | On selective unboundedness of VASS[END_REF] finally proposed to relax the class of models by considering "pseudo-runs" instead of actual runs, and provided a formal framework (general unboundedness properties) to express properties on such runs, allowing him to prove ExpSpace upper bounds for several open problems like place boundedness, regularity, strong promptness, etc. This is the most closely related approach.

We can express general unboundedness properties as PrECTL ≥ (F) formulae, but not as eventually increasing ones, because these properties only enforce local increasing conditions instead of the global one we employed in this work. On the other hand many aspects of eiPrECTL ≥ (F) formulae are beyond the reach of general unboundedness properties, since for instance we allow full Presburger arithmetic, and can nest EF modalities directly (general unboundedness properties would intersperse plain EF modalities between any two Presburger-refined modalities). This opens the question whether we could design a larger fragment of PrECTL ≥ (F) with an ExpSpace-easy VAS model-checking problem and capturing general unboundedness properties.

We believe eiPrECTL ≥ (F) formulae to be much easier to write than general unboundedness properties; for instance for place unboundedness, one would also have to write explicitly all the different permutations on the order in whichvalues can be introduced in a general unboundedness property, instead of the straightforward formula (10).

A Omitted Proofs

A.1 Proof of Lemma 2.4

Lemma A.1. Let = ⟨V, x 0 ⟩ be a -VAS and a -admissible partial cover of . Then ≼ ( ).

Proof. Let = ⟨ , →, ℓ, 0 ⟩ be a -admissible partial cover of and ( ) =

⟨ ′ , → , ℓ ′ , ′ 0 ⟩ its CCG. Let us show that Claim A.1.1. If 0 a1⋅⋅⋅a ----→ in , then there exists ′ in ′ s.t. ′ 0 a1⋅⋅⋅a ----→ ′ in ( ) and ℓ( ) ≤ ℓ ′ ( ′ ).
The claim is trivially true for = 0, and for the induction step, assume

0 a1⋅⋅⋅a ----→ a +1 ---→ +1 in with ′ 0 a1⋅⋅⋅a ----→ ′ and ℓ( ) ≤ ℓ ′ ( ′ ) by induction hypothesis. Since a +1
---→ +1 and ℓ( ) ≤ ℓ ′ ( ′ ), the transition a +1 can also be fired from ′ , leading to some ′ +1 . Now, by definition of -admissibility (see Definition 2.2), for every 1 ≤ ≤ , either 1. ℓ( +1 )( ) < and thus ℓ ′ ( ′ +1 )( ) ≥ ℓ( +1 )( ) by monotonicity, or 2. ℓ( +1 )( ) = and two cases arise:

• if ℓ( )( ) = , then ℓ ′ ( ′ )( ) = = ℓ ′ ( ′ +1 )( ), or
• there exists a -antecedent of ( , a +1 ) on the path 0 a1⋅⋅⋅a ----→ in , thus by induction hypothesis on ≤ , ℓ ′ ( ′ ) ≥ ℓ( ). We proceed by contradiction: assume that ℓ

′ ( ′ +1 )( ) = (ℓ ′ ( ′ ) + a +1 )( ) < . By definition of a -antecedent (see (1)), ℓ( )( ) < (ℓ( ) + a +1 )( ) = (ℓ( ) + Δa +1 ⋅ ⋅ ⋅ a +1 )( ) , (14) hence (Δa +1 ⋅ ⋅ ⋅ a +1 )( ) > 0 and ℓ ′ ( ′ )( ) < (ℓ ′ ( ′ ) + Δa +1 ⋅ ⋅ ⋅ a +1 )( ) = (ℓ ′ ( ′ ) + a +1 )( ) < .
(15) Furthermore, for every 1 ≤ ≤ with ∕ = , either ℓ( )( ) = and then ℓ

′ ( ′ )( ) = = ℓ ′ ( ′ +1 )( ), or ℓ( )( ) < and thus ℓ( )( ) < and (ℓ( ) + a +1 )( ) = (ℓ( ) + Δa +1 ⋅ ⋅ ⋅ a +1 )( ) ≥ ℓ( )( ) implies (Δa +1 ⋅ ⋅ ⋅ a +1 )( ) ≥ 0: therefore ℓ ′ ( ′ )( ) ≤ (ℓ ′ ( ′ ) + a +1 )( ) by monotonicity. Thus overall ℓ ′ ( ′ ) ≤ ℓ ′ ( ′ ) + a +1 and ℓ ′ ( ′ )( ) < (ℓ ′ ( ′ ) + a +1 )( ), i.e. ′ is a -antecedent for ( ′ , a +1 ), in contradiction with ℓ ′ ( ′ +1 )( ) < .
Returning to the main proof, let us show that the relation

= {( , ′ ) ∈ × ′ | ∃a 1 ⋅ ⋅ ⋅ a ∈ V * , 0 a1⋅⋅⋅a ----→ ∧ ′ 0 a1⋅⋅⋅a ----→ ′ } (16)
is a monotone simulation between and ( ). Indeed, Proof sketch. We reduce from the VAS model-checking problem for CTL(F, X a ), which is shown undecidable by Esparza (1997, Section 4.5) using a reduction from the VAS containment problem. Consider an instance ⟨ , ⟩ of the VAS model-checking problem for CTL(F, X a ); we an instance ⟨ ′ , Φ⟩ of the PrCTL ≥ (F) model-checking problem s.t.

|= ′ |= Φ. Indeed, let = ⟨V, x 0 ⟩ be a -VAS with V = {a 1 , . . . , a }, and define a ( + )-VAS ′ that simulates each transition a on the first coordinates and additionally increments coordinate + . We also define inductively a PrCTL ≥ (F) formula ( ) from the CTL(F, X a ) formula , by preserving EF modalities, and by translating relativized "next" subformulae EX a ′ with a in V as EF a ( ′ ) where a ( 1 , . . . , ′ ) def = + = 1. Finally, we need to ensure that the considered partial cover is a partial unfolding of the reachability graph, i.e. that we do not allow -values, by defining

Φ def = ( ) ∧ AG ( ⋀ + =1 ( ) < ) .
A.3 Proof of Proposition 3.2

Lemma A.3. If 1 ≼ 2 and is a PrECTL ≥ (U) formula, then 1 |= implies 2 |= .
Proof. By definition of 1 ≼ 2 , there exists a covering simulation ⊆ 1 × 2 . First note that the following claim holds by induction on thanks to Definition 2.3.2b:

Claim A.3.1. If ′ and = 0 a1 -→ 1 a2 -→ ⋅ ⋅ ⋅ is a path in Paths( ), then there exists a path ′ = ′ 0 a1 -→ ′ 1 a2 -→ ⋅ ⋅ ⋅ in Paths( ′ ) s.t.
′ for all and

| ′ | ≥ | |.
For the main proof, let us prove by induction on that for any ′ , |= implies ′ |= , which will yield the lemma by Definition 2.3.1.

For ⊤ and ⊥ |= ⊤ and ′ |= ⊤, ∕ |= ⊥ and ′ ∕ |= ⊥. For a coverability constraint if |= ( ) ≥ , then since ℓ 2 ( ′ ) ≥ ℓ 1 ( ) ≥ by Definition 2.3.2a, ′ |= ( ) ≥ .
For ∨ ′ or ∧ ′ the result holds by ind. hyp.

For E( U Corollary A.4. Let = ⟨V, x 0 ⟩ be a -VAS and a -formula of PrECTL ≥ (U, X).

′ ) if |= E( U ′ ), i.e. if
Then Proof. The decision procedure is an extension of the classical dynamic algorithm for CTL that computes the satisfaction set ′ for every subformula ′ of : for a PrCTL ≥ formula ′ , ′ def = { ∈ | |= ′ }. We show that these satisfaction sets can be computed in a finite LTS, and the decision problem then reduces to checking whether init ∈ . Write V = {a ∈ ℤ | ∃ , ′ ∈ , a -→ ′ }; V is a finite set {a 1 , . . . , a } since is finite. Let us first prove the following: Claim A.5.1. Let , ⊆ and be a QFP formula with free variables. Then Pre , ( )

def = { 0 ∈ | ∃ ′ ∈ , ∃ ≥ 0, ∃a 1 , . . . , a ∈ ℤ , 0 a1 -→ 1 ⋅ ⋅ ⋅ -1 a --→ ′ ∧ PA |= (Δa 1 ⋅ ⋅ ⋅ a ) ∧ ∀ < , ∈ } is effectively computable.
The claim is an easy consequence of Parikh's Theorem: for every 0 in , we define the finite automaton = ⟨ ∪ , V, , { 0 }, ⟩ with 0 as unique initial state, = → ∩ ( × V × ( ∪ )) as set of transitions, and as set of final states. Accepting runs

0 a1 -→ 1 ⋅ ⋅ ⋅ -1 a --→ ′ in verify ′ ∈
and ∀ < , ∈ . The language ( ) has a semilinear Parikh image, which can be described by an existential Presburger formula Ψ( 1 , . . . , ) verifying PA |= Ψ(y) for a vector y in ℕ iff there exists an accepting run 0 a1⋅⋅⋅a ----→ ′ in with a occurring exactly y( ) times in the string a 1 ⋅ ⋅ ⋅ a for every 1 ≤ ≤ -see [START_REF] Verma | On the complexity of equational Horn clauses[END_REF] for a polynomial-time construction of Ψ from . Thus a state 0 belongs to Pre , ( ) iff

PA |= ∃ 1 , . . . , ∃ , ⋀ =1 ≥ 0∧Ψ( 1 , . . . , )∧ ( ∑ =1 a (1) ⋅ , . . . , ∑ =1 a ( ) ⋅ )
iii which is decidable in NPTime since this is an existential formula of Presburger Arithmetic.

Returning to the main proof, we merely need to define by induction on :

⊤ def = ¬ def = ∖ ∨ ′ def = ∪ ′ E( U ′ ) def = Pre , ( ′ ) ( ) ≥ def = { ∈ | ℓ( )( ) ≥ } .
As a direct consequence of Corollary A.4, of the finiteness of the canonical coverability graph, and of Lemma A.5, we conclude:

A.4 Proof of Proposition 4.1

Proposition A.7. The satisfiability problem for PrECTL ≥ (F) is decidable in NPTime.

Proof sketch. Let be a -formula of PrECTL ≥ (F). Let V be the positive and negative canonical base: V = {e , -e | 1 ≤ ≤ } where e is the unit vector with e ( ) = 1 and e ( ) = 0 if ∕ = . For any x 0 in ℕ , ⟨V, x 0 ⟩ is a -VAS. Introducing an value in coordinate in order to satisfy a ( ) ≥ constraint is always possible by firing e and -e in sequence. Finite coverability constraints of form ( ) ≥ are satisfiable by choosing a high enough x 0 . Thus coverability constraints are always satisfiable. Finally, satisfying QFP constraints on paths for EF modalities is done by finding a solution to in NPTime, and if there exists one, playing the corresponding sequence of transitions. To sum up, is satisfiable iff all its Presburger formulae are satisfiable.

A.5 Proof of Proposition 4.2

Proposition A.8. Let be a -formula of PrECTL ≥ (F). Whether is a -formula of iPrECTL ≥ (F) is decidable in NPTime.

Proof. Let be a -formula of PrECTL ≥ (F). We are going to compile the constraints on any tree-shaped model of into Presburger arithmetic.

Consider a modal subformula EF ′ and a tree-shaped submodel with -→ ′ s.t. ′ |= ′ and PA |= (Δ ) (and thus |= EF ′ ). We associate -tuples of variables ¯ = ⟨¯ (1), . . . , ¯ ( )⟩, ¯ = ⟨¯ (1), . . . , ¯ ( )⟩, and Ω = ⟨ Ω(1), . . . , Ω( )⟩ to each such modal subformula of representing the reached label ℓ( ′ ), the effect of the last followed sequence of transitions Δ , and the set of coordinates holding an value {1 ≤ ≤ | ℓ( )( ) = } (represented by integers with the "C semantics" that value "1" stands for true and any other value for false), along with a -tuple of variables ¯ 0 representing the initial (root) marking ℓ( 0 ). iv We inductively define an existential Presburger formula (¯ 0 , ¯ , Ω, ′ ) for each subformula ′ of , carrying information about the root marking (¯ 0 ) and the previous marking (¯ and Ω): 22)

(¯ 0 , ¯ , Ω, ⊤) def = ⊤ (17) (¯ 0 , ¯ , Ω, ⊥) def = ⊥ (18) (¯ 0 , ¯ , Ω, 1 ∨ 2 ) def = (¯ 0 , ¯ , Ω, 1 ) ∨ (¯ 0 , ¯ , Ω, 2 ) (19) (¯ 0 , ¯ , Ω, 2 ∧ 2 ) def = (¯ 0 , ¯ , Ω, 1 ) ∧ (¯ 0 , ¯ , Ω, 2 ) (20) (¯ 0 , ¯ , Ω, ( ) ≥ ) def = { Ω( ) = 1 if = ⊤ otherwise (21) (¯ 0 , ¯ , Ω, ′ = EF ′′ ) def = { ∃¯ ′ Ω′ . ( Ω, Ω′ ) ∧ ′ (¯ 0 , ¯ , ¯ ′ , Ω′ , ′ ) if ′′ is a CC (13) ∃¯ ′ Ω′ . ( Ω, Ω′ ) ∧ ′′ (¯ 0 , ¯ , ¯ ′ , Ω′ , ′ ) otherwise (
′ (¯ 0 , ¯ , ¯ ′ , Ω, ′ ) def = (∃ .1 ≤ ∧ ≤ ∧ Ω( ) ∕ = 1 ∧ ¯ ′ ( ) < ¯ 0 ( )) ∧ ′′ (¯ 0 , ¯ , Ω, ′ ) (23) ′′ (¯ 0 , ¯ , ¯ ′ , Ω, ′ = EF ′′ ) def = ∃¯ . (¯ 0 , ¯ ′ , Ω′ , ′′ ) ∧ (¯ ) ∧ ⎛ ⎝ ⋀ 1≤ ≤ Ω( ) ∕ = 1 =⇒ ¯ ( ) = ¯ ′ ( ) -¯ ( ) ⎞ ⎠ (24)
( Ω, Ω′ )

def = ⋀ =1 Ω( ) = 1 =⇒ Ω′ ( ) . ( 25
)
Hence for each ′ = EF ′′ modal subformula, we guess the reached marking (the ¯ ′ and Ω′ variables in ( 22)) and the effect of the last sequence of transitions Δ (the ¯ variables in ( 24)). The latter is checked against in (24). However some of the ¯ variables might be left unrelated to the actual effect of (which is ¯ ′ -¯ ) if the coordinate at hand contains an -value, i.e. if Ω( ) = 1. Equation ( 21) checks the consistency of the set of -values guessed in ( 22) with coverability constraints, while (25) ensures that -values are propagated in the model. When we reach a leaf, i.e. when we consider a formula EF with a CC, we check with (23) whether the formula has decreased on this branch, that is to say, whether there is a place on which no value was introduced and the current marking ¯ is not greater the that of the root ¯ 0 : thus the constructed Presburger formula checks the existence of a counter-example to the fact that is increasing. Consider the same set of vectors V as in the proof Proposition 4.1; given an appropriate x 0 this set can satisfy any . Let

Ψ def = ∃¯ 0 . (¯ 0 , ¯ 0 , (0) 1≤ ≤ , ) ; (26)
Ψ is an existential Presburger formula which is satisfiable iff we can build aadmissible partial cover of the -VAS ⟨V, x 0 ⟩ (for an appropriate x 0 ) satisfying but not increasing. We have thus reduced the question of increasingness to existential Presburger satisfaction formula; as Ψ can be constructed in polynomial time, the problem can thus be solved in NPTime.

v

A.6 Proof of Lemma 4.3

We prove Lemma 4.3 with refined parameters for the size of formulae:

Formula Size. We consider several parameters on the size of PrECTL ≥ (F) formulae : its disjunctive size | | ∨ , corresponding to its modal size when maximizing over disjunctions, defined inductively by

|⊤| ∨ def = |⊥| ∨ def = | ( ) ≥ | ∨ def = 0 |EF | ∨ def = 1 + | | ∨ | ∨ ′ | ∨ def = max(| | ∨ , | ′ | ∨ ) | ∧ ′ | ∨ def = | | ∨ + | ′ | ∨
its conjunctive size | | ∧ measuring the maximal number of leaves in a treeshaped model and defined inductively by

|⊤| ∧ def = |⊥| ∧ def = | ( ) ≥ | ∧ def = 0 |EF | ∧ def = { 1 if is a CC (13) 0 otherwise | ∨ ′ | ∧ def = max(| | ∧ , | ′ | ∧ ) | ∧ ′ | ∧ def = | | ∧ + | ′ | ∧ (note that | | ∨ ≥ | | ∧ for any formula ), its maximal constant size ∥ ∥ def = ∥{ ∈ ℕ | ∃ , ( ( ) ≥ ) ∈ sub( )}∥
and two measures related to the QFP formulae appearing in EF modalities: the Presburger constant size Pr ( ) defined as the log of the maximal constant (i.e. size of a subterm according to [START_REF] Axelsson | Extended computation tree logic[END_REF]) appearing in any QFP formula, and the Presburger constraint size Pr ( ) defined as the total number of Presburger constraints (i.e. of subterms according to ( 7)) appearing in . For instance, with formulae (8)-( 11 Lemma A.9 (Small Models for Bounded LTS). Let ⟨V, x 0 ⟩ be a generalized -VAS with > 1, be a PrECTL ≥ (F) formula, and 0 ≤ ≤ and ≥ 0. If there exists an ( , )-bounded partial cover of ⟨V, x 0 ⟩ s.t. |= | , then there exists a tree-shaped ( , )-bounded partial cover ′ of ⟨V,

x 0 ⟩ with ′ |= | and | ′ | ≤ (2 ∥V∥+Pr ( ) | | ∨ ) ( +| | ∧ +Pr ( ))
for some constant (independent of V, x 0 , , , , and ).

Proof. As in (Rackoff, 1978, Lemma 4.5) we identify and remove loops (called -loops) in (an unfolding of) before reintroducing them in a controlled manner in order to maintain both the satisfaction of Presburger formulae on paths and the existence of some -antecedent for every introduced -value. These two points are specific to our problem.

To this end, we decompose the unfolding of into a tree of individual segments where no values are introduced. Figure 2 illustrates this decomposition on a partial cover of the VAS of Figure 1 which models the non-regularity formula (11). The model is decomposed into three segments 1 , 2 , and 3 , along with Presburger constraints inherited from EF modalities (dashed above) and -antecedency relations (dashed below). We find and remove -loops in each segment individually. Both -antecedency relations and the Presburger formulae in modalities are used as Presburger constraints on the number of times each -loop should appear. The bounds of [START_REF] Papadimitriou | On the complexity of integer programming[END_REF] on the size of solutions for linear constraints result in a small number of -loops having to be reintroduced in order to yield ′ . Details follow. vi

⟨1, 0, 1⟩ ⟨2, 1, 0⟩ ⟨2, 0, 0⟩ ⟨1, 0, 1⟩ ⟨0, 0, 2⟩ ⟨1, , 1⟩ ⟨1, , 1⟩ a c b b a c ⊤ 1 ≥ 0 ∧ 2 > 0 ∧ 3 ≥ 0 1 ≥ 0 ∧ 2 < 0 ∧ 3 ≥ 0 1 2 3
Figure 2: Decomposition of a model for (11).

Decomposition by EF Formulae. The PrECTL ≥ (F) fragment clearly enjoys a finite tree model property, in the sense that any -admissible partial cover that models a PrECTL ≥ (F) formula can be "unfolded" into a tree-shaped one.

Formally, since

EF ( ∨ ′ ) ≡ (EF ) ∨ (EF ′ ) , (27)
we can put any PrECTL ≥ (F) formula into disjunctive normal form, by pulling all disjunctions to the front, i.e. ≡ ⋁ where each is disjunction-free. Then by definition |= iff there exists s.t. |= , thus we can restrict our attention to disjunction-free formulae. The unfolding then consists roughly in associating subterms of with states of and choosing intermediate states for paths verifying EF ′ formulae. The latter formulae decompose

′ into ≤ | | ∨ segments -→ ′ in where |= EF ′ thanks to PA |= (Δ ) and ′ |= ′ .
Example A.10. Consider the CCG given in Figure 1 and formula unreg given in (11). We have

unreg ≡ ⋁ ⊆ {1, . . . , } ∕ = ∅ ⋁ ⊆ ⊆{1,..., } EF ⎛ ⎝ ⋀ ∈ ( ) ≥ ∧ EF , ⊤ ⎞ ⎠ (28)
and we can select a subformula satisfied by (with = = {2}):

′ unreg def = EF ( (2) ≥ ∧ EF 1 ≥0∧ 2 <0∧ 3 ≥0 ⊤) . (29)
In turn, we can unfold into the partial cover displayed in Figure 2. The decomposition of this model by EF subformulae results in the two segments displayed on top with their respective Presburger constraints.

Decomposition by Antecedents. First observe that there are

≤ | | ∧ (30)
pairs ( , a) with a -antecedent ′ in the unfolding of , because once introduced an -value cannot disappear. All in all, this unfolding is split into No -value is introduced within a segment before its last transition.

def = 2 + | | ∨ ≤ 2 | | ∧ + | | ∨ ≤ (2 + 1)| | ∨ (31)
Let ′ -→ a -→ ′′ be the path witnessing that ′ is a -antecedent of ( , a). We capture this relationship with a QFP formula z defined for any z in ℕ and ≤ by z ( 1 , . . . ,

) def = > 0 ∧ ⋀ 1 ≤ ≤ z( ) < ≥ 0 . (32)
Indeed, PA |= ℓ( ′′ ) (Δ ⋅ a) is then a characterization of -antecedency. Note that the sequence ⋅ a might span over several consecutive segments for 1 ≤ ≤ .

Example A.11. Continuing with the example of Figure 2, an -value is introduced in the 6th state with the 1st and 4th states as possible 2-antecedents, where 2 ⟨0,0,2⟩ ( 1 , 2 , 3

) def = ( 1 ≥ 0 ∧ 2 > 0 ∧ 3 ≥ 0)
, and in each case with PA |= 2 ⟨0,0,2⟩ (Δacbba) = 2 ⟨0,0,2⟩ (Δba) = 2 ⟨0,0,2⟩ (⟨0, 1, 0⟩). Choosing arbitrarily the 4th state as antecedent, we obtain a decomposition into three segments 1 , 2 , and 3 .

The constraints on the segments are then

• PA |= ⊤(Δacbba) (corresponding to the constraint on top of the 1 2 segment),

• PA |= 2 ⟨0,0,2⟩ (Δba) (corresponding to the constraint below the 2 segment), and

• PA |= {2} (Δc) (corresponding to the constraint above the 3 segment, where {2} ( 1 , 2 , 3 ) is defined in (12) as 1 ≥ 0 ∧ 2 < 0 ∧ 3 ≥ 0).
-Loops Removal. Next, let be the transition label in (ℤ ) * of each segment , 1 ≤ ≤ . We apply the decomposition technique of (Rackoff, 1978, Lemma 4.5) to each : call a factor of an -loop if Δ ( ) = 0 for each 1 ≤ ≤ and Δ ′ ( ) ∕ = 0 for some 1 ≤ ≤ for any proper factor ′ of , i.e. no proper factor of is an -loop. Considering again the example of Figure 2, the sequence acb between the 1st and 4th states is both a 3-loop and a 2-loop, but not a 1-loop because the factor c between the 2nd and 3rd states is a 1-loop.

Rackoff's technique decomposes into a path ′ and a number of -loops

( ) in (ℤ ) * s.t. | ′ | ≤ ( + 1) 2 and Δ = Δ ′ + ∑ ⋅ Δ (33)
for some constants ( ) each corresponding to the number of times theloop is removed. In addition, the set of projections on the first places of vectors along ′ is the same as that of , which garantees that -loops can be reintroduced freely. viii Each -loop obtained this way has length at most ≤ , thus each coordinate Δ ( ) has absolute value at most max def = 2 ∥V∥ , thus there are at most def = (2(2 ∥V∥ ) + 1) -loops with different effects. Identifying -loops having the same effect, we see that (33) only needs different , while the effect Δ ′ is of absolute value at most max def = 2 ∥V∥ ( +1) 2 on every coordinate.

Reintroducing -Loops. In order to obtain a partial cover ′ that models , we merely need to ensure that both the -antecedent relations and the Presburger constraints on paths are preserved. Indeed, finite values on the first coordinates are preserved by -loop removal, thus the only difficulty is to ensure that -values and Presburger constraints are also preserved, so that we obtain a partial cover and preserve constraints of form ( ) ≥ .

We reintroduce -loops: each of the -antecedency constraints translates into verifying a Presburger constraint PA |= ℓ( ′′ ) ( ∑ ∈ Δ ) and each of the | | ∨ modal subterms EF ′ into a Presburger constraint PA |= ( ∑ ∈ Δ ), each time for some set of consecutive indices corresponding to the span of the -antecedent relation or path verifying , and we need to enforce the conjunction of all these + | | ∨ constraints. Therefore, we obtain a system of linear constraints in

def = ( + | | ∨ ) ⋅ + Pr ( ) (34) ≤ ( | | ∧ + | | ∨ ) ⋅ + Pr ( ) ≤ ( + 1)| | ∨ ⋅ + Pr ( ) = ( + 1)| | ∨ (2(2 ∥V∥ ) + 1) + Pr ( )
integer variables (telling how many times each -loop should be reintroduced)the Pr ( ) term is needed to account for divisibility relations ≡ ′ in QFP formulae-and

def = ⋅ + Pr ( ) ≤ 2 | | ∧ + Pr ( ) (35)
constraints, with variable coefficients ≤ max ⋅ 2 Pr ( ) in absolute value, and constant coefficients ≤ ⋅ max +2 Pr ( ) ≤ (2 +1)| | ∨ max +2 Pr ( ) in absolute value. By the results of [START_REF] Papadimitriou | On the complexity of integer programming[END_REF] (see also [START_REF] Seshia | Deciding quantifier-free Presburger formulas using parametrized solution bounds[END_REF], Theorem 2)), we deduce a bound of

( + 1 + )(1 + (2 + 1)| | ∨ max + 2 Pr ( ) )( ( max + 2 Pr ( ) )) 2 +3 ≤ (2 ∥V∥+Pr ( ) | | ∨ ) ( +| | ∧ +Pr ( )) (36)
for some constant on the solutions of this system, i.e. on the number of times each -loop should be repeated. Multiplying (36) by the maximal length of an -loop and adding the sum ( + 1) 2 of the lengths of the ′ segments, we end up with a bound of (2 ∥V∥+Pr ( ) | | ∨ ) ( +| | ∧ +Pr ( )) for some constant on the length of the new partial cover ′ . ix A.7 Proof of Lemma 4.4

We prove Lemma 4.4 for a refined version of that takes formula size into account. Given V ⊆ (ℤ ) , a -coverability formula , and some 0 ≤ < , let (0

) def = (2 ∥V∥+Pr ( ) ⋅ |V| ⋅ | | ∨ ) ( +| | ∧ +Pr ( )) ( + 1) def = ( 2 ∥V∥+Pr ( ) ⋅ (2 ∥V∥ ( ) + 2 ∥ ∥ ) ⋅ | | ∨ ) ( +| | ∧ +Pr ( )) + 1 + ( )
where is the constant of Lemma 4.3.

Lemma A.12. Let ⟨V, x 0 ⟩ be a -VAS and = EF ′ be an eventually increasing -formula. Let be an -admissible partial cover of ⟨V, x 0 ⟩ with |= | . Then there exists a tree-shaped -admissible partial cover ′ of ⟨V,

x 0 ⟩ s.t. ′ |= | and | ′ | ≤ ( ).
Proof. The proof follows in part (Rackoff, 1978, Lemma 4.6 & 4.7) and is by induction on .

variables with coefficients at most max def = 2 ∥V∥+Pr ( ) in absolute value and constants at most max def = 2 Pr ( ) , thus by [START_REF] Papadimitriou | On the complexity of integer programming[END_REF] we can construct a model ′ of size at most

( +1+ )(1+ max )( max ) 2 +3 ≤ (2 ∥V∥+Pr ( ) ⋅|V|⋅| | ∨ ) ( +| | ∧ +Pr ( )) = (0)
for the constant of Lemma 4.3.

Induction

Step for + 1. Let | +1 = EF ′ with ′ an increasing formula. We assume wlog. to be tree-shaped, with an initial path of form init → * 0 s.t.

0 |= ′ . Set def = 2 ∥V∥ ( ) + 2 ∥ ∥ , (38)
which a high enough value to ensure any model of size ( ) will be unable to decrease a coordinate holding below the maximal finite constant appearing in a ( ) ≥ subformula of | +1 . Two cases arise:

If is ( + 1, )-bounded then by Lemma 4.3 it is of length at most (2 ∥V∥+Pr ( ) | | ∨ ) ( +| | ∧ +Pr ( )) = ( + 1) .
Otherwise there exists some state ′ in with ≤ ℓ( ′ )( ) < for some ; wlog. we assume this to occur only in = + 1.

x Consider the leaves 1 , . . . , of . Since ′ is increasing, ℓ( ) ≥ ℓ( ) for all 1 ≤ ≤ . By monotonicity, this means that we can "replay" the entire submodel rooted in 0 from any of the leaves 1 , . . . , , i.e. fire the same sequences of transitions and introduce (if necessary) -values at the same points. By performing this operation sequentially on 1 , then on 1 2 (the leaf corresponding to 2 in the replay started in 1 ), then on 2 3 (the leaf corresponding to 1 3 in the replay from 1 2 , where 1 3 is the leaf corresponding to 3 in the replay from 1 ), . . . , we end with a copy of the submodel rooted at -1 s.

t. -1 |= ′ , and init → * 0 → * 1 → * 1 2 → * 2 3 → * ⋅ ⋅ ⋅ -1 , i.e.
we have constructed a model 1 of | +1 , which is also an ( + 1)-admissible partial cover of ⟨V, x 0 ⟩.

There are two immediate but crucial properties of 1 :

1. there exists now a first state ′ with ≤ ℓ( ′ )( ) < reachable from init , and it appears somewhere in the segment init → * -1 ; 2. any -value that appeared in any of the leaves 1 , . . . , is now introduced during the prefix init → * -1 and its -antecedency relation also points inside this prefix.

Because of these two properties, we can identify -antecedency relations that "cross" the ′ boundary inside the init → * -1 prefix. By monotonicity, we can also "replay" the pumping segment (called a in (1)) and introduce the -value on the second instance only; doing so for all theantecedency relations that span over ′ (in their order of appearance after ′ ) allows to split the prefix init → * -1 into two segments init → * ′ and ′ → * -1 with no -antecedency relations crossing over ′ . Call 2 this new model of | +1 .

We now treat the prefix init → * ′ and the suffix ′ → * -1 with the submodel rooted at -1 separately:

• the prefix init → * ′ can in turn be split into init → * a -→ ′ with a in V and the last state with ℓ( )( ) < or ℓ( ) = for all 1 ≤ ≤ + 1. The segment init → * is ( + 1, )-bounded and verifies the ( + 1)-formula

′′ def = EF +1 ⋀ =1 ( ( ) ≥ ℓ( )( )) ∧ ⋀ |ℓ( )( )= ( ( ) ≥ ) . (39)
By Lemma 4.3 we can replace init → * by another prefix also verifying ′′ of size at most (2 ∥V∥ ) (40)

By monotonicity, continuing this model of ′′ with a and the suffix we obtain a model of | +1 .

• the suffix ′ → * -1 along with the submodel rooted at -1 is in particular an -admissible model of | for the generalized -VAS ⟨V, ℓ( )⟩. By induction hypothesis we can replace it with a model of size ( ). Since ℓ( )( + 1) ≥ , this new model is also ( + 1)admissible and models +1 , as no value on the ( + 1)th coordinate can drop below the largest constant in .

xi All in all, we have constructed a model ′ of size at most

(2 ∥V∥ ) + 1 + ( ) = ( 2 ∥V∥ (2 ∥V∥ ( ) + 2 ∥ ∥ ) ) ≤ ( + 1) .
A.8 Proof of Theorem 4.5

Theorem A.13 (Complexity of VAS model checking). The VAS model-checking problem for eiPrECTL ≥ (F) formulae is ExpSpace-complete.

Proof. The hardness result already holds for place coverability and is due to Lipton [START_REF] Cardoza | Exponential space complete problems for Petri nets and commutative semigroups[END_REF]. We only need to prove the upper bounds. Thanks to Lemma 4.4, we know that if a coverability formula has a model, then it has one of size is bounded by

( ) ≤ (2 ∥V∥+∥ ∥+Pr ( ) |V|| | ∨ ) 2 ′ log 2 ( +| | ∧ +Pr ( )) (41)
for some constant ′ independent of V and . We use a non-deterministic algorithm, that guesses and checks a witness on the fly up to length ( ) in space ((∥V∥ + ∥ ∥ + Pr ( )

+ log 2 |V| + log 2 | | ∨ ) ⋅ ( + | | ∧ + Pr ( )) ⋅ 2
′ ), which is polynomial for fixed and exponential otherwise. Note that the size of the formula only influences this bound polynomially.

B Additional Comments

B.1 Extensions of PrECTL ≥ (U)

We consider in this section the PrECTL ≥ (G) fragment, and a variant of PrECTL ≥ (U) with "until" refined by two QFP formulae.

"Globally" Modalities. We use the natural semantics of G as a dual modality of F:

|= EG iff ∃ = 0 a1 -→ 1 a2 -→ ⋅ ⋅ ⋅ ∈ Paths( ), ∀ ≤ | |, PA |= (Δa 1 ⋅ ⋅ ⋅ a ) implies |= .
This EG modality is not very useful with our partial cover semantics, because we have no control on the length of paths (it often suffices to "cut" a branch in order to satisfy a EG modality). However, if we look at satisfaction on a particular partial cover, things change:

Proposition B.1 (Undecidability of CCG Model-Checking). Let = ⟨V, x 0 ⟩ be a -VAS and a -formula of PrECTL ≥ (G). It is undecidable whether ( ) |= . Proof sketch. We reduce an instance ⟨ℳ⟩ of the halting problem in 2-counter deterministic Minsky machines to an instance ⟨ , ⟩ of the CCG model-checking problem. The construction of is classical, using nondeterminism to simulate " : if = 0 then goto ′ else ← -1; goto ′′ " instructions. This VAS allows many incorrect runs in addition to a single honest run that corresponds to the xii unique run of ℳ. The task of is thus to filter out dishonest runs in ( ) and only leave the honest one, and also to test whether the honest run halts. Let def = EG ¬honest∨halt ⊥ .

(42)

A run = 0 a1 -→ 1 a2 -→ ⋅ ⋅ ⋅ satisfying has to continuously ensure that PA ∕ |= ¬honest∨halt (Δa 1 ⋅ ⋅ ⋅ a ). As should be clear from its name, ¬honest∨halt holds if the run is dishonest or halts, so that ( ) |= iff ℳ does not halt.

Assuming to be a (2| | + 2)-VAS coding the states of ℳ in its first 2| | coordinates and the two counters in the last two coordinates, and coordinate ∈ to denote that an "if branch" has just been chosen (which should imply that the counter holds zero), this can be checked by defining Observe that this proof does not hold if we consider any -admissible partial cover instead of the CCG: the cover could simply stop in the initial state and verify even if ℳ did halt. (43)

We leave the definition of ¬honest and halt to the reader's imagination, and conclude with the fact that |= iff ℳ halts.

xiii

B.2 More Coverability-Like Properties

We present in this section a few more properties of vector addition systems testable in ExpSpace. We already gave eiPrECTL ≥ (F) formulae for coverability, boundedness, place boundedness, and regularity in ( 8)-( 11). We found more examples considered by Yen (1992, Section 4), [START_REF] Atig | On Yen's path logic for Petri nets[END_REF]Habermehl (2009, Section 6.1), andDemri (2010, Section 3.3).

1. Nondeterminism is a variant of coverability and asks whether two different transitions a and a ′ can be fired simultaneously. Define the vector of ℕ x a by x a ( ) = -a( ) if a( ) < 0 and x a ( ) = 0 otherwise, and take the (pointwise) least upper bound x a ⊔ x a ′ : nondeterminism reduces to coverability of x a ⊔ x a ′ for some a ∕ = a ′ :

nondet def = EF ⋁ a∕ =a ′ ∈V ⋀ =1 ( ) ≥ (x a ⊔ x a ′ )( ) . (44)
2. Repeated control-state reachability [START_REF] Habermehl | On the complexity of the linear-time -calculus for Petri nets[END_REF]) is used to modelcheck -regular properties. Using an encoding of the set of states using ⌈log 2 ⌉ additional counters and an extra counter at index incremented with every transition, this property is a form of repeated coverability for some vector x, and captured by

Indeed, if there exists an infinite run in ( ) where x is covered infinitely often, we can consider the infinite sequence x 0 , x 1 , . . . of configurations ≥ x in this run; by Dickson's Lemma there exists two indices 1 < 2 in this sequence s.t. x 1 ≤ x 2 thus the corresponding factor between 1 and 2 in the run verifies the rep-cov condition. Conversely, if rep-cov,x holds, then there exists a run covering x infinitely often by monotonicity.

3. Simultaneous unboundedness [START_REF] Demri | On selective unboundedness of VASS[END_REF] tests whether a subset of {1, . . . , } can be simultaneously unbounded. This is very simply captured by

It checks for the existence of two loops in the coverability graph, starting with two different initial transitions on a and b (see (Chambart et al., 2011, Proposition 4)).

Demri also shows that there is a LogSpace reduction of the strong promptness detection problem to the complement of the simultaneous unboundedness problem (Demri, 2010, Lemma 3.4); in the same way, reversal-boundedness [START_REF] Finkel | Reversal-bounded counter machines revisited[END_REF]

Figure 1 :

 1 Figure 1: The canonical coverability graph for the VAS = ⟨{a, b, c}, ⟨1, 0, 1⟩⟩ with transitions a = ⟨1, 1, -1⟩, b = ⟨-1, 0, 1⟩, and c = ⟨0, -1, 0⟩.

=

  ¬⊤, ∧ ′ def = ¬((¬ ) ∨ (¬ ′ )), ( ( ) < ) def = ¬( ( ) ≥ ), and AG def = ¬EF ¬ . Semantics of PrCTL ≥ (U). The models of PrCTL ≥ (U) formulae are labeled transition systems ⟨ , →, ℓ, init ⟩. Given a state in , write Paths( ) for the set of maximal paths = 0 a1 -→ 1 a2 -→ ⋅ ⋅ ⋅ starting in = 0 and where each a is in ℤ and each in . The path is either infinite with length | | = , or finite of form = 0 a1 -→ ⋅ ⋅ ⋅ a -→ if has no successor and then |

  because ( ) is deterministic, given a 1 ⋅ ⋅ ⋅ a there is no choice for ′ , which verifies ℓ( ) ≤ ℓ ′ ( ′ ) by the previous claim, thus fulfills Definition 2.3.2a, and (b) if furthermore a +1 ---→ +1 , then by the claim there exists ′ 2. The VAS model-checking problem for PrCTL ≥ (F) is undecidable.

  in Paths( ) and an index ≤ | |, s.t. PA |= (Δa 1 ⋅ ⋅ ⋅ a ), |= ′ , and for all 0 ≤ < , |= , then by the claim, there exists a path ′ ⋅ ⋅ in Paths( ′ ) s.t. ′ for all and | ′ | ≥ | |. In particular for = ≤ | | ≤ | ′ |, by ind. hyp. ′ |= ′ , and for all 0 ≤ = < , by ind. hyp. ′ |= . All in all, ′ |= E( U ′ ).

Proposition A. 6 .

 6 The VAS model-checking problem for PrECTL ≥ (U) is decidable in nondeterministic polynomial time in | ( )| and | |.

  ), | | ∨ ≤ 2, | | ∧ = 1, and Pr ( ) ≤ .

  segments 1 , . . . , defined by various extremal points: vii 1. the ≤ | | ∨ + 1 states , ′ witnessing the satisfaction of EF ′ subformulae of , i.e. with |= EF ′ thanks to PA |= (Δ ) and ′ |= ′ , and 2. the ≤ 2 different states ′ and ′′ corresponding to -antecedency relations of form ′ -→ a -→ ′′ .

  Base Case = 0. The only requisite of |0 are Presburger constraints on paths and proper introduction of -values. As in the proof of Lemma 4.3, we decompose a model of |0 into segments, each labeled by some , 1 ≤ ≤ , with Δ = ∑ |V| =1 a for some ( ) where V = {a 1 , . . . , a |V| }. Theantecedent constraints and Presburger constraints result in linear constraints as in (35) over def = ( + | | ∨ ) ⋅ |V| + Pr ( ) ≤ ( + 1)| | ∨ |V| + Pr ( )

  branch" when ∕ = 0) ∨ 2 ≥ 1 .(halt state)

"

  Until" Modalities with Two Presburger Formulae. The semantics of EG lead rather naturally to an extension of PrCTL ≥ (U) where we also control what happens along the way of the "until":|= E( U , ′ ′ ) iff ∃ ⋅ ⋅ ∈ Paths( ), ∃ ≤ | |, PA |= ′ (Δa 1 ⋅ ⋅ ⋅ a ), |= ′ , and ∀ < , PA |= (Δa 1 ⋅ ⋅ ⋅ a ) implies |= .The "until" modality of the paper can then defined asE( U ′ ) def = E( U ⊤, ′). Let us call the resulting existential fragment PrECTL ≥ (U 2 ); it is easily seen to have an undecidable VAS model-checking problem:Proposition B.2. The VAS model-checking problem for PrECTL ≥ (U 2 ) is undecidable.Proof sketch. As in the proof sketch for Proposition B.1, we reduce from the halting problem of deterministic 2-counter Minsky machines. In fact we keep the same construction for the VAS and only slightly modify the formula: def = E(⊥ U ¬honest , halt ⊤) .

  Trace boundedness[START_REF] Chambart | Forward analysis and modelchecking for trace-bounded WSTS[END_REF] checks whether the language of a VAS is a bounded language according to[START_REF] Ginsburg | Bounded Algol-like languages[END_REF]'s definition. Trace unboundedness can be checked by a EF ,a ⊤) ∧ (EX b EF ,b ⊤) (48) xiv where EX a was defined in the proof of Proposition 3.1, and ,a is defined for all a in ℤ and ⊆ {1, . . . , } by ,a ( 1 , . . . , )

  reduces to place boundedness. It is worth noting that in all our examples the various parameters on formula sizes remained small: | | ∨ ≤ 5, | | ∧ ≤ 2, ∥ ∥ ≤ ∥V∥, Pr ( ) ≤ ∥V∥, and Pr ( ) ≤ .

  |= iff ( ) |= . Proof. First assume ∕ |= . By definition, this means that for any -admissible partial cover of , ∕ |= . Since ( ) is a -admissible partial cover of , ( ) ∕ |= . Conversely, assume |= . By definition, there exists a -admissible partial cover of s.t. |= . By Lemma 2.4, ≼ ( ), and by Lemma A.3, ( ) |= .

	By Corollary A.4, the VAS model-checking problem for PrECTL ≥ (U) re-
	duces to the model-checking problem on a particular, finite LTS. As expected,
	this is a decidable problem:
	Lemma A.5. Let	≥ 1,	= ⟨ , →, ℓ, init ⟩ be a finite LTS, and	a -
	formula of PrCTL

≥ (U). Then whether |= is decidable in nondeterministic polynomial time in | | and | |.

We include the divisibility relations, which are required for quantifier elimination, with semantics ≡ iff ∃ . + = for all , in ℤ and ≥


Frédéric Lavancier

Aggregation of isotropic autoregressive fields

Keywords: Long memory, aggregation, random fields, long range dependence

), JSPI, 139:2581-2597. The aggregation of isotropic four nearest neighbors autoregressive models on the lattice Z 2 , with random coefficient, is investigated. The spectral density of the resulting random field is studied in details for a large class of law of the AR coefficient. Depending on this law, the aggregated field may exhibit short memory or isotropic long memory.

Introduction

Contemporaneous aggregation of random parameter autoregressive processes is a well-known scheme to produce long memory in time series. This idea first appeared in [START_REF] Robinson | Statistical inference for a random coefficient autoregressive model[END_REF] and was more deeply investigated in [START_REF] Granger | Long memory relationships and the aggregation of dynamic models[END_REF]. A lot of papers have then been devoted to this subject, among them [START_REF] Gonçalvez | Agrégation de processus autorégressifs d'ordre 1. Annales d[END_REF], [START_REF] Oppenheim | Aggregation of random parameter Ornstein-Uhlenbeck or AR processes: some convergence results[END_REF], [START_REF] Zaffaroni | Contemporaneous aggregation of linear dynamic models in large economies[END_REF]. This construction of long memory is famous in econometrics, since it illustrated the fact that long memory may arise in macroeconomic time series, although micro-dynamics are short range dependent.

More recently, the concept of long memory has been extended to random fields on a lattice. In this setting, the intensity of long memory may depend on the direction or may be isotropic. We refer to [START_REF] Lavancier | Long memory random fields[END_REF] for a review. From a statistical point of view, the isotropic case is investigated in [START_REF] Anh | Parameter estimation of random fields with long-range dependence[END_REF], [START_REF] Frias | Semiparametric estimation of spatial long-range dependence[END_REF] and [START_REF] Wang | Memory parameter estimation for long range dependent random fields[END_REF]. Some anisotropic models are studied in [START_REF] Boissy | Parameter estimates for fractional autoregressive spatial processes[END_REF], [START_REF] Guo | Local whittle estimator for anisotropic random fields[END_REF] and [START_REF] Beran | On least squares estimation for long-memory lattice processes[END_REF]. A statistical test to detect long memory in random fields is provided in [START_REF] Lavancier | The V/S test of long-range dependence in random fields[END_REF].

As for time series, it seems natural to study the effect of aggregation in random fields, in particular the emergence of long memory. The aggregation in this case in not contemporaneous but is implemented at each point of the lattice. This scheme has been described in [START_REF] Lavancier | Long memory random fields[END_REF], where it is applied to produce some anisotropic models of long memory. In [START_REF] Azomahou | Memory properties and aggregation of spatial autoregressive models[END_REF], aggregation of isotropic four nearest neighbors autoregressive models on the lattice Z 2 is studied. These autoregressive models are very natural models on Z 2 and their introduction dates back to [START_REF] Whittle | On stationary processes in the plane[END_REF]. Their aggregation is expected to produce isotropic long memory in some cases, as announced in [START_REF] Azomahou | Memory properties and aggregation of spatial autoregressive models[END_REF]. Unfortunately, this article contains false results and the emergence of isotropic long memory by aggregation is not clearly described.

The present note is a corrigendum to the article of [START_REF] Azomahou | Memory properties and aggregation of spatial autoregressive models[END_REF]. In section 2, the general scheme of aggregation for random fields on Z 2 is recalled. In section 3, the aggregation of isotropic four nearest neighbors autoregressive models is considered. First, we recall the necessary and sufficient conditions for existence of a stationary solution to such autoregressive equations, which are known since [START_REF] Whittle | On stationary processes in the plane[END_REF] (see e.g. [START_REF] Guyon | Random Fields on a Network[END_REF]), but are improperly stated in Lemma 1 in [START_REF] Azomahou | Memory properties and aggregation of spatial autoregressive models[END_REF]. Then, the existence of a stationary aggregated field in L 2 is studied. Under some general conditions on the law of the autoregressive parameter, this existence is ensured in Theorem 1. The behavior of the spectral density of the induced field is also presented. The memory properties of the aggregated field are then deduced. These results are a corrected version of Propositions 2 and 3 in [START_REF] Azomahou | Memory properties and aggregation of spatial autoregressive models[END_REF].

Aggregating autoregressive random fields with random coefficients

The definition of an autoregressive field in Z 2 is very similar to the definition of an autoregressive time series (see [START_REF] Brockwell | Time Series: Theory and Methods[END_REF]) and appears in [START_REF] Whittle | On stationary processes in the plane[END_REF]. Basic results are presented in [START_REF] Rosenblatt | Stationary sequences and random fields[END_REF] and [START_REF] Guyon | Random Fields on a Network[END_REF].

Let L 1 (resp. L 2 ) be the lag operator acting on the first (resp. second) index of the field

(X i,j ) (i,j)∈Z 2 , i.e. L 1 X i,j = X i-1,j and L 2 X i,j = X i,j-1 .
The field (X i,j ) (i,j)∈Z 2 is an autoregressive field if there exists a white noise (ε i,j ) (i,j)∈Z 2 in L 2 and a complex function

P (z 1 , z 2 ) = (k,l)∈S a k,l z k 1 z l 2 ,
where S is a finite subset of Z 2 and (a k,l ) (k,l)∈S are real coefficients, such that for all (i, j) ∈ Z 2

P (L 1 , L 2 )X i,j = ε i,j .
(2.1)

It is well known that such an equation admits a stationary solution if and only if P (e iθ1 , e iθ2 ) = 0 for all (θ 1 , θ 2 ) (see [START_REF] Whittle | On stationary processes in the plane[END_REF], [START_REF] Rosenblatt | Stationary sequences and random fields[END_REF] or [START_REF] Guyon | Random Fields on a Network[END_REF]). In this case, the field (X i,j ) (i,j)∈Z 2 may be written

X i,j = (k,l)∈Z 2 c k,l ε i-k,j-l (2.2)
where (c k,l ) are the coefficients involved in the Laurent expansion of

P -1 (z 1 , z 2 ) in the neighbor- hood of {|z 1 | = 1, |z 2 | = 1} and satisfy |c k,l | < ∞.
Note that the series in (2.2) converges almost surely and in L 2 (see [START_REF] Brockwell | Time Series: Theory and Methods[END_REF], Proposition 3.1.1, for a proof in the time series setting which can be easily adapted to random fields).

Let us now turn to autoregressive fields with random coefficients. They are defined as in (2.1) where the coefficients (a k,l ) (k,l)∈S defining P are random. Assuming that for almost every (a k,l ), P (e iθ1 , e iθ2 ) = 0 for all (θ 1 , θ 2 ), we deduce easily that the representation (2.2) (where the coefficients (c k,l ) are now random) holds almost surely. See [START_REF] Oppenheim | Aggregation of random parameter Ornstein-Uhlenbeck or AR processes: some convergence results[END_REF] for a justification in the time series setting which remains valid for random fields. However, for (2.2) to be true in L 2 , it is necessary and sufficient that

E [-π,π] 2 |P (e iλ1 , e iλ2 )| -2 dλ 1 dλ 2 < ∞, (2.3)
where the expectation is with respect to the law of the coefficients (a k,l ) (k,l)∈S (see the same references). If (2.3) holds, the spectral density of (X i,j

) (i,j)∈Z 2 is f X (λ 1 , λ 2 ) = σ 2 ε 4π 2 E|P (e iλ1 , e iλ2 )| -2 , (2.4)
where σ 2 ε denotes the variance of the white noise (ε i,j ) (i,j)∈Z 2 . Finally, aggregation of random fields is implemented according to the classical scheme for time series. Consider N independent copies of autoregressive fields with random coefficients as above, i.e. for n = 1, . . . , N , for all (i, j) ∈ Z 2 ,

P (n) (L 1 , L 2 )X (n) i,j = ε (n) i,j , (2.5)
where (ε (n) ) are i.i.d. copies of white noises (called idiosyncratic components) and the P (n) 's come from i.i.d. copies of the random coefficients (a k,l ) (k,l)∈S . Aggregation of these N fields defines the field Z (N ) as, for all (i, j) ∈ Z 2 ,

Z (N ) i,j = 1 √ N N n=1 X (n) i,j .
(2.6)

Under condition (2.3), since the (X (n) i,j ) n 's are i.i.d, the field Z (N ) shares the same L 2 properties as the (X (n) i,j ) n 's. In particular, its spectral density is (2.4). When N goes to infinity, from the central limit theorem, Z (N ) tends to a Gaussian field Z. The aggregated field Z is thus a zero mean Gaussian field with spectral density (2.4). Moreover, contrary to Z (N ) , Z is ergodic (see [START_REF] Robinson | Statistical inference for a random coefficient autoregressive model[END_REF]).

Isotropic long memory random fields as aggregated fields

In this section we study the particular aggregation of isotropic four nearest neighbors autoregressive fields as in [START_REF] Azomahou | Memory properties and aggregation of spatial autoregressive models[END_REF]. Unfortunately that article contains false statements. Our results correct them and provide further properties.

For each n ∈ N, X (n) is the autoregressive field following the representation, for all (i, j) ∈ Z 2 ,

X (n) i,j -θ X (n) i-1,j + X (n) i+1,j + X (n) i,j-1 + X (n) i,j+1 = ε (n) i,j , (3.1)
where ε (n) is a white noise in L 2 . This representation corresponds to (2.1) where

P (L 1 , L 2 ) = 1 -θ(L 1 + L -1 1 + L 2 + L -1
2 ). When θ is not random, this model has been first considered in [START_REF] Whittle | On stationary processes in the plane[END_REF] and is studied for instance in [START_REF] Guyon | Random Fields on a Network[END_REF]. Contrary to the statement of Lemma 1 in [START_REF] Azomahou | Memory properties and aggregation of spatial autoregressive models[END_REF], we deduce from these references (or by easy computation) that the condition |θ| < 1 4 is necessary and sufficient so that (3.1) admits a stationary solution in L 2 . Let us now assume that θ is random and belongs almost surely to [0, 1 4 [ (see Remark 2 for the case θ < 0). More precisely, let us suppose that the law of θ admits a density of probability of the form Φ(x)( 1 4x) α , for 0 ≤ x ≤ 1 4 , where α > -1 and Φ is some function whose properties will be specified later. According to (2.4), if (2.3) holds, the spectral density of X (n) defined by (3.1) is in this case

f X (λ 1 , λ 2 ) = σ 2 ε 4π 2 1 4 0 Φ(x)( 1 4 -x) α (1 -2x(cos(λ 1 ) + cos(λ 2 ))) 2 dx.
Assumption (2.3) is equivalent to the integrability of f X on [-π, π] 2 . Conditions on α and Φ which imply (2.3) are deduced from the following lemma.

Lemma 1. Let α > -1 and Φ be a bounded function on [0, 1 4 ], continuous at 1 4 with Φ( 1 4 ) = 0. Consider, for any σ 2 ε > 0, the function

f defined on [-π, π] 2 by f : (λ 1 , λ 2 ) → σ 2 ε 4π 2 1 4 0 Φ(x)( 1 4 -x) α (1 -2x(cos(λ 1 ) + cos(λ 2 ))) 2 dx. (3.2) Then, (i) when α > 1, f is continuous at any point (λ 1 , λ 2 ) ∈ [-π, π] 2 , (ii) when -1 < α ≤ 1, f is continuous at any (λ 1 , λ 2 ) = (0, 0) in [-π, π] 2 and diverges to +∞ when (λ 1 , λ 2 ) → (0, 0). Moreover, as (λ 1 , λ 2 ) → (0, 0), -if -1 < α < 1, f (λ 1 , λ 2 ) ∼ c α (λ 2 1 + λ 2 2 ) α-1 (3.3) where c α = σ 2 ε 4π 2 16 -α Φ( 1 4 ) +∞ 0 u α (1+u) 2 du. -if α = 1 and assuming Φ is a β-Hölder function (β > 0), f (λ 1 , λ 2 ) ∼ c 1 | ln(λ 2 1 + λ 2 2 )| (3.4)
where

c 1 = σ 2 ε 4π 2 16 -1 Φ( 1 4
). The proof of this lemma is postponed to the appendix. As a consequence of Lemma 1, (2.3) holds if α > 0 and Φ satisfies the assumptions in Lemma 1. In this case, the aggregated field Z, constructed as the limit of (2.6) when N → ∞, belongs to L 2 and its spectral density is (3.2). The memory properties of Z are deduced from the behavior of its spectral density. When it is continuous, then Z exhibits short memory. When the spectral density is unbounded, then the autocovariance function of Z is not summable and Z is said to exhibit long memory. These properties are summarized in the following theorem. It provides the spectral properties improperly presented in Propositions 2 and 3 of [START_REF] Azomahou | Memory properties and aggregation of spatial autoregressive models[END_REF].

Theorem 1. Let X (n) , n ∈ N, be a sequence of i.i.d isotropic autoregressive fields defined by (3.1), where θ is random with probability density Φ(x)( 1 4x) α , 0 ≤ x ≤ 1 4 . Assume that α > 0 and that Φ is a bounded function on [0, 1 4 ], continuous at 1 4 with Φ( 1 4 ) = 0. If α = 1, assume moreover that Φ is a β-Hölder function with β > 0. Let Z be the aggregated field obtained as the limit of (2.6) when N → ∞. Then Z is a zero mean Gaussian random field in L 2 with spectral density (3.2), where σ 2 ε denotes the variance of the white noises in (3.1). In particular, • if α > 1, Z is short-range dependent, for its spectral density is continuous everywhere,

• if 0 < α < 1, Z exhibits long memory and its spectral density behaves as (3.3) at 0,

• if α = 1, Z exhibits long memory and its spectral density behaves as (3.4) at 0.

According to the results recalled in section 2, the proof of this theorem is a direct consequence of Lemma 1.

Remark 1. Following Definition 1 in [START_REF] Lavancier | Long memory random fields[END_REF], a random field over Z 2 exhibits isotropic long memory if its spectral density behaves at 0 as |λ| γ L 1 |λ| b λ |λ| , -2 < γ < 0, where λ = (λ 1 , λ 2 ), |.| denotes the euclidean norm, L is slowly varying at infinity and where b is continuous on the unit sphere in R 2 . According to (3.3), this is the case for Z when 0 < α < 1 with γ = 2α -2. When α = 1, the behavior of the spectral density at 0 is also a diverging function of |λ|. For this reason, one may also say that Z exhibits isotropic long memory, even if it does not suit the latter definition.

Remark 2. From a general point of view, the law of θ may be supported on the whole interval ] -1 4 , 1 4 [. From Theorem 1, the behavior of the spectral density at 0 is driven by the behavior of the probability density of θ near 1 4 . It is easy to see that under similar conditions, the behavior of the probability density of θ at -1 4 rules the behavior of the spectral density at points (λ 1 , λ 2 ) such that |λ 1 | = |λ 2 | = π. In particular, some similar spectral singularities may arise at these points, leading to the so-called seasonal long memory phenomena (see [START_REF] Oppenheim | Long memory with seasonal effects[END_REF] in the time-series setting).

A Proof of Lemma 1

For any fixed x < 1 4 , the integrand in (3.2) is continous with respect to (λ 1 , λ 2 ) ∈ [-π, π] 2 . Moreover, since cos(λ 1 ) + cos(λ 2 ) ≤ 2 , it is bounded by Φ(x) 4 ( 1 4x) α-2 , which is integrable when α > 1. So (i) is proved thanks to the dominated convergence theorem.

Similarly, for any (λ 1 , λ 2 ) in a sufficiently small neighborhood of some fixed ( λ1 , λ2 ) = 0, there exists ε > 0 such that cos(λ 1 ) + cos(λ 2 ) ≤ 2 -2ε. Thus for any fixed x < 1 4 , for any such (λ 1 , λ 2 ), the integrand in (3.2) is bounded by ε -2 Φ(x)( 1 4x) α . This gives the continuity of f at any point ( λ1 , λ2 ) = 0 when α > -1.

On the other hand, changing Letting A λ = cos(λ1)+cos(λ2) 2-cos(λ1)-cos(λ2) and applying the change of variables u = 4zA λ , we obtain

f (λ 1 , λ 2 ) = σ 2 ε 4π 2
4 -α (2 -cos(λ 1 ) -cos(λ 2 )) 1-α | cos(λ 1 ) + cos(λ 2 )| -α cos(λ 1 ) + cos(λ 2 )

A λ 0 |u| α Φ( 1 4 (1 -u A λ )) (1 + u) 2
du.

(A.1) Note that A λ → +∞ as (λ 1 , λ 2 ) → (0, 0). Since Φ is continous at 1 4 and bounded on [0, 1 4 ], the dominated convergence theorem applies when -1 < α < 1 and easy computations give (3.3).

When α = 1, we get from (A.1),

f (λ 1 , λ 2 ) = σ 2 ε 4π 2
4 -1 (cos(λ 1 ) + cos(λ 2 )) 2 (I 1 + I 2 ) , (A.2)

where

I 1 = A λ 0 |u| (1 + u) 2 Φ 1 4 du and I 2 = A λ 0 |u| (1 + u) 2 Φ 1 4 1 - u A λ -Φ 1 4 du.
Assuming Φ is a β-Hölder function on [0, 1 4 ] when α = 1, we have (A.3)

|I 2 | < c |4A λ | β A λ 0 |u| 1+β (1 + u) 2 du,

where c > 0, which shows that I 2 → 0 as (λ 1 , λ 2 ) → (0, 0). For I 1 , note that A λ > 0 if (λ 1 , λ 2 ) is small enough, so direct computation leads to

The equivalence (3.4) then follows easily from (A.2), (A.3) and (A.4).