Rémi Bonnet

Alain Finkel

Jérôme Leroux

Marc Zeitoun

Place-Boundedness for Vector Addition Systems with one zero-test *

Reachability and boundedness problems have been shown decidable for Vector Addition Systems with one zero-test. Surprisingly, place-boundedness remained open. We provide here a variation of the Karp-Miller algorithm to compute a basis of the downward closure of the reachability set which allows to decide place-boundedness. This forward algorithm is able to pass the zero-tests thanks to a finer cover, hybrid between the reachability and cover sets, reclaiming accuracy on one component. We show that this filtered cover is still recursive, but that equality of two such filtered covers, even for usual Vector Addition Systems (with no zero-test), is undecidable.

Introduction

Context. Petri Nets, Vector Addition Systems (VAS), and Vector Addition Systems with control states (VASS) are equivalent well-known classes of counter systems for which the reachability problem is decidable [START_REF] Mayr | An algorithm for the general Petri net reachability problem[END_REF][START_REF] Kosaraju | Decidability of reachability in vector addition systems (preliminary version)[END_REF][START_REF] Leroux | The general vector addition system reachability problem by Presburger inductive invariants[END_REF], even if its complexity is still an open problem. On the other hand, testing equality of the reachability sets of two such systems is undecidable [START_REF] Hack | The equality problem for vector addition systems is undecidable[END_REF]. For that reason, one cannot compute a canonical finite representation of the reachability set that would make it possible to test for equality. However, there is such an effective finite representation for the cover, a useful over-approximation of the reachability set which is connected to various verification problems.

If we add to VAS the ability to test at least two counters to zero, one obtains a model equivalent to Minsky machines, for which all nontrivial properties are undecidable. The study of VAS with a single zero-test transition began recently, and very few results are known for this model. Reinhardt [START_REF] Reinhardt | Reachability in Petri Nets with inhibitor arcs[END_REF] has shown that the reachability problem is decidable for VASS with one zero-test transition (as well as for hierarchical zero-tests). Abdulla and Mayr have shown that the coverability problem is decidable in [START_REF] Abdulla | Minimal cost reachability/coverability in priced timed Petri nets[END_REF], by using the backward procedure of Well Structured Transition Systems [START_REF] Abdulla | General decidability theorems for infinite-state systems[END_REF]. See [START_REF] Finkel | Well-structured transition systems everywhere![END_REF] for a survey. The boundedness problem (whether the reachability set is finite), the termination and the reversal-boundedness problem (whether the counters can alternate infinitely often between the increasing and the decreasing modes) are all decidable by using a forward procedure, a finite but non-complete Karp and Miller tree [START_REF] Finkel | Mixing coverability and reachability to analyze VASS with one zero-test[END_REF]. The place-boundedness problem, and more generally the possibility to compute a finite representation of the cover were still open problems. Only in the particular case of dimension 2 with control states, the reachability set is semilinear reachability and its basis and periods are computable [START_REF] Finkel | Decidability of reachability problems for classes of counters automata[END_REF] and then the place-boundedness is decidable; but this result cannot be extended in dimension 3, even without zero-test [START_REF] Hopcroft | On the reachability problem for 5-dimensional vector addition systems[END_REF].

Our contribution. We give an algorithm for computing a finite representation of the cover for a VAS with one zero-test. This result makes it possible to decide the place-boundedness, which is in general is undecidable for VAS extensions (such as VAS with resets [START_REF] Dufourd | Réseaux de Petri avec Reset/Transfert : décidabilité et indécidabilité[END_REF] or Lossy Minsky machines, i.e. Lossy VAS with zero-test transitions [START_REF] Bouajjani | Model checking lossy vector addition systems[END_REF][START_REF] Mayr | Undecidable problems in unreliable computations[END_REF]). Our proof techniques introduce a filtered cover, an hybrid between the reachability and cover sets, which unlike the cover reclaims accuracy on one component. We show that this set is recursive, but that one cannot decide the equality of such filtered covers of two VAS (even without zero-test). Thus, our work is a contribution to understanding the limits of decidability, taking into account two parameters: the models (VAS and VAS with zero-test) and the problems (reachability, cover and filtered cover).

The difficulty. The central problem is to compute the cover of a VAS with one zero-test. Let us explain the reasons why the usual Karp and Miller is not sufficient for that purpose. A natural idea appearing in [START_REF] Finkel | Mixing coverability and reachability to analyze VASS with one zero-test[END_REF] is to adapt the classical Karp-Miller construction [START_REF] Karp | Parallel program schemata[END_REF], first building the Karp-Miller tree, but without firing the zero test. To continue the construction after this first stage, we need to fire the zero test from the leaves of the Karp-Miller tree carrying a 0 value on the component tested to 0. The problem is that accelerations performed while building the Karp-Miller tree may have produced, on this component in the label of such a leaf, an ω value which represents infinity, and abstracts actual values. For that reason, one may not be able to determine if the zero test succeeds or not. We therefore want a more accurate information for the labeling of the leaves, for the component tested to 0. This is what the filtered cover actually captures.

The schema of our proof.

1.

We start in Section 3 with usual VAS: we extend the decidability of the reachability problem for VAS, in proving that the set Lim Reach of limits of increasing sequences of reachable states is also recursive (Lim Reach contains the reachability set). The set Lim Reach is a more sophisticated set than both the cover and the reachability set. It allows us to know whether an element in (N∪{ω}) d is a reachable state or is the limit of a sequence of reachable states. This information is not given by the reachability set neither by the cover. The proof carries on by using Higman's Lemma, using a nontrivial ordering.

2.

In Section 4, we refine the definition of the cover in which the first component has now to be exactly known (and not only bounded by a maximum). We prove that, for VAS, a finite basis of this filtered cover is still computable by using the recursivity of Lim Reach. 3. We finally compute in Section 5 the finite basis of the cover of a VAS with one zero-test by using a variation of the Karp and Miller algorithm that uses the previously defined filtered covers in order to convey enough information to go through the zero-test.

Due to lack of space, some proofs are omitted.

Vector Addition Systems

Orderings and vectors. An ordering on a set X is a reflexive, transitive and antisymmetric binary relation on X. Given x, y ∈ X, we write x ≺ y for x y and x = y. For d 1, we write any x ∈ X d as x = (x(1), . . . , x(d)), with x(i) ∈ X. The pointwise ordering on X d , still denoted , is defined by x y if x(i) y(i) for all i. For x 1 ∈ X d1 and x 2 ∈ X d2 , we let (x 1 , x 2 ) ∈ X d1+d2 be the vector obtained by gluing x 1 and x 2 . For X = N, let 0 be the vector whose components are all 0, and for i ∈ {1, . . . , d}, let e i be the vector such that e i (i) = 1 and e i (k Downward closed sets of N d . Given an ordered set, one may under suitable hypotheses construct a topological completion of this set to recover a finite description of downward closed sets [START_REF] Finkel | Forward analysis for WSTS, part I: Completions[END_REF][START_REF] Finkel | Forward analysis for WSTS, Part II: Complete WSTS[END_REF]. The completion of N d is N d ω , with N ω = N ∪ {ω}, where we extend by n ω for all n ∈ N ω . The results of [START_REF] Finkel | Forward analysis for WSTS, part I: Completions[END_REF][START_REF] Finkel | Forward analysis for WSTS, Part II: Complete WSTS[END_REF] Intuitively, a VAS 0 works on d counters, one for each component, whose initial values are given by x in . Executing a ∈ A ∪ {a Z } translates the counters according to δ(a) ∈ Z d . The mapping δ extends to a monoid morphism δ :

) = 0 if k = i. Finally, given Y ⊆ X, let ↓ Y = {x ∈ X | ∃y ∈ Y,
(A ∪ {a Z }) * → Z d , so that δ(ε) = 0 and δ(uv) = δ(u) + δ(v) for u, v ∈ (A ∪ {a Z }) * . A word u ∈ (A ∪ {a Z }) * is fireable from x ∈ N d if (a)
for every prefix v of u, we have x + δ(v) 0, and (b) for every prefix wa Z of u, we have [x + δ(w)](1) = 0.

The first condition means that all counters must remain nonnegative while firing actions. The second one says that the zero-test a Z is possible only when the first counter is zero. We write x u -→ y if u is fireable from x and y = x + δ(u). This implies in particular that x, y 0.

◮ Definition 2. (VAS). A Vector Addition System (VAS) of dimension d is a tuple

A, δ, x in , where A is a finite alphabet, δ : A → Z d is a mapping, and x in ∈ N d is the initial state.
A VAS is a particular VAS 0 : choosing δ(a Z ) = -e 1 makes the zero-test a Z never fireable. Given the VAS S = A, δ, x in , we say that u ∈ A * is fireable if condition (a) above is satisfied.

For a VAS 0 or a VAS S, the reachability set Reach(S) and the cover Cover(S) of S are:

Reach(S) = {x in + δ(u) | u is fireable in S},

Cover(S) = ↓Reach(S).

We call elements of Reach(S) reachable states (also called reachable markings in related work). The reachability (resp. coverability) problem consists in deciding membership in the set Reach(S) (resp. in Cover(S)). Reachability is decidable for VAS [START_REF] Mayr | An algorithm for the general Petri net reachability problem[END_REF][START_REF] Kosaraju | Decidability of reachability in vector addition systems (preliminary version)[END_REF][START_REF] Leroux | The general vector addition system reachability problem by Presburger inductive invariants[END_REF] and VAS 0 [START_REF] Reinhardt | Reachability in Petri Nets with inhibitor arcs[END_REF].

◮ Theorem 3. Given a VAS S, the reachability problem is decidable.

Leibniz International Proceedings in Informatics Schloss Dagstuhl -Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany

Testing membership in the cover set is easier. One even gets a more precise result [START_REF] Karp | Parallel program schemata[END_REF][START_REF] Finkel | Well-structured transition systems everywhere![END_REF][START_REF] Finkel | Forward analysis for WSTS, Part II: Complete WSTS[END_REF].

◮ Theorem 4. Given a VAS S, one can effectively compute a finite basis of Cover(S).

Observe that from a finite basis B of a downward closed set D, one can effectively test membership in D. Therefore, one can effectively test membership in Cover(S). Computing a finite basis of the cover makes it possible to decide place-boundedness, that is, whether the projection of Reach(S) on some given component is bounded. In the next sections, we will show that one can also effectively compute a finite basis for the cover of a VAS 0 .

3

Limits of reachable states of a VAS

Limits in N d ω . A sequence (ℓ n ) n 0 (also written (ℓ n ) n ) of elements of N ω has limit ℓ ∈ N ω , noted lim n ℓ n = ℓ, if
either it is ultimately constant with value ℓ, or its subsequence of integer values is infinite, it tends to infinity, and

ℓ = ω. A sequence (x n ) n of vectors of N d ω has limit x ∈ N d ω , noted lim n x n = x, if lim n x n (i) = x(i) for all i ∈ {1, . . . , d}. For M ⊆ N d ω ,
we denote by Lim M the set of limits of sequences of elements of M . Note that M ⊆ Lim M . Topologically speaking, Lim M is the least closed set (for the topology associated with the ordering) containing M and is usually called the (topological) closure of M . Also note that for

M ⊆ N d , if Lim M is recursive, then so is M = N d ∩ Lim M .
However, in general, M may be recursive while Lim M is not.

We prove in this section the following statement.

◮ Theorem 5. Lim Reach(S) is recursive.

We do so by proving that Lim Reach(S) and its complement in N d ω are both recursively enumerable. We start by proving that Lim Reach(S) is recursively enumerable, by introducing productive sequences, a notion inspired by Hauschildt [START_REF] Hauschildt | Semilinearity of the Reachability Set is Decidable for Petri Nets[END_REF].

◮ Definition 6. Let S = A, δ, x in be a VAS. A sequence π = (u i ) 0 i k of words u i ∈ A * is productive in S for a word v = a 1 • • • a k (a i ∈ A) if
(1) the partial sums δ(u 0 ) + • • • + δ(u i ) are nonnegative for every i ∈ {0, . . . , k}, and (2) the word

u 0 a 1 u 1 • • • a k u k is fireable from x in .
The total sum k i=0 δ(u i ) is called the production of π and is simply denoted δ(π).

The following lemma provides a characterization of the productive sequences.

◮ Lemma 7. A sequence π = (u i ) 0 i k is productive for v = a 1 • • • a k if and only if the words u n 0 a 1 u n 1 • • • a k u n k are fireable from x in for all n 1.
In particular, every marking in

x in + δ(v) + nδ(π) where n 1 is reachable from x in .
Proposition 9 below shows that limits of reachable states can be witnessed by productive sequences. Its essential argument is Higman's Lemma. Recall that an ordering is well if every infinite sequence (ℓ n ) n∈N admits an infinite increasing subsequence (ℓ n k ) k∈N : ℓ n0 ℓ n1 ℓ n2 • • • . The pointwise ordering on N d or on N d ω is well (Dickson's Lemma). Higman's Lemma. For a (possibly infinite) set Σ, we denote by Σ * the set of finite words over Σ. Given an ordering on Σ, let * be the ordering on Σ * defined as follows: for

u, v ∈ Σ * , we have u * v if u = a 1 • • • a n with a i ∈ Σ, v = v 0 b 1 v 1 • • • v n-1 b n v n , with v i ∈ Σ * , b j ∈ Σ,
and for all i = 1, . . . , n, we have a i b i . In other words, u is obtained from v by removing some letters, and then replacing some of the remaining letters by smaller ones. Higman's Lemma is the following result, see [START_REF] Diestel | Graph Theory[END_REF] for instance for a proof.

◮ Lemma 8. (Higman)

If is a well ordering on A, then * is a well ordering on A * .

We extend the multiplication on N ω by ω

• 0 = 0 = 0 • ω and ω • k = ω = k • ω if k = 0.
This multiplication then extends componentwise to the scalar multiplication of N d ω by N ω . ◮ Proposition 9. Let S = A, δ, x in be a VAS. Then

Lim Reach(S) = x in + δ(v) + ωδ(π) | π is productive for v .
Proof. For the inclusion from right to left, if π is a productive sequence for a word v, then x in + δ(v) + ωδ(π) is the limit of the sequence (x n ) n∈N with x n = x in + δ(v) + nδ(π), and x n is a reachable state by Lemma 7. We prove the reverse inclusion thanks to Higman's lemma.

We first introduce a well ordering ⊑ over Reach(S), using an temporary ordering . Consider the infinite set Σ = A × N d ω . This set is well ordered by , defined by (a, y) (b, z) if and only if a = b and y z.

Since is a well ordering, Higman's lemma shows that * is a well-ordering over Σ * . Let us now associate to every reachable state y ∈ Reach(S) a word α y in Σ * as follows: since

y is reachable, we can choose a word v = a 1 • • • a k , with a i ∈ A, such that x in v -→ y.
We introduce the sequence (y i ) 0 i k of states defined by y i = x in + δ(a 1 • • • a i ), and we let:

α y = (a 1 , y 1 ) • • • (a k , y k ).
The ordering ⊑ over Reach(S) is defined by y ⊑ z if α y * α z and y z. Since the orderings * over Σ * and over N d are well, we deduce that ⊑ is a well ordering over Reach(S).

To show the inclusion from left to right, pick x ∈ Lim Reach(S): x is the limit of a sequence (x k ) k∈N of reachable states. By extracting a subsequence we can assume that (x k (i)) k∈N is strictly increasing if x(i) = ω, and x k (i) = x(i) if x(i) < ω. Denote by α k the word α xk associated to the reachable state x k . Since ⊑ is a well ordering, there exist m < n such that x m ⊑ x n . By construction of α m there exists a word v = a 1 • • • a k with a j ∈ A such that the sequence (y j ) 0 j k defined by y j = x in + δ(a 1 • • • a j ) for every j ∈ {1, . . . , k} satisfies:

α m = (a 1 , y 1 ) • • • (a k , y k ).

Since x m

* x n and by definition of * , there exist a sequence (z j ) 1 j k of states with y j z j , and a sequence (β j ) 0 j k of words in Σ * such that the following equality holds:

α n = β 0 (a 1 , z 1 )β 1 • • • (a k , z k )β k We call label of a word (b 1 , t 1 ) • • • (b ℓ , t ℓ ) over Σ the word b 1 • • • b ℓ over A.
Consider the sequence π = (u j ) 0 j k where u j is the label of β j . By definition of α n , we have

x in u0a1 ---→ z 1 • • • u k-1 a k -----→ z k u k -→ x n
In particular, z j = y j + δ(u 0 ) + • • • + δ(u j-1 ) for every j ∈ {1, . . . , k} and

x n = z k + δ(u k ) = y k + δ(π) = x m + δ(π).
As y j z j for every j ∈ {1, . . . , k} and x m x n , we deduce that π is productive for v.

Finally, let us prove that x = y where y = x in + δ(v) + ωδ(π). We have

x n = x m + δ(π). Let us consider i ∈ {1, . . . , d}. If x(i) < ω then x m (i) = x(i) = x n (i).
Thus δ(π)(i) = 0 and we deduce that x(i) = y(i). If x(i) = ω then x m (i) < x n (i) and we deduce that δ(π)(i) > 0 and in particular x(i) = ω = y(i). Thus x = y. We have proved that there exists a productive sequence π for a word v such that x = x in + δ(v) + ωδ(π). ◭

It is easier to prove that the complement of Lim Reach(S) recursively enumerable. We just give the construction. Let S = A, δ, x in and y ∈ N d ω . We introduce d distinct additional elements b 1 , . . . , b d ∈ A. Let B = {b 1 , . . . , b d }. We introduce the VAS S y = A ⊎ B, δ y , x in , where δ y extends δ by:

δ y (b i ) = 0 if y(i) < ω, -e i if y(i) = ω.
Finally, we define from y a sequence (y ℓ ) ℓ converging to y, by y ℓ (i) = ℓ if y(i) = ω, y(i) if y(i) < ω. ◮ Lemma 10. Let S y and (y ℓ ) ℓ constructed from y as above. Then,

y ∈ Lim Reach(S) ⇐⇒ ∃ℓ ∈ N, y ℓ / ∈ Reach(S y ). ( 1
)
In particular, the complement of Lim Reach(S) is recursively enumerable.

Theorem 5 now follows from Proposition 9 and Lemma 10.

Between the cover and the reachability set: the filtered covers

In this section, we introduce a set hybrid between the reachability and cover sets, which to our knowledge has not yet been considered. Instead of the downward closure Cover(S) of Reach(S) wrt. the pointwise ordering , we consider Cover P (S) = ↓ P Reach(S), that is, we replace with an ordering P parametrized by a set of "positions" P ⊆ {1, . . . , d}:

x P y if x(i) = y(i) for i ∈ P ,
x(i) y(i) for i / ∈ P .

The set P contains the components for which we insist on keeping equality. Thus, ∅ is the usual pointwise ordering , while {1,...,d} boils down to equality. Note that P is not a well ordering, except if P = ∅ (e.g., N ordered by {1} consists only of incomparable elements).

The ordering {1} will be abbreviated as 1 . It is a natural order to study for a VAS 0 (recall that the zero-test occurs on the first component). Indeed, the transition relation of a VAS 0 is monotonic regarding this order: if x u -→ x ′ and x 1 y, then there exists y ′ with y u -→ y ′ and x ′ 1 y ′ . More precisely, testing if Cover 1 (S) contains a vector whose first component is 0 is what we need to design our algorithm computing the cover of a VAS with one zero test. Unfortunately, this set has infinitely many maximal elements for 1 , and thus cannot be represented by a finite basis. The following theorem shows that we cannot find a sensible way to compute a representation of this set, as any representation would not allow to test for equality.

◮ Theorem 11. Given two VAS S 1 and S 2 of the same dimension d, the equality problem

Cover 1 (S 1 ) = Cover 1 (S 2 ) is undecidable.
Proof. We reduce this problem to the equality problem Reach(S 1 ) = Reach(S 2 ). This problem is known to be undecidable [START_REF] Hack | The equality problem for vector addition systems is undecidable[END_REF]. Let us first consider a VAS S = A, δ, x in of dimension d. We introduce a VAS S ′ = A, δ ′ , x ′ in of dimension d + 1 that counts in the first component the sum of the other components. Formally, x ′ in = ( The main result of this section states that both conditions of Lemma 12 actually hold when M is the reachability set of a VAS. This is obtained by first proving that Cover P (S) = Reach(S P ) where S P is a VAS constructed from S and P . From this equality, we deduce that Lim Cover P (S) = Lim Reach(S P ). Applying Theorem 5, it follows that this set is recursive, which proves condition (b) for M = Reach(S). Then by Lemma 12, condition (a) also holds.

Filter(M, f ) = x ∈ M | d i=1 f (i) < ω =⇒ x(i) = f (i) , ⇓ f M =  Filter(M, f ). Note that ⇓ f M = ↓M for f = (ω, ω, . . . , ω). On the other hand, if f ∈ N d , then ⇓ f M = ↓f if f ∈ M ,
Let S = A, δ, x in be a VAS and P ⊆ {1, . . . , d}. Let us define a VAS S P such that Reach(S P ) = Cover P (S). We consider d distinct additional elements b 1 , . . . , b d ∈ A. Let B = {b 1 , . . . , b d }. We consider the VAS S P = A ⊎ B, δ P , x in , where δ P extends δ by:

δ P (b i ) = 0 if i ∈ P -e i if i / ∈ P .
◮ Lemma 13. Let S P constructed from S and P as above. Then Cover P (S) = Reach(S P ).

Proof. Consider a state x ∈ Cover P (S). By definition, there exists y ∈ Reach(S) such that

x P y. Observe that x in * -→ y u -→ x in S P with u = d i=1 b y(i)-x(i) i
. Hence x ∈ Reach(S P ). Conversely let x ∈ Reach(S P ) and let u ∈ (A ∪ B) * such that x in u -→ x in S P . Consider the word v obtained from u by erasing all letters of B. Since δ P (b) 0 for b ∈ B, the word v is still fireable from x in . Thus y = x in + δ(v) ∈ Reach(S). Moreover, by definition of S P we have x P y. Therefore x ∈ Cover P (S). ◭

Combining Lemma 13, Theorem 5 and Lemma 12 as explained above yields:

◮ Theorem 14. Given f ∈ N d ω and a VAS S, one can effectively compute a basis of ⇓ f Reach(S).

Computing the cover of a VAS with one zero-test

We provide an algorithm computing the basis of Cover(S) of any VAS 0 S = A, a Z , δ, x in . Intuitively the algorithm, inspired by the Karp and Miller algorithm for VAS [START_REF] Karp | Parallel program schemata[END_REF], builds a tree with nodes labeled by vectors in {0} × N d-1 ω such that the finite set R of node labels satisfies the following equality when the algorithm terminates:

⇓ f Reach(S) = (↓R) ∩ N d , where f = (0, ω, . . . , ω).
In order to simplify the presentation, we assume without loss of generality that x in ∈ {0} × N d-1 and δ(a Z ) ∈ {0} × Z d-1 . In the sequel we denote by S V AS the VAS S V AS = (A, δ, x in ) obtained from S by removing the zero-test a Z . Moreover, given s ∈ {0}×N d-1 we denote by S(s) and S V AS (s) the VASs obtained respectively from S and S V AS by replacing the initial state x in by s.

At any step of the execution, in the tree built in the algorithm, every ancestor node n of a node n ′ satisfies the invariant x * = ⇒ x ′ where x, x ′ are the labels of n, n ′ and where * = ⇒ is the binary relation defined over the vectors in {0} × N d-1 ω by:

x * = ⇒ x ′ if (↓x ′ ) ∩ N d ⊆ s∈(↓x)∩N d ⇓ f Reach(S(s)).
By the next lemma, it is sufficient to maintain this invariant along each parent-child edge.

◮ Lemma 15. The binary relation * = ⇒ is reflexive and transitive.

Proof. The reflexivity is immediate. For the transitivity, we first introduce the binary relation

* -→ over N d defined by x * -→ x ′ if there exists u ∈ (A ∪ {a Z }) * such that x u -→ x ′ .
We observe that x * = ⇒ x ′ if and only if the following relation holds: ω labels a leaf. We create a child of this leaf if the vector y = x + δ(a Z ) is nonnegative. Note that in this case y ∈ {0} × N d-1 ω , since δ(a Z )(1) = 0. We do not violate the invariant when creating the child labeled y since x * = ⇒ y. We may also add new children labeled by elements of the minimal basis B(x) of the following downwardclosed set:

∀s ′ ∈ (↓x ′ ) ∩ N d ∃s ∈ (↓x) ∩ N d ∃z ∈ {0} × N d-1 ω s * -→ s ′ + z.
s∈(↓x)∩N d ⇓ f Reach(S V AS (s))
We observe that x * = ⇒ b for every b ∈ B(x), so that the invariant will still be fulfilled after adding elements of B(x).

◮ Lemma 16. The basis B(x) is effectively computable.

Proof. We introduce the set I of components i ∈ {2, . . . , d} such that x(i) = ω. We consider the VAS S ′ V AS = (A, δ ′ , x ′ ) obtained from S V AS (x) by preventing any modification of components in I. More formaly δ ′ and x ′ are defined by δ ′ (a)(i) = 0 and x ′ (i) = 0 if i ∈ I and δ ′ (a)(i) = δ(a)(i) and x ′ (i) = x(i) if i ∈ I. Theorem 14 shows that we can effectively compute the basis B ′ of ⇓ f Reach(S ′ V AS ). Now B(x) = {y + z | y ∈ B ′ }, where z is the vector defined by z(i) = ω if i ∈ I and z(i) = 0 if i ∈ I. ◭

The algorithm termination is obtained by introducing an acceleration operator ∇. We define the vector x∇y for every x, y ∈ {0} × N d-1 ω such that x y by (x∇y Let us now describe informally the algorithm. It inductively computes a tree with nodes labeled by vectors in {0} × N d-1 ω . The tree is rooted at a node labeled by x in (recall that

)(i) = ω if x(i) < y(i) x(i) if x(i) = y(i).
x in ∈ {0} × N d-1
). The tree is modified in such a way that for every node n and for every child n ′ of n, the labels x, x ′ of n, n ′ satisfy x * = ⇒ x ′ . While there exists a leaf n ′ labeled by a vector x ′ that admits an ancestor n labeled by a vector x such that x x ′ < x∇x ′ , we replace the label x ′ of node n ′ by x∇x ′ . From Lemma 17, we deduce that the invariant still holds. Since this loop just replaces some components by ω, it terminates. Then, the algorithm checks if for every leaf n labeled by x, there exists a strict ancestor (i.e., different from n) labeled by the same vector x. In this case, the algorithm terminates and it returns the set of node labels. Otherwise the algorithm considers a leaf n not fulfilling this condition, and it creates a new child of n labeled by b for each b ∈ B(x). It also creates a new child labeled by x + δ(a Z ) if this vector is nonnegative. The modification of the tree is then restarted.

The termination of this algorithm follows from König's lemma. If the algorithm does not terminate, then it would generate an infinite tree. Because this tree has a finite branching degree, by König's lemma, there is an infinite branch. Since is a well-ordering over {0} × N d-1 ω , this implies that we can extract from this infinite branch an infinite increasing subsequence. However, since we add children to a leaf only if there does not exist a strict ancestor labeled by the same vector, this sequence cannot contain the same vector twice, and must therefore be strictly increasing. But, due to the use of the operator ∇, a component with an integer is replaced by ω at every acceleration step. Because the number of ω's in the vectors labeling a branch cannot decrease, we obtain a contradiction. We deduce the following proposition. ◮ Proposition 18. Algorithm 1 terminates and it returns a finite set R such that

⇓ f Reach(S) = ↓R ∩ N d
We have proved that we can effectively compute a basis R of ⇓ f Reach(S). Now, observe that the following equality holds: if the label of every strict ancestor of n is not equal to x then

Cover(S) =

Conclusion and perspectives

Our main result is a forward algorithm, à la Karp&Miller, to compute the downward closure of the reachability set of a nonmonotonic transition system: VAS 0 . This implies that placeboundedness is decidable. For our purposes, we introduced new sets, sitting between the cover and the reachability set. Unfortunately, we cannot say anything about the complexity of the computation of the cover for VAS 0 , because our proof uses the decidability of the reachability problem for VAS as an oracle, whose complexity is still open.

Since we have solved the place-boundedness problem, a natural question would be an instance of a liveness problem, like the repeated control-state reachability problem (RCSRP). One could think of a reduction from the RCSRP to the place-boundedness problem (or to the computation of the cover), by adding a new counter c q getting increased each time the control-state q is hit. This does actually not work, because c q might be unbounded even if on each single run, it is bounded. It seems that these two problems are not close: for solving the RCSRP, we need to decide whether there is an infinite run along which a given counter is unbounded, while the cover gives boundedness information about the global reachability set, but not on infinite runs. For VAS with one weak zero-test (for instance a lossy zero-test, like a reset), the usual Karp and Miller algorithm can be easily extended, and the RCSRP is decidable; for VAS with two weak zero-test (two resets), the techniques used in [START_REF] Dufourd | Boundedness of reset P/T nets[END_REF] allow one to show that this problem is undecidable. Finally, the RCSRP remains open for VAS 0 .

We have proved new decidability results for VAS 0 . One could think that maybe, VAS 0 can be simulated by VAS. The answer is negative: the language {a n b n | n 1} * can be easily recognized by a VAS 0 , but not by a VAS [START_REF] Kosaraju | Limitations of Dijkstra's Semaphore Primitives and Petri Nets[END_REF]. More generally, one may prove that for every VAS-language L, there is a VAS 0 S such that L(S) = L * . One can also separate VAS and VAS 0 wrt. the reachability set. Hence, even if their reachability problem is decidable [START_REF] Reinhardt | Reachability in Petri Nets with inhibitor arcs[END_REF] and their cover is computable (this paper), VAS 0 are strictly more powerful than VAS.

d i=1 x

  in (i), x in ) and δ ′ (a) = ( d i=1 δ(a)(i), δ(a)) for every a ∈ A. Observe that the following equivalence holds: (n, x) ∈ Reach(S ′ ) ⇐⇒ x ∈ Reach(S) and n = d i=1 x(i) Leibniz International Proceedings in Informatics Schloss Dagstuhl -Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany

  and ⇓ f M = ∅ otherwise. Observe also that ⇓ f M is downward closed and that the maximal elements of any basis of ⇓ f M agree with f on every component i where f (i) is finite. The next lemma provides a relationship between the sets ⇓ f M and ↓ P M .◮ Lemma 12. Let M ⊆ N d . Then, the following conditions are equivalent:(a) For all f ∈ N d ω , one can effectively compute the basis of ⇓ f M . (b) For all P ⊆ {1, . . . , d}, the set Lim ↓ P M is recursive.

Assume that x * =

 * ⇒ x ′ and x ′ * = ⇒ x ′′ . Let s ′′ ∈ (↓x ′′ ) ∩ N d . From x ′ * = ⇒ x ′′ , we deduce that there exist z ′ ∈ {0} × N d-1 and s ′ ∈ (↓x ′ ) ∩ N d such that s ′ * -→ s ′′ + z ′ . From x * = ⇒ x ′ , we deduce that there exist z ∈ {0} × N d-1 and s ∈ (↓x) ∩ N d such that s * -→ s ′ + z. In particular we deduce that s * -→ s ′′ + z + z ′ . We have proved that x * = ⇒ x ′′ . ◭ Assume now that x ∈ {0} × N d-1

◮ Lemma 17 .

 17 If x * = ⇒ y with x y then x * = ⇒ x∇y.

Algorithm 1 1 : 4 :

 114 b∈R s∈(↓b)∩N dCover(S V AS (s))A reduction similar to the one provided in the proof of Lemma 16 shows that the basis of s∈(↓b)∩N d Cover(S V AS (s)) can be obtained from a basis of Cover(S ′ V AS ), where S ′ V AS is a VAS obtained from S V AS and b by removing the components i ∈ {2, . . . , d} such that b(i) = ω. We deduce the following theorem. ◮ Theorem 19. Given a VAS 0 S, one can effectively compute the finite basis of Cover(S). Leibniz International Proceedings in Informatics Schloss Dagstuhl -Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany An algorithm to compute a basis of ⇓ f Reach(S) Inputs: A VAS 0 S such that x in ∈ {0} × N d-1 and a δ(a Z ) ∈ {0} × Z d-1 . Outputs: R, a finite subset of {0} × N d-1 ω . Internal Variables: T , a tree labeled by elements of N d ω . N , a set of nodes. Algorithm: Initialize T as a single root n in , labeled by x in 2: N ← {n in } 3: while N = ∅ do Take a node n from N 5:x ← label(n)6:

7 :Replace the label of n by x 14 : 15 : 16 : 19 : 20 :

 71415161920 for all strict ancestor n 0 of n do 8:x 0 ← label(n 0 ) if x + δ(a Z )0 then Create a new node in T labeled by x + δ(a Z ), as a child of n Add this node to N for all b ∈ B(x) do Create a new node in T labeled by b, as a child of n Add this node to N 24: R ← {label(n) | n ∈ nodes(T )} 25: return R

  x y} denote the downward closure of Y with respect to . The set Y is said downward closed if Y = ↓ Y . When working in N d or N d ω (see below) we shorten the downward closure operator ↓ as ↓.

Definition 1. (VAS 0 ). A

  in this case yield that, if D ⊆ N d is downward closed, then D = N d ∩ ↓B for some finite set B ⊆ N d ω , which we call a (finite) basis of D. One can show that the maximal elements of any basis B of D still form a basis which does not depend of B. It is minimal for inclusion among all basis, and is called the minimal basis. Vector Addition System of dimension d with one zero-test (VAS 0 ) is a tuple A, a Z , δ, x in , where A is a finite alphabet of actions, a Z / ∈ A is called the zero-test, δ : A ∪ {a Z } → Z d is a mapping, and x in ∈ N d is the initial state.

	An example. Let us consider in N 2 the downward closed set
	(x, y) ∈ N 2 | x	3 ∨ y	1 ∪ (4, 2), (4, 3), (5, 2) . A (non-
	minimal) basis is ({0, 1, 2, 3} × {ω}) ∪ {(4, 3), (5, 2)} ∪ {ω} × {0, 1}.
	It is shown with dots • in the figure, where elements involving ω
	fall beyond the grid. The elements of the minimal basis are circled.
	◮

  Finally let us consider two VAS S 1 and S 2 and just observe that Reach(S 1 ) = Reach(S 2 ) if and only if Cover 1 (S ′ 1 ) = Cover 1 (S ′ 2 ). ◭ So, we cannot hope for a useful representation of the sets Cover P (S) themselves. However, one can capture the needed information differently, by replacing the downward closure ↓ P in Cover P (S) = ↓ P Reach(S) with an operator ⇓ f parametrized by a vector f of N d ω . Informally, ⇓ f M takes into account only elements of M that agree with f on its finite components. Formally, for f ∈ N d ω and M ⊆ N d , let

Leibniz International Proceedings in InformaticsSchloss Dagstuhl -Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany

* Supported by the Agence Nationale de la Recherche, AVERISS (grant ANR-06-SETIN-001) and AVER-ILES (grant ANR-05-RNTL-002).


J Almeida

J C Costa

M Zeitoun

Some structural properties of the free profinite aperiodic semigroup

Profinite semigroups provide powerful tools to understand properties of classes of regular languages. Until very recently however, little was known on the structure of "large" relatively free profinite semigroups. In this paper, we present new results obtained for the class of all finite aperiodic (that is, group-free) semigroups. Given a finite alphabet X, we focus on the following problems: (1) the word problem for ω-terms on X evaluated on the free pro-aperiodic semigroup, and (2) the computation of closures of regular languages in the ω-subsemigroup of the free pro-aperiodic semigroup generated by X.

Introduction

Context. Profinite semigroups provide powerful tools to understand properties of classes of regular languages. However, until very recently, little was known on the structure of "large" relatively free profinite semigroups. In this paper, we present some results recently obtained for the class of all finite aperiodic (that is, group-free) semigroups. This class has been investigated for a long time: the first deep instance of an Eilenberg correspondence [START_REF] Eilenberg | Automata, Languages and Machines[END_REF] goes back to Schützenberger [START_REF] Schützenberger | On finite monoids having only trivial subgroups[END_REF], who related this class of semigroups with the class of starfree languages.

For a finite alphabet X and a pseudovariety V, the free pro-V semigroup on X is denoted Ω X V. We will recall its construction in Section 2, but for now, let us just state some of its most important properties: it is naturally equipped with a metric making it a topological semigroup (meaning that the multiplication is continuous). This topological semigroup is compact and totally disconnected. Moreover, it enjoys the following universal property: every mapping ϕ : X → S into a semigroup S of V can be extended in a unique way to a continuous homomorphism φ : Ω X V → S, when we endow the finite semigroup S with the discrete topology. If S denotes the pseudovariety of all finite semigroups, there is a unique continuous homomorphism p V : Ω X S → Ω X V extending the identity mapping on X.

Motivations. Consider a signature σ, whose elements have a natural interpretation on semigroups of V. The σ-word problem over V consists in determining whether two σ-terms are equal when evaluated on semigroups of V. Due to the universal property of Ω X V mentioned above, the interpretation of elements of σ may be lifted to Ω X V, and the σ-word problem is equivalent to testing that two σ-terms have the same interpretation in Ω X V.

An example of such a signature is denoted κ. It consists of the semigroup multiplication, and of the (ω -1)-power, interpreted in Ω X V as follows: x ω-1 is the limit of the sequence (x n!-1 ). If V is a pseudovariety of aperiodic semigroups, the word problem for κ-terms is equivalent to the word problem over terms built from X using the multiplication and the ω-power, where we interpret x ω as the limit of the sequence (x n! ), or equivalently as the unique idempotent of the closed subsemigroup generated by x. On finite semigroups, x ω is the idempotent of the subsemigroup generated by X. We call such terms ω-terms.

When V is the pseudovariety G of finite groups, the κ-word problem can be solved easily: the algebra on the signature κ can be seen as the free group on X, and the term x ω-1 as the inverse x -1 of x. Testing that two terms are equal when interpreted in every finite group amounts to testing that they are equal in the free group, which can be done using rewriting rules (xy) -1 → y -1 x -1 , (x -1 ) -1 → x, xx -1 → 1 and x -1 x → 1. It is well known that this forms a confluent rewriting system, yielding a normal form which characterizes the value of a term in the free group (see e.g. [START_REF] Berstel | Transductions and context-free languages[END_REF]).

For the pseudovariety A of aperiodic semigroups, the κ-word problem is also decidable, but its solution is much more involved. It has been proposed by Mc-Cammond [START_REF] Mccammond | Normal forms for free aperiodic semigroups[END_REF], and is again based on a rewriting system. However, the rewriting computation has to be guided in order to end at a normal form characterizing the value of the term on all finite aperiodic semigroups. In this paper, we sketch an alternative approach to prove that this normal form indeed characterizes the value of a term on all finite aperiodic semigroups.

Several other problems considered recently at the interface of the theories of finite semigroups and formal languages lead to natural formulations in terms of these profinite semigroups. One of them, the computation of pointlike sets, boils down to the computation of closures of regular languages in the subalgebra of Ω X V on the signature κ, and to nonemptiness tests. For the pseudovariety G of all finite groups, Rhodes' type II conjecture asked for the computation of the kernel of an X-generated semigroup S, given by a surjective homomorphism ϕ : X + → S. The kernel consists of the elements of S which have to be related to 1 through the composite relational morphism S

ϕ -1 --→ Ω X S p G -→ Ω X G.
The algorithm proposed by Rhodes has been validated by Ash's inevitability theorem [START_REF] Ash | Inevitable graphs: a proof of the type II conjecture and some related decision procedures[END_REF] (in turn rediscovered itself by Herwig and Lascar [START_REF] Herwig | Extending partial automorphisms and the profinite topology on free groups[END_REF], see [START_REF] Almeida | Sur certains systèmes d'équations avec contraintes dans un groupe libre[END_REF]Thm. 8] for the connection between both results), and a formulation of Ash's theorem for any pseudovariety of semigroups has been proposed by the first author [START_REF] Almeida | Hyperdecidable pseudovarieties and the calculation of semidirect products[END_REF], and by the first author and Steinberg [START_REF] Almeida | On the decidability of iterated semidirect products and applications to complexity[END_REF].

A generalization of the computation of the kernel of a finite semigroup is the computation of the so-called pointlike sets with respect to some pseudovariety V: these are the subsets T of S such that t∈T µ V (t) = ∅, where µ V is the composite

relational morphism S ϕ -1 --→ Ω X S p V -→ Ω X V.
It turns out that for the case of groups, being able to compute closures of regular languages in the free group and to test nonemptiness of the intersection of two such closures is sufficient for solving Rhodes' conjecture. Pin and Reutenauer [START_REF] Pin | A conjecture on the Hall topology for the free group[END_REF] proposed a nice algorithm to compute the topological closure of a regular language in the free group: the closure operator commutes with finite unions and products, while the closure of L + , for some nonempty regular language L, is the subgroup generated by L.

Contributions. This paper presents structural properties of the relatively free aperiodic profinite semigroup Ω X A. Among the few known results concerning the profinite semigroup Ω X A, two are of particular importance: first, as stated above, McCammond [START_REF] Mccammond | Normal forms for free aperiodic semigroups[END_REF] showed that the word problem for testing equality over Ω X A of two terms built from letters using concatenation and ω-power is decidable. Second, one can effectively compute pointlike subsets of a semigroup with respect to Ω X A (the first proof, due to Henckell [START_REF] Henckell | Pointlike sets: the finest aperiodic cover of a finite semigroup[END_REF], has been recently simplified and generalized by Henckell, Rhodes and Steinberg [START_REF] Henckell | Aperiodic Pointlikes and Beyond[END_REF]).

The first contribution of the paper is an alternative proof of the word problem for ω-terms on aperiodic semigroups, which, unlike McCammond's original proof, does not use the solution of the word problem for certain Burnside semigroups. This method leads to several new applications: we prove in particular that all factors of an ω-term in the relatively free aperiodic profinite semigroup must also be representable by an ω-term. Next, we also generalize the algorithm of Pin and Reutenauer: we state and prove a similar algorithm for the pseudovariety A of aperiodic semigroups instead of that of groups. We show finally that this algorithm can be transferred from a pseudovariety to a subpseudovariety if both of them enjoy the property of being full. This makes it possible to show that the algorithm also holds for the pseudovariety R of R-trivial semigroups.

The paper is organized as follows. We recall the basics of the theory of profinite semigroups in Section 2. We then present in Section 3 McCammond's normal form. We then introduce a family of star-free languages associated to an ω-term in Section 4, which we use to reprove McCammond's theorem. Some consequences of the star-freeness of these languages are drawn in Sections 5, 6 (which is devoted to the Pin-Reutenauer algorithm) and 7. Due to lack of space, all proofs are omitted, and will be available in [START_REF] Almeida | McCammond normal forms for free aperiodic semigroups revisited[END_REF][START_REF] Almeida | The Pin-Reutenauer algorithm for aperiodic semigroups[END_REF].

Profinite semigroups

We briefly set some notation and recall the basics of the theory of profinite semigroups. See [START_REF] Almeida | Finite semigroups: an introduction to a unified theory of pseudovarieties[END_REF][START_REF] Almeida | Profinite semigroups and applications[END_REF] for introductions to this theory, or [START_REF] Almeida | Finite Semigroups and Universal Algebra[END_REF][START_REF] Rhodes | The q-theory of finite semigroups[END_REF] for comprehensive treatments.

A semigroup pseudovariety is a class of finite semigroups closed under finite direct product, subsemigroup and quotient. We call star-free, or sometimes aperiodic, a language recognized by an aperiodic semigroup (the terminology is justified by Schützenberger's theorem [START_REF] Schützenberger | On finite monoids having only trivial subgroups[END_REF]). Fix a finite alphabet X. A semigroup S separates two words u, v ∈ X + if there exists a homomorphism ϕ : X + → S such that ϕ(u) = ϕ(v). Given a pseudovariety V and u, v ∈ X + , let r V (u, v) = min |S| : S ∈ V and S separates u and v (with v) , with 2 -∞ = 0, defines a pseudo-metric on X + . Further, the relation ∼ V defined by u ∼ V v if and only if d V (u, v) = 0 is a congruence, so that the quotient set Ω X V = X + /∼ V inherits from X + a structure of semigroup.

r V (u, v) = ∞ if no semigroup of V separates u and v). Then d V (u, v) = 2 -r V (u,
We denote by Ω X V the topological completion of the metric space (Ω X V, d V ). Elements of Ω X V are called pseudowords over V. A topological semigroup is pro-V if it is compact and residually in V, where semigroups of V are endowed with the discrete topology. In particular, all semigroups of V are pro-V. It turns out that Ω X V is the pro-V semigroup freely generated by X: every mapping ϕ : X → S into a pro-V semigroup S can be extended by a unique continuous homomorphism φ : Ω X V → S. This yields an interpretation of any pseudoword u ∈ Ω X V in a pro-V-semigroup S, by the mapping u S : S X → S which associates to each function ϕ : X → S the element φ(u) ∈ S. For instance, if X = {a, b} and u = ab, the interpretation of u is the semigroup multiplication from S × S into S. For an element u of a pro-V semigroup, it is easy to check that the sequence (u n!-1 ) n converges, and we denote its limit by u ω-1 . If X = {a}, the interpretation of a ω-1 in groups coincides with the usual inversion a -1 . For aperiodic semigroups, u ω-1 and u.u ω-1 = u ω have the same interpretation, namely the unique idempotent of the closed subsemigroup generated by u.

An implicit signature is a set σ of pseudowords containing the semigroup multiplication. We consider a canonical such signature, namely κ = {ab, a ω-1 }. A pro-V semigroup S has a structure of σ-semigroup, that is, a structure of σ-algebra in which each operation in σ receives its natural interpretation in S. Given an implicit signature σ, denote by Ω σ X V the relatively V-free σ-semigroup generated by X, whose elements are called σ-words. Each σ-word has a representation by a formal term over X in the signature σ. These terms are called σ-terms. For instance, κ-terms are obtained from letters of X using multiplication and (ω -1)-power. Since our multiplication is associative, we identify terms that only differ by the order in which multiplications are to be carried out.

For a subset L of a topological semigroup S, denote by cl S (L) the closure of L in S. For convenience, we write cl(L) instead of cl ΩX S (L), cl σ (L) instead of cl Ω σ X S (L), cl V (L) instead of cl Ω X V (L), and cl σ,V (L) instead of cl Ω σ X V (L). Let p V : Ω X S → Ω X V be the only continuous homomorphism sending each free generator to itself. Slightly abusing notation, for L ⊆ X + , we will write cl σ,V (L) to denote cl σ,V (p V (L)). Since the pro-V topology of Ω σ X V is its induced topology as a subspace of Ω X V, we note that, for every L ⊆ Ω σ X S,

cl σ,V (L) = cl V (L) ∩ Ω σ X V. ( 1
)
If S is a σ-semigroup and L ⊆ S, we denote by L σ the σ-subsemigroup of S generated by L. Finally, for L ⊆ X + , we let L σ,V = p V (L) σ .

McCammond's normal form

Recall that by an ω-term, we mean an expression constructed from letters by applying the operations of concatenation and (formal) ω-power. Such an expression may be viewed naturally as an operation on finite semigroups. McCammond's solution of the word problem for Ω κ X A [START_REF] Mccammond | Normal forms for free aperiodic semigroups[END_REF] consists in the reduction of arbitrary ω-terms to a certain normal form. McCammond then goes on to show that different ω-terms in normal form cannot represent the same pseudoword over A, which he does by invoking his results on free Burnside semigroups [START_REF] Mccammond | The solution to the word problem for the relatively free semigroups satisfying t a = t a+b with a ≥ 6[END_REF]. In this section, we briefly describe the normal form and we associate with each ω-term w and positive integer n a regular language L n (w).

The first important result of this work is that, if w is in normal form and n is sufficiently large, then L n (w) is aperiodic. This result yields an alternative proof of the uniqueness of normal forms for ω-terms over A, which is independent of the theory on free Burnside semigroups, by showing that, if u and v are both ω-terms in normal form and n is sufficiently large such that

L n (u) ∩ L n (v) = ∅, then u = v.
Let us first recall the definition of McCammond's normal form. To simplify the notation, McCammond represents ω-terms over an alphabet X as wellparenthesized words in the alphabet X ∪ {(, )}, for which the parentheses are thus viewed as letters. The ω-term associated with such a word is obtained by replacing each matching pair of parentheses ( * ) by ( * ) ω . Conversely, every ωterm determines a unique correctly parenthesized word over X ∪{(, )}. We define the length of an ω-term w to be the length of the word over X ∪ {(, )} which it determines, and we denote it |w|. From hereon, in the absence of mention to the contrary, we will refer to an ω-term meaning its associated word over X ∪ {(, )}. It is easy to check that the ω-subsemigroup of the free semigroup (X ∪ {(, )}) + generated by X, where the ω-power is interpreted as the operation w → (w), is freely generated by X as a unary semigroup.

In particular, there is a natural homomorphism of ω-semigroups ǫ : U X → Ω κ X A, where U X is the set of well-parenthesized words over X, that fixes each x ∈ X (when we view X as a subset of U X and Ω κ X A in the natural way). To avoid ambiguities in the meaning of the parentheses, we write ǫ[w] for the image of w ∈ U X under ǫ. The elements of Ω κ X A will sometimes be called ω-words. Whenever we say that an ω-term over the alphabet X is a factor of another, we mean that that is the case in the free semigroup (X ∪ {(, )}) + .

The ω-word problem for A (over X) consists in deciding when two elements of U X have the same image under ǫ. To solve this problem, McCammond described a normal form for ω-terms over A. For its description, a total order is fixed on the underlying alphabet X; on the extended alphabet, we set ( < x < ) for every x ∈ X. A primitive word is a word that cannot be written in the form u n with n > 1. Two words u and v are said to be conjugate if there are factorizations of the form u = xy and v = yx, with the words x and y possibly empty. A Lyndon word is a primitive word that is lexicographically minimum in its conjugacy class. The rank of a word in the extended alphabet is the maximum number of nested parentheses in it.

A rank 0 normal form ω-term is simply a finite word. Assuming that rank i normal form terms have been defined, a rank i + 1 normal form term is a term of the form α 0 (β 1 )α 1 (β 2 ) • • • α n-1 (β n )α n , where the α j and β k are ω-terms such that (1) each β k is a Lyndon word;

(2) no intermediate α j is a prefix of a power of β j or a suffix of a power of β j+1 ;

(3) replacing each subterm (β k ) by β k β k , we obtain a rank i normal form term; (4) at least one of the properties (2) and ( 3) is lost by canceling from α j a prefix β j (in case j > 0) or a suffix β j+1 (in case j < n).

These conditions yield a unique normal form. One can verify, for instance, that the normal form of (aa) ω is a ω , that the normal form of a ω b ω is a ω abb ω , and that the normal form of (a ω b ω ) ω is a ω abb ω ba ω a ω abb ω , assuming the order a < b.

McCammond also described a method to transform an arbitrary ω-term into one in normal form with the same image under ǫ. Moreover, he proved that if two ω-terms in normal form have the same image under ǫ, then they are equal. We don't describe here McCammond's procedure to obtain the normal form. It consists in applying elementary changes that obviously retain the value of the ω-term under ǫ. The types of changes are given by the following rewriting rules, where u ↔ v abbreviates u → v and v → u, and where α and β stand for arbitrary ω-terms: Since all the rewriting rules are based on identities of ω-semigroups that are valid in A, every ω-term over X has the same image under ǫ as its normal form. To prove that distinct ω-terms in normal form have different images in Ω κ X A, McCammond used his solution of the word problem for certain free Burnside semigroups [START_REF] Mccammond | The solution to the word problem for the relatively free semigroups satisfying t a = t a+b with a ≥ 6[END_REF]. We have obtained a direct combinatorial proof of the same result which leads to many other applications.

We often use in our proofs the rank as an induction parameter for ω-terms. The rank of an ω-term is defined as the rank of its normal form, and it can be viewed as the maximal nesting of parentheses in this normal form. Thus, words have rank 0, a ω and (a ω ) ω both have rank 1 (because their normal form is a ω ), and (a ω b) ω has rank 2.

  1. ((α)) ↔ (α) 2. (α k ) ↔ (α) 3. (α)(α) ↔ (α) 4. (α)α ↔ (α), α(α) ↔ (α) 5. (αβ)α ↔ α(βα)

Acknowledgements This work was partly supported by the Pessoa Portuguese-French project Egide-Grices 11113YM Automata, profinite semigroups and symbolic dynamics. The work of the first author was supported, in part, by Fundação para a Ciência e a Tecnologia (FCT) through the Centro de Matemática da Universidade do Porto, by FCT. The work of the second author was supported, in part, by FCT through the Centro de Matemática da Universidade do Minho. Both the first and second authors were also supported by the project PTDC/MAT/65481/2006, which is partly funded by the European Community Fund FEDER. The work leading to this paper has also been carried out within the framework of the ESF programme "Automata: from Mathematics to Applications (AutoMathA)", whose support is gratefully acknowledged.

Languages L n (v) associated to an ω-term v

The main idea of the paper is to associate to each ω-term v a decreasing family of regular languages L n (v) characterizing the value of v over Ω X A (or, which is equivalent by a standard compactness argument, over all finite aperiodic semigroups). In this section we present the main properties of the languages L n (v) and derive some applications. This gives, in particular, an alternative proof of McCammond's solution of the ω-word problem for A.

For L ⊆ X + and n ≥ 1, let L ≥n = L n L * . Given an ω-term w, we let L n (w) be the regular language obtained from w by replacing all ω-powers by ≥ n. Since L ≥n ⊇ L ≥n+1 , this clearly defines a decreasing family. For instance, L n (a ω ) = a n a * . The following statement is useful to compute inductively these languages.

Lemma 1. The following formulas hold:

(1) for ω-terms u and v, we have

r is a factorization of an ω-term such that all the v j have the same rank i and all the u j have rank at most i, then

We now introduce another parameter for ω-terms.

r be a term of rank i ≥ 1 where each v j has rank i -1 and each u j has rank at most i -1. Let µ(v) denote the integer

In case v is a word, we let µ(v) = |v|. It is easy to check that, if the above expression for v is its normal form, then µ(v) ≥ max{µ(u j ), µ(v j )}. The fundamental property of the languages L n (v) is the following. Theorem 2. Let v be a term in normal form and let n ≥ µ(v). Then the language L n (v) is star-free.

The theorem is proved by induction on the rank of the term in normal form. Using Schützenberger's characterization of star-free languages, it suffices to show that there exists a bound k such that xy k z ∈ L n (v) if and only if xy k+1 z ∈ L n (v), for all words x, y, z. From xy k z ∈ L n (v), we obtain two factorizations of the same word: one is given by xy k z, and the other one by the expression of L n (v) that is obtained inductively using Lemma 1. One of the ingredients to control how these factorizations match is the following consequence of the well-known Theorem of Fine and Wilf on the relationship between the periods of a sufficiently long word and their synchronization. Lemma 3. Let u and v be Lyndon words and suppose that w is a word such that |w| ≥ |u| + |v| and w is a factor of both a power of u and a power of v. Then u = v. Moreover, for all factorizations u m = xwy and v n = zwt, there is a factorization w = w 1 w 2 such that xw 1 , zw 1 ∈ u * .

In the statement of Theorem 2, we do not know whether the bound n ≥ µ(v) is optimal, but we do know that some bound is required, that is, that L n (v) may not be star-free for v in normal form. An example is obtained by taking

From Theorem 2, one can deduce several applications, yielding an alternative proof of the ω-word problem for A, that is, an algorithm to test equality under ǫ of two ω-terms. The proof is based on the following separation criterion.

Theorem 4. Let u and v be two ω-terms in normal form and let n be an integer greater than

Corollary 5 (McCammond's solution of the word problem [START_REF] Mccammond | Normal forms for free aperiodic semigroups[END_REF]). If u and v are terms in normal form which define the same pseudoword over A, then u = v as parenthesized words.

First consequences of the star-freeness of L n (v)

There are several consequences of the star-freeness of L n (v) for v in normal form and n large enough. We first prove an important property which, apparently, does not follow easily from McCammond's results. We say that a pseudovariety

Theorem 6. The pseudovariety A is κ-factorial.

Recall now that a semigroup is stable if any two J-equivalent elements which are comparable for the ≤ R -ordering are also R-equivalent, and dually for the ≤ Lordering.

Corollary 7. The semigroup Ω κ X A is stable, and the Green relations J and D coincide in Ω κ X A. Using the very definition of the languages L n (w) and the fact that for u ∈ Ω X A, the sequence (u n ) n converges to u ω , one can show the following statement. Proposition 8. If u is an arbitrary ω-term, then

Let us now formulate another direct consequence of the star-freeness of L n (w) and of Proposition 8. Corollary 9. Let w be an ω-term in normal form. Then

However, one can show that the closures of these aperiodic languages do not form a basis for the topology of the whole pro-A semigroup.

Proposition 10. Let X be a finite alphabet with at least two letters. Then the set of all open subsets of the form cl A (L n (w)), with w an ω-term in normal form and n ≥ µ(w), is not a basis of the topology of Ω X A.

We next want to test whether some given ω-word lies in the closure of a given regular language. An answer to this question is given by the following statement. Given a semigroup S, we denote by P(S) the semigroup whose elements are the subsets of S, with the multiplication given by XY = {xy : x ∈ X and y ∈ Y }. The index of a finite semigroup S is the least integer i such that S satisfies x i+p = x i for some positive integer p. Proposition 11. Let u ∈ Ω κ X A, L ⊆ X + be a regular language, and let i be the index of P(Synt(L)).

Theorem 12. Given a regular language L ⊆ X + and w ∈ Ω κ X A, let w denote the normal form of w. Then w ∈ cl κ,A (L) if and only if L ∩ L i ( w) = ∅, where i is the index of P(Synt(L)).

Corollary 13. Given a regular language L ⊆ X + and u ∈ Ω κ X A, one can decide whether u ∈ cl κ,A (L).

The Pin-Reutenauer algorithm for A

We say that the Pin-Reutenauer procedure holds for a pseudovariety V in the implicit signature σ if, for all nonempty regular languages K, L ⊆ X + , the following equations hold:

Note that, given subsets K, L ⊆ Ω σ X V, the inclusion cl σ,V (K)cl σ,V (L) ⊆ cl σ,V (KL) is always true: it follows directly from the continuity of the multiplication.

The name is justified by the fact that the above formulas hold for the pseudovariety G of all finite groups and the implicit signature κ. This was conjectured by Pin and Reutenauer [START_REF] Pin | A conjecture on the Hall topology for the free group[END_REF] and the conjecture was reduced to another conjecture concerning the profinite topology of the free group Ω κ X G, which in turn was proved by Ribes and Zalesskiȋ [START_REF] Ribes | On the profinite topology on a free group[END_REF]. The Pin-Reutenauer conjecture was in turn introduced as an approach and later shown to be formally equivalent to the Rhodes "type II conjecture", which was settled independently by Ash [START_REF] Ash | Inevitable graphs: a proof of the type II conjecture and some related decision procedures[END_REF]. The situation for groups is somewhat simpler since the right side of formula (3) reduces to the subgroup H generated by L. To prove that indeed H = cl κ,G (L) κ , it suffices to observe that L + is contained in H and that H is finitely generated by a theorem of Anissimow and Seifert [START_REF] Anissimow | Zur algebraischen Charakteristik der durch kontext-freie Sprachen definierten Gruppen[END_REF], and therefore it is closed by a theorem of M. Hall (see [START_REF] Pin | A conjecture on the Hall topology for the free group[END_REF] for details).

For more general pseudovarieties, the topological closure on the right side of (3) cannot be dropped, as the following example shows. Consider the regular language L = a + b + and its closure cl κ (L) in Ω κ X S. We claim that L κ is not closed in Ω κ X S. Indeed, since L + ⊆ L κ , if L κ were closed then we would have cl

while one can show that for every element of L κ , the exponents of its factors of the form a n are all finite. Hence L κ is not closed in Ω κ X S. In this section, we generalize the Pin-Reutenauer procedure to pseudovarieties of finite aperiodic semigroups.

Theorem 14. The Pin-Reutenauer procedure holds for the pseudovariety A with respect to the signature κ.

We first present general results concerning closures of regular languages. It shows in particular that the Pin-Reutenauer procedure can be transferred from a pseudovariety to a subpseudovariety, provided both pseudovarieties are σ-full (as defined below). We shall use this to deduce that the Pin-Reutenauer procedure also holds for R, the pseudovariety of all R-trivial semigroups.

Given a finite X-generated semigroup S and an onto continuous homomorphism ϕ : Ω X S → S, we denote by µ V the relational morphism S → Ω X V given by µ

, and by μσ V the relational morphism given by μσ V = µ V ∩(S×Ω σ X V). Following [START_REF] Almeida | On the decidability of iterated semidirect products and applications to complexity[END_REF][START_REF] Almeida | Syntactic and global semigroup theory, a synthesis approach[END_REF], we say that V is σ-full if μσ V = µ σ V for every such homomorphism ϕ : Ω X S → S into a finite semigroup S. Proposition 15. A pseudovariety V is σ-full with respect to an implicit signature σ if and only if, for every regular language L ⊆ X + , we have the equality

The following statement allows us to transfer properties (2) and (3) to subpseudovarieties, assuming fullness. Proposition 16. Let V, W be two σ-full pseudovarieties such that V ⊆ W. Let K, L ⊆ X + be regular languages.

We state for the record the following consequence of Proposition 16.

Corollary 17. Let V and W be σ-full pseudovarieties such that V ⊆ W. If the Pin-Reutenauer procedure holds for W with respect to σ then it also holds for V. ⊓ ⊔ Note that an immediate consequence of Corollary 17 is that if the Pin-Reutenauer procedure holds for the pseudovariety S of all finite semigroups with respect to the implicit signature σ then it also holds for every σ-full pseudovariety. Indeed, S is trivially σ-full for every implicit signature σ. This motivates the problem of determining for which implicit signatures the Pin-Reutenauer procedure holds for S. In view of the above and later results in this paper, it would be particularly interesting to consider this problem for the signature κ. Proposition 18. Let K, L ⊆ X + be regular languages. Let σ be an implicit signature, and V be a σ-factorial pseudovariety. Then cl σ,V (KL) = cl σ,V (K)cl σ,V (L).

For the closure of regular languages of the form L + in Ω κ X A, the most difficult inclusion to prove is the following. Proposition 19. Let w be a κ-term in normal form over the finite alphabet X, let L ⊆ X + be a regular language, and suppose that w ∈ cl κ,A (L + ). Then w ∈ cl κ,A (L) κ .

κ-fullness of A and an application

In order to be able to apply Theorem 14 and Corollary 17 to deduce that κ-full subpseudovarieties of A are also such that the Pin-Reutenauer procedure holds for them, we need the following result.

Theorem 20. The pseudovariety A is κ-full.

In turn, the following is a simple application of well-developed techniques concerning the pseudovariety R of all finite R-trivial semigroups.

Theorem 21. The pseudovariety R is κ-full.

We may now apply Corollary 17 to obtain the following result.

Theorem 22. The Pin-Reutenauer procedure holds for the pseudovariety R with respect to the signature κ.

⊓ ⊔