Cécile Hardouin
email: hardouin@univ-paris1.fr

Jian-Feng Yao
email: jian-feng.yao@univ-rennes1.fr

Multi-parameter auto-models and their application

Keywords: Auto-models, Multi-parameter exponential families, spatial cooperation, beta conditionals

Motivated by the modelling of non Gaussian data or positively correlated data on a lattice, extensions of Besag's Markov random fields auto-models to exponential families with multi-dimensional parameters have been proposed recently. In this paper, we provide a multiple-parameter analog of Besag's one-dimensional result that gives the necessary form of the exponential families for the Markov random field's conditional distributions. We propose estimation of parameters by maximum pseudo-likelihood and give a proof for the consistency of the estimators for the multiparameter auto-model. The methodology is illustrated with some examples, particularly the building of a cooperative system with beta conditional distributions.

Introduction

We consider a random field X = {X i , i ∈ S} on a finite set of sites S = {1, . . . , n}. For a site i, let p i (x i |x (i) ) = p i (x i |x j , j = i) be the full conditional distribution, that is the conditional density of X i given the values of all the X j 's other than X i , where we have used the notation x (i) = {x j : j = i}. An important approach in stochastic modelling consists of specifying the family of these conditional distributions {p i (x i |•) : i ∈ S}, and then determining a joint distribution P of the random field that is compatible with this family (i.e., the p i 's are exactly the conditional distributions associated with P ). The investigation of this problem dates back to the 1960's; see [START_REF] Whittle | Stochastic processes in several dimensions[END_REF] and [START_REF] Bartlett | A further note on nearest neighbour models[END_REF]. Let us recall that if the joint probability distribution P is positive wherever the marginal distributions are positive, the Hammersley-Clifford Theorem characterizes log P as being proportional to a sum of potentials deduced from a set of cliques. The milestone paper of [START_REF] Besag | Spatial interactions and the statistical analysis of lattice systems[END_REF] provides several key steps for the development of the subject, including a proof of the Hammersley-Clifford theorem, the introduction of auto-models, and popular estimation methods such as maximum pseudo-likelihood estimation. Related developments on conditionally specified models include a series of works by Arnold, Castillo, and Sarabia; see [START_REF] Arnold | Conditional Specification of Statistical Models[END_REF], [START_REF] Arnold | Conditionally specified distributions: an introduction (with discussion)[END_REF] for complete references, even though their approach is not specifically suited to the Markov random-field framework.

In this paper, we focus on auto-models introduced by [START_REF] Besag | Spatial interactions and the statistical analysis of lattice systems[END_REF]. This class of spatial models is constructed under two assumptions: first, the dependence between sites is pairwise and, secondly, the full conditionals belong to some exponential family. Special instances of auto-models include the so-called auto-logistic, auto-binomial, auto-Poisson, auto-exponential, auto-gamma and auto-normal schemes. However, these schemes have a major limitation: the sufficient statistic as well as the canonical parameter are onedimensional. More precisely, the exponential families can involve more than one parameter, but both the sufficient statistic and the canonical parameter are one-dimensional: for instance, in the so-called auto-normal scheme, the conditional mean at each site i is expressed as a linear combination of the values at its neighbouring sites {x j , j = i}, and the conditional variance is constant or depends only on the site i. Furthermore, integrability conditions have to be satisfied for the model to be well defined. As noticed by the author himself, several auto-models like the Poisson, exponential, and gamma schemes are of little practical interest, since the integrability condition ensures that only spatial competition between neighbouring sites can occur. However, mostly one would like to model spatial cooperation.

To overcome these drawbacks, significant effort has been put in by a number of au-

thors. An extension of the first condition is proposed in [START_REF] Lee | Multiway dependence in exponential family conditional distributions[END_REF], where the pairwise dependence is replaced with a multiway dependence, but still with one parameter exponential families. Recently, a Markovian approach is proposed in [START_REF] Kaiser | The construction of multivariate distributions from Markov random fields[END_REF], where the commonly used positivity condition on the joint distribution is relaxed.

To the best of our knowledge, the first attempt to extend the one-parameter exponential family set-up to a multi-parameter one was made by [START_REF] Cressie | New models for Markov random fields[END_REF], where the term multi-parameter exponential family Markov random field models was coined. Later, improvements were proposed in [START_REF] Kaiser | The construction of multivariate distributions from Markov random fields[END_REF], where a spatial model using beta conditional distributions, an exponential family with two-parameters, is analysed in detail. In [START_REF] Kaiser | Spatial mixture models based on exponential family conditional distributions[END_REF], Equation ( 7), the authors introduce a class of spatial models with general multi-parameter exponential family conditional distributions and raise the question of ensuring their compatibility with a joint distribution. A general answer to this question is the subject of this paper.

We give here the general parametrisation of multi-parameter auto-models, which is a new result. The main result of this paper, Theorem 1 in Section 2, determines the necessary form for multi-parameter exponential families in terms of the full conditionals. We provide a directly analogous result to that of Eq. (4.4) in [START_REF] Besag | Spatial interactions and the statistical analysis of lattice systems[END_REF].

Having established the general result, we examine several related problems. We begin with a simple illustration of an auto-model on two sites, which is interesting because we consider different state spaces. Then, in Section 3, we address the problem of building cooperative spatial models. In particular, we discuss auto-models with full conditionals that are beta distributed and we give explicit conditions on the parameters to ensure the integrability condition. These auto-models have the advantage of being able to exhibit spatial cooperation as well as spatial competition according to suitable choices of their parameter values. The results are more general than those of [START_REF] Kaiser | The construction of multivariate distributions from Markov random fields[END_REF] and [START_REF] Kaiser | Spatial mixture models based on exponential family conditional distributions[END_REF].

Next, in Section 4, the consistency of the pseudo-likelihood estimator in multi-parameter auto-models is established under quite general conditions. To give more insight into the effectiveness of this estimator, several simulation experiments are conducted for auto-models with beta conditional distributions and two different neighbourhood systems.

In Section 5, we give a discussion of our findings. Proofs of the theoretical results are gathered together in Section 6.

2 Multi-parameter auto-models Recall the set of sites S = {1, . . . , n}, and consider a measurable state space (E, E, m) (often a subset of R). We let the configuration space Ω = E S be equipped with the σalgebra E ⊗S and the product measure ν := m ⊗S . Although we consider Ω = E S , all the following results hold equally with a more general configuration space Ω = i∈S E i , where each individual space (E i , E i ) is equipped with some measure m i (we give such an example at the end of this section). A random field is specified by a probability distribution µ on Ω, and we will assume throughout the paper the positivity condition, namely, µ has an everywhere positive density P with respect to ν. Consequently we can write

µ(dx) = P (x)ν(dx) , P (x) = Z -1 exp Q(x) , (2•1)
where Z is a normalisation constant. From the Hammersley-Clifford Theorem, the energy function Q(x) is a sum of potentials G defined on the set of underlying cliques. Moreover, the positivity condition implies that at each site i, the conditional distribution of (X i |X j = x j , j = i) has a density p i (x i |x (i) ) with respect to m(dx i ) that is itself everywhere positive.

The two basic assumptions are as follows.

[B1] The dependence between the sites is pairwise-only, that is,

Q(x) = i∈S G i (x i ) + {i,j} G ij (x i , x j ) .
We fix a reference configuration τ = (τ i ) ∈ Ω. In most cases, τ = (0, . . . , 0), but the choice of this reference configuration is arbitrary [START_REF] Guyon | Random Fields on a Network: Modeling, Statistics, and Applications[END_REF], [START_REF] Kaiser | The construction of multivariate distributions from Markov random fields[END_REF]). In the case of the beta conditional distributions in Section 3, E = (0, 1) and we take τ = ( 1 2 , . . . , 1 2 ). The following notation is useful. If x ∈ Ω, for each i we denote τ i x to be the realisation deduced from x replacing x i with τ i .

Next, the potential functions are uniquely determined if we assume for all i, j, and

x ∈ Ω that G ij (τ i , x j ) = G ij (x i , τ j ) = G i (τ i ) = 0 .
(2•2)

Note that if this condition were not naturally satisfied, we may substitute for G ij (x i , x j ),

G ij (x i , x j ) -G ij (τ i , x j ) -G ij (x i , τ j ) + G ij (τ i , τ j ) ,
and make a similar adjustment for G i (x i ). Thus, from (2•1), we have Q(τ ) = 0 and Z -1 = P (τ ).

The second assumption generalises Besag's auto-models schemes of one-parameter exponential families to multi-parameter exponential families:

[B2] : log p i (x i |x (i) ) = A i (x (i) ), B i (x i ) +C i (x i )+D i (x (i) ) , A i (x (i) ) ∈ R l , B i (x i ) ∈ R l .
The main result of the paper is the following theorem, which determines the necessary form of the local natural parameters {A i (.)} to ensure the compatibility of the family of full conditional distributions.

Theorem 1 Assume that the two conditions [B1] and [B2] are satisfied with the normalisation

B i (τ i ) = C i (τ i ) = 0 in [B2]
. Furthermore, assume the following condition

[C]: For all i ∈ S, Span{B i (x i ) : x i ∈ E} = R l .
Then, necessarily, the functions A i take the form:

A i (x (i) ) = α i + j =i β ij B j (x j ) ; i ∈ S, (2•3)
where {α i : i ∈ S} is a family of l-dimensional vectors, and

{β ij : i, j ∈ S, i = j} a family of l × l matrices {β ij } satisfying β T ij = β ji .
Moreover, the potentials are given by

G i (x i ) = α i , B i (x i ) + C i (x i ) , (2•4) G ij (x i , x j ) = B T i (x i )β ij B j (x j ) .
(2•5)

A model satisfying the assumptions of the theorem is called a multi-parameter automodel. The additional condition [C] is not present in the one-parameter case, since it is automatically satisfied, because the B i 's are not identically zero. We shall see below that this condition is not restrictive and is easily satisfied in most examples.

Another important property of the model is that of symmetry. The general formulation given above does not impose any symmetry, and hence it can be useful for modelling random fields on arbitrary or oriented graphs. As an illustration, a simple auto-model is given at the end of this section on two sites that play an asymmetrical role. On the other hand, in the case of a spatially symmetrical random field, it is necessary that all the potentials G ij (x i , x j ) are symmetric functions or, equivalently, that all the matrices β ij are symmetric.

It is interesting at this point to compare the necessary form (2•3) and several existing forms proposed in [START_REF] Kaiser | Spatial mixture models based on exponential family conditional distributions[END_REF]. It is not difficult to see that their three proposed forms, Eqs. ( 10), (11), and (12) of [START_REF] Kaiser | Spatial mixture models based on exponential family conditional distributions[END_REF], correspond respectively to the cases,

β ij = η ij    1 • • • 1 1 . . . 1 1 • • • 1    ; η ij = η ji ∈ R , (2•6) β ij =    η ij1 • • • 0 0 . . . 0 0 • • • η ijl    ; η ijk = η jik ∈ R, 1 ≤ k ≤ l , (2•7)
and

β ij = η ij 0 1 1 0 ; η ij = η ji ∈ R. (2•8)
Even though these specific forms are useful in practice, the general result is given by Eqs.

(2•4) and (2•5).

The following proposition is useful, giving a converse to Theorem 1. It also provides a practical way to choose the parameters for a well defined multi-parameter auto-model. Indeed, the only additional condition one must check in practice is that the energy function Q is admissible in the sense of the integrability condition:

Ω e Q(x) ν(dx) < ∞ .
(2•9)

Proposition 1 Assume that the energy function Q is defined by [B1] with potentials G i , G ij given in (2•4) and (2•5). Assume further that the integrability condition (2•9) holds. Then the family of conditional distributions p i (x i |x (i) ) belong to a multi-parameter exponential family given by [B2] whose natural parameters A i (x (i) ) satisfy (2•3).

We now give a simple example illustrating Theorem 1. Consider just two variables (X 1 , X 2 ) such that the conditional distribution of X 1 given X 2 = x 2 is a gamma distribution, and X 2 given X 1 = x 1 is a Gaussian distribution. This example with S = {1, 2} is interesting since the two state spaces are different, and the model is not symmetric. The reference configuration is τ = (1, 0). In other words, we have according to [B2]:

log p 1 (x 1 |x 2 ) = log f θ 1 (x 2 ) (x 1 ) = A 1 (x 2 ), B 1 (x 1 ) -D 1 (x 2 ) , log p 2 (x 2 |x 1 ) = log g θ 2 (x 1 ) (x 2 ) = A 2 (x 1 ), B 2 (x 2 ) -D 2 (x 1 ) . Here l = 2 and B i 's in [B2] are B 1 (x) = (-x + 1, log x) T and B 2 (x) = (x, x 2 ) T .
Condition [C] is trivially satisfied here. Therefore, by Theorem 1, there exist two vectors α 1 , α 2 of R 2 and a 2 × 2 matrix β such that

A 1 (x 2 ) = α 1 + βB 2 (x 2 ) , A 2 (x 1 ) = α 2 + β T B 1 (x 1 )
The joint density is

P (x 1 , x 2 ) = P (τ ) exp Q(x 1 , x 2 ) with Q(x 1 , x 2 ) = α 1 , B 1 (x 1 ) + α 2 , B 2 (x 2 ) + B T 1 (x 1 )βB 2 (x 2 ) .
If we do not consider the matrix β to be symmetric, and it does not have to be, the model contains 8 parameters. Explicit conditions on these parameters can be obtained straightforwardly from (2•9) to ensure admissibility of the energy function Q. In fact, this is a known result presented in [START_REF] Arnold | Conditional Specification of Statistical Models[END_REF], §4.8, but our derivation is simpler.

A special class of auto-models with beta conditionals

As pointed out in [START_REF] Besag | Spatial interactions and the statistical analysis of lattice systems[END_REF], several one-parameter auto-models necessarily imply spatial competition but not spatial cooperation between neighbouring sites. For instance, this is the case for the auto-exponential, the auto-Poisson and the auto-gamma schemes. This competitive behaviour is clearly inadequate for many spatial systems where neighbouring sites are indeed cooperative. A common way to get rid of this drawback is to transform the variables onto a bounded range. For instance a truncation or projection procedure could be used.

Another possible way to get cooperative auto-models is by using multi-parameter automodels such as beta conditional distributions. Notice that the family of beta distributions offers a large variety of densities on a bounded interval [a, b], which makes the auto-beta models a potentially important class of spatial models.

Consider the univariate beta density on (0, 1) with parameters p, q > 0 :

f θ (x) = κ(p, q)x p-1 (1 -x) q-1 = exp { θ, B(x) -ψ(θ)} , 0 < x < 1, where θ = (p-1, q-1) T , B(x) = [log(2x), log(2(1-x))] T , ψ(θ) = (p+q-2) log 2+log κ(p, q), and κ(p, q) = Γ(p + q)/[Γ(p)Γ(q)]. Throughout this section, we denote the two components of B(x) by u(x) = log(2x) and v(x) = log[2(1 -x)]. Notice that u( 1 2 ) = v( 1 2 ) = 0.
We now consider a random field X with such beta conditional distributions and reference configuration τ = ( 1 2 , 1 2 , ..., 1 2 ). Clearly, Condition [C] is satisfied. From Theorem 1, for i, j ∈ S and i = j, there exist vectors

α i = (a i , b i ) T ∈ R 2 and 2×2 matrices β ij = c ij d ij f ij e ij satisfying β ij = β T ji , such that A i (x (i) ) = α i + j =i β ij B(x j ) = α i + j =i β ij u(x j ) v(x j ) .
Furthermore, the energy function Q can be written as

Q(x 1 , . . . , x n ) = i∈S α i , B(x i ) + {i,j} B T (x i )β ij B(x j ) ,
and the reference configuration, τ = ( 1 2 , . . . , 1 2 ), satisfies Q(τ ) = 0. This model is well defined if its energy function Q satisfies the integrability condition (2•9), something we now examine in detail. We first note that the natural parameters of the conditional beta distributions are given by

A i (x (i) ) = A i,1 (x (i) ) A i,2 (x (i) ) = a i + j =i {c ij u(x j ) + d ij v(x j )} b i + j =i {f ij u(x j ) + e ij v(x j )} . (3•1)
Since p > 0 and q > 0 defines the natural parameter space for the univariate beta distribution, it follows that for all i and all configurations

x (i) ∈ (0, 1) n-1 , 1 + a i + j =i {c ij u(x j ) + d ij v(x j )} > 0 , (3•2) and 1 + b i + j =i {f ij u(x j ) + e ij v(x j )} > 0 . (3•3)
We first consider the inequality (3•2) . If x j tends to 0+ or 1-, it follows necessarily that c ij ≤ 0 and d ij ≤ 0. Consequently,

c ij u(x j ) + d ij v(x j ) = (c ij + d ij ) log 2 + c ij log(x j ) + d ij log(1 -x j ) ≥ (c ij + d ij ) log 2.
Therefore, a sufficient condition for (3•2) is,

c ij ≤ 0, d ij ≤ 0, and 1 + a i > -(log 2) j =i (c ij + d ij ) . (3•4)
Similarly, a sufficient condition for the second inequality (3•3) is

f ij ≤ 0, e ij ≤ 0, and 1 + b i > -(log 2) j =i (f ij + e ij ) . (3•5)
Under these conditions, the family of beta conditional distributions {p i (x i |x (i) ) , i ∈ S} is everywhere well defined.

As we now show in the following proposition, these conditions also ensure the admissibility of the energy function Q.

Proposition 2 Assume that for all i, j ∈ S, the conditions (3•4) and (3•5) are satisfied. Then 1. The family of beta conditional distributions {p i (x i |x (i) ) , i ∈ S} is everywhere well defined.

2. The energy function Q satisfies the integrability condition (2•9).

Consequently, the auto-model with beta conditional distributions is well defined by (3•1).

While the conditions (3•4) and (3•5) are already used in practice (see [START_REF] Kaiser | The construction of multivariate distributions from Markov random fields[END_REF] and [START_REF] Kaiser | Spatial mixture models based on exponential family conditional distributions[END_REF]), we are not aware of any published proof that they are sufficient for (2•9) and hence for the joint distribution to exist. Having well defined conditional distributions does not necessarily imply well defined joint distribution.

3•1 Spatial cooperation versus spatial competition

We now examine the spatial-competition and spatial-cooperation behaviour of the autobeta model. At each site i, the mean of the conditional distribution

p i (x i |x (i) ) is E(X i |x (i) ) = 1 + A i,1 (x (i) ) 2 + A i,1 (x (i) ) + A i,2 (x (i) )
.

The model is said to be spatially cooperative (respectively competitive) if, at each i,

E(X i |x (i)
) is non-decreasing (respectively non-increasing) in each neighbouring value x j , and is increasing (respectively decreasing) in at least one. Notice that E(X i |x (i) ) increases with A i,1 (x (i) ) and decreases with A i,2 (x (i) ).Therefore, the auto-beta model is spatially cooperative if, for all i = j, c ij = e ij = 0; and it is spatially competitive if, for all i = j,

d ij = f ij = 0.
To conclude the discussion about the auto-beta models, we compare our results to those of [START_REF] Kaiser | The construction of multivariate distributions from Markov random fields[END_REF], specifically their eq. ( 16). In our notation, their auto-beta model corresponds to:

β ij = -η ij 0 1 1 0 , η ij ≥ 0.
In other words, c ij = e ij = 0 and

d ij = f ij = -η ij ,
where η ij ≥ 0. This provides an autobeta model with spatial cooperation as proved by [START_REF] Kaiser | The construction of multivariate distributions from Markov random fields[END_REF], but our results are more general. For example, the constraint d ij = f ij is generally unnecessary, except in the case of a spatially symmetrical random field (see the remark following Theorem 1).

3•2 A spatially cooperative model with a scheme that has four or eight nearest neighbours

First consider the scheme with four nearest neighbours on a two-dimensional lattice, S = [1, M] × [1, N]: each site i ∈ S has four neighbours denoted as {i e = i + (1, 0), i w = i -(1, 0), i n = i + (0, 1), i s = i -(0, 1)} (with obvious neighbour adjustments near the boundary). We assume translation invariance in the sense that the parameters are functions of the displacement between sites; we assume spatial symmetry, which implies d ij = f ij ; we allow possible anisotropy between the horizontal and vertical directions; and we assume c ij = e ij = 0, in order to model spatial cooperation. Under all these conditions and from the result above, there exists a vector α = (a, b) and two 2 × 2 matrices,

β (k) = d k 0 1 1 0 , k = 1, 2, (3•6)
such that for all i, vectors α i = α, and for all {i, j}, matrices β ij = 0 unless i and j are neighbours, in which case

β i,ie = β iw,i = β (1) , β i,in = β is,i = β (2) .
The model involves 4 parameters (a, b, d 1 , d 2 ). The integrability conditions (3•4) and (3•5) become

d 1 ≤ 0, d 2 ≤ 0 ; (1 + a) ∧ (1 + b) > -2(d 1 + d 2 ) log 2 . (3•7)
The conditional distributions are beta-distributed with natural parameters,

A i (x (i) ) = a + d 1 [v(x ie ) + v(x iw )] + d 2 [v(x in ) + v(x is )] b + d 1 [u(x ie ) + u(x iw )] + d 2 [u(x in ) + u(x is )] . (3•8)
We now enlarge the model to a scheme with eight nearest neighbours. Each site then has four more neighbours {i nw = i -(1, 1), i ne = i + (-1, 1), i sw = i + (1, -1), i se = i + (1, 1)} (with neighbour adjustments near the boundary). Note that in this case, some cliques have three or four elements but we consider pairwise interactions only, as specified in the condition [B1]. We again assume translation invariance, spatial symmetry, and spatial anisotropy. We wish to model spatial cooperation. Consequently, there exists a vector α = (a, b) and four 2 × 2 matrices β (k) of the form of (3•6) with constants {d k : k = 1, ..., 4} , such that for all i, vectors α i = α, and for all {i, j}, matrices β ij = 0 unless i and j are neighbours, in which case (3•9)

β i,ie = β iw,i = β (1) , β i,in = β is,i = β (2) , β i,inw = β ise,i = β (3) , β i,ine = β isw,i = β (4) .
The conditional distributions are beta-distributed with natural parameters,

A i (x (i) ) = (3•10) a + d 1 [v(x ie ) + v(x iw )] + d 2 [v(x in ) + v(x is )] + d 3 [v(x inw ) + v(x ise )] + d 4 [v(x ine ) + v(x isw )] b + d 1 [u(x ie ) + u(x iw )] + d 2 [u(x in ) + u(x is )] + d 3 [u(x inw ) + u(x ise )] + d 4 [u(x ine ) + u(x isw )]
We propose the method of maximum pseudo-likelihood to estimate the parameters of the multi-parameter auto-models.

Estimation for a multi-parameter auto-model

Parameter estimation for a Markov random field has been well studied. The method of maximum likelihood unfortunately needs computer-intensive approximations, since the likelihood function is known only up to a constant that involves the parameters. As a remedy, [START_REF] Besag | Spatial interactions and the statistical analysis of lattice systems[END_REF][START_REF] Besag | Efficiency of pseudolikelihood estimation for simple Gaussian fields[END_REF] proposed the method of maximum pseudo-likelihood. We refer the reader to [START_REF] Guyon | Random Fields on a Network: Modeling, Statistics, and Applications[END_REF] for an account of theoretical investigations of the properties of maximum pseudo-likelihood estimators. We give below a result for the consistency of the maximum pseudo-likelihood estimator under assumptions of translation invariance, and this is followed by a simulation study to investigate the behaviour of the estimators in finite samples.

4•1 Consistency of the pseudo-likelihood estimator on a lattice

We now introduce specific notation for fields on the two-dimensional lattice Z 2 . The process is observed on a rectangle

Λ n = [-n 1 , n 1 ] × [-n 2 , n 2 ] where n = (n 1 , n 2 ) and n 1 ∧ n 2 → ∞.
As is usual in asymptotic theory, we assume translation invariance: that is, the neighbourhood relationship is defined through a bounded set V 0 of neighbours of the origin (0, 0), such that the set of neighbours of an arbitrary site i ∈ Z 2 is V i = i + V 0 , and the interaction coefficients that appear in the matrices {β ij } are possibly nonzero if and only if j -i = u, for some u ∈ V 0 . Furthermore, translation invariance allows us to write the parameters of the multi-parameter auto-model as:

θ = (α, β u , u ∈ V 0 ) ∈ R q ,
where q denotes the dimension of θ.

For any subset A ∈ Z 2 , write x A = (x i , i ∈ A) as the restriction of x on A. To emphasize the parameters θ, the family of local conditional distributions is written as:

log p(x i |x (i) , θ) = log p(x i |x V i , θ) = A(x V i , θ), B(x i ) + C(x i ) + D(x V i , θ) , (4•1)
where

A(x V i , θ) = α + u∈V 0 β u B(x i+u ) . (4•2)
To give the statement (and the proof) of the result, we need more notation and definitions. We suppose that for each θ, there exists a Gibbs distribution µ θ on E Z 2 such that the conditional distributions 4•1 are those of µ θ . Let the parameter space be

Θ = {θ ∈ R q : E exp [ A(x V 0 , θ), B(x 0 ) + C(x 0 )] dm(x 0 ) < ∞ for all x V 0 ∈ E |V 0 | }, (4•3)
and let θ 0 be the true value of the parameter. Define G s (θ 0 ) to be the set of limiting Gibbs measures on E Z 2 that are translation invariant and compatible with the family of conditional distributions {p(x i |x (i) , θ 0 )}.

Denote

W i = i ∪ V i and define R(x W i , θ) = log[p(x i |x V i ; θ)/p(x i |x V i ; θ 0 )] , i ∈ Λ n , θ ∈ Θ. (4•4)
Then the maximum pseudo-likelihood estimator introduced by [START_REF] Besag | Spatial interactions and the statistical analysis of lattice systems[END_REF][START_REF] Besag | Efficiency of pseudolikelihood estimation for simple Gaussian fields[END_REF] is defined by

θ n = arg min θ∈Θ U n (θ) ,
where

U n (θ) = - 1 |Λ n | i∈Λn R(x W i , θ), θ ∈ Θ. (4•5)
and

|Λ n | = card(Λ n ).
Notice that the computation of θ n does not need the value of θ 0 appeared in (4•4). We now show that θ n is a consistent estimator under mild regularity conditions.

Theorem 2 Assume:

1. The true (limiting) distribution belongs to G s (θ 0 ).

2. For all θ, R(x W 0 , θ) is an integrable random variable in L 1 (µ θ 0 ).

3.

The following identifiability condition holds: for any θ ∈ Θ, if R(x W 0 , θ) = 0 for almost all x W 0 (with respect to µ θ 0 ), then necessarily θ = θ 0 .

Then, the pseudo-likelihood estimator θ n converges to θ 0 almost surely (µ θ 0 ), as

n 1 ∧ n 2 → ∞.
The assumptions made in Theorem 2 are natural. In particular, Assumption 3 ensures that the parametrisation θ → p(x 0 |x V 0 ; θ) is proper. For Assumption 1, as the dependence set V 0 is finite, it is well-known (see [START_REF] Ya | Theory of Phase Transitions: Rigorous Results[END_REF]) that if the state space E is compact and the reference measure m finite, the set G s (θ 0 ) is not empty.

We give an application of this general theorem to the beta auto-models defined in Section 3•2 while assuming translation invariance, spatial symmetry, anisotropy and spatial cooperation. In relation to Equations (3•7) and (3•9), let us define

A 4 = {(a, b, d 1 , d 2 ) : d 1 , d 2 ≤ 0; a ∧ b ≥ -2(log 2)(d 1 + d 2 )}, (4•6)
in the scheme with four nearest neighbours, and

A 8 = {(a, b, d 1 , d 2 , d 3 , d 4 ) : d 1 , . . . , d 4 ≤ 0; a ∧ b ≥ -2(log 2) 4 k=1 d k }, (4•7)
in the eight nearest neighbours system case.

Proposition 3 Consider the auto-beta model of Section 3•2. Assume:

1. The parameter space Θ is a compact subset of A 4 or A 8 accordingly to the associated neighbours system.

2. The (true) limiting distribution µ θ 0 of the observations, defined on E Z 2 , is translation invariant.

3. The following identifiability condition holds: for any θ ∈ Θ, if R(x W 0 , θ) = 0 for almost all x W 0 (with respect to µ θ 0 ), then necessarily θ = θ 0 .

Then, the pseudo-likelihood estimator θ n converges to θ 0 almost surely (µ θ 0 ) as n 1 ∧n 2 → ∞.

4•2 Simulation experiments

We propose several simulation experiments to assess further the properties of the maximum pseudo-likelihood estimator. We consider the auto-models of Section 3•2, where we assumed translation invariance, anisotropy, spatial symmetry and spatial cooperation. Both the eight and the four nearest neighbours systems are examined with various lattice sizes.

For each simulation, we ran a Gibbs sampler on a square lattice, in order to generate a sample from the auto-model (600 sweeps). Empirical estimates are computed from 1600 independent simulations: systematic errors from simulations are then of order 1600 -1 2 = 0.025.

4•2.1 Experiment with the eight nearest neighbours system

First we consider the model with eight nearest neighbours described by (3•9) and (3•10). We choose a set of parameter values that satisfy the integrability conditions (3•9) and allow spatial anisotropy between the four directions: (a, b, d 1 , d 2 , d 3 , d 4 ) = (12, 16, -1, -3, -0.5, -2). The lattice size is 64 × 64. Table 1 gives the bias averages and the standard deviations of the parameter estimates from 1600 independent runs. In this case, the maximum pseudolikelihood method provides consistent estimators with however non-negligible standard deviations especially for small parameter values like

d 1 or d 3 . Parameter a b d 1 d 2 d 3 d 4
True values 12 16 -1 -3 -0.5 -2 Bias average 0.0263 0.0282 0.0018 -0.0117 -0.0077 0.0033 St. deviation 0.3503 0.4775 0.2956 0.2775 0.2457 0.2619 Table 1: Bias averages and standard deviations of the parameter estimates for the beta auto-model with eight nearest neighbours, on a 64×64 lattice, from 1600 independent runs.

4•2.2 Extended experiments with the four nearest neighbours system

Next we consider the model with four nearest neighbours as described in (3•7) and (3•8) with the four parameters (a, b, d 1 , d 2 ). This model appears in [START_REF] Kaiser | Spatial mixture models based on exponential family conditional distributions[END_REF] as a latent process for the analysis of a real data set of diseased trees that involves a spatial hierarchical model. The authors impose the constraint d 1 = d 2 , and propose Monte Carlo maximum likelihood estimation that results in the estimates (a, b, d 1 = d 2 ) = (16.6, 18.9, -4.5). Notice that these values satisfy the integrability condition (3•7). Then we choose these values for our simulation experiments.

Here we are also interested in measuring empirically the convergence rate of the pseudolikelihood estimators. Therefore, simulations are conducted on increasing lattice sizes: n = 8 × 8, 16 × 16, 32 × 32, 48 × 48, 56 × 56, and Next, to get insights on the sampling distributions, we examine Gaussian Q-Q plots of the estimates. Figure 1 below displays such plots for extreme sizes n = 16 2 and n = 64 2 (in the case of the smallest size n = 8 2 , the plot shows a non Gaussian behaviour). For a size as small as n = 16 2 , the plot is not so bad and the empirical distribution is close to a Gaussian distribution. Step by step, the Q-Q plots set right, and we finally get a "perfect" Gaussian approximation for n = 64 2 .

Finally, we examine empirically the convergence rate of the estimates to their respective Gaussian distributions. Based on Table 2 and with the "bad" case n = 8 2 excluded, Figure 2 displays scatter-plots of the logarithms of the standard deviations versus log n. Simple regression fits indicate a slope around -1 2 for all the four parameters, yielding a strong support for a root-n rate of their weak convergence to an asymptotic Gaussian distribution.

Discussion

In this paper we have proposed a directly analogous to Besag's auto-models to the situations where the local conditional distributions belong to some multi-parameter exponential families, such as the beta distribution. This allows one to model spatial cooperation (as well as spatial competition). Another interesting application is the modelling of mixedstate data where the distributions are mixtures of discrete and continuous components. Measurements can present continuous values during some periods and discrete values at other times, such as for daily rainfall time series. At a given site, there may be many zeros when the rain is absent, followed by periods with positive rainfall values [START_REF] Allcroft | A latent Gaussian Markov random-field model for spatiotemporal rainfall disaggregation[END_REF]); then, the state space becomes E = {0} ∪ (0, ∞). Any random variable X taking its values in E is called a mixed-state random variable, which we can define formally as follows: with probability γ ∈ (0, 1), set X = 0, and with probability 1 -γ, X is positive, continuous having a density belonging to a s-dimensional exponential family,

g ξ (x) = H(ξ) exp ξ, T (x) , x > 0, ξ ∈ R s , T (x) ∈ R s .
Let m(dx) = δ 0 (dx) + λ(dx) where δ 0 and λ are respectively the Dirac measure at 0 and the Lebesgue measure on (0, ∞). Define the indicator function δ(x) = I {0} (x) and set δ * (x) = 1 -δ(x), x ≥ 0. Then X has then the following density function (with respect to m(dx)):

f θ (x) = γδ(x) + (1 -γ)δ * (x)g ξ (x) = Z -1 (θ) exp θ, B(x) , x ≥ 0,
where we have set

θ = (θ 1 , θ 2 ) T = log (1 -γ)H(ξ) γ , ξ T , B(x) = (δ * (x), T (x) T ) T .
In other words, X belongs to a (s + 1)-dimensional exponential family. When this formulation is applied to the conditional distributions on a lattice, we obtain a multi-parameter auto-model suitable for modelling data that are either zero or positive-valued. Theoretical results for these specific mixed-state auto-models will be studied elsewhere. Experimental application to motion measurements in video sequences can be found in [START_REF] Bouthemy | Mixed-State auto-models and motion texture modelling[END_REF]).

On the other hand, the auto-model scheme will gather more power in applications if the assumed pairwise interactions are extended to more general multiway dependence. Another important question is to relax the positivity condition as proposed by [START_REF] Kaiser | The construction of multivariate distributions from Markov random fields[END_REF] in a general context. Finally, the simulations of Section 4 indicate that the maximum pseudo-likelihood estimators of the auto-models' parameters should be asymptotically normally distributed with a root-n convergence rate. It is clearly worth investigating theoretical studies to support such empirical evidence.

Proofs

Proof of Theorem 1

For each i, we have:

Q(x) -Q(τ i x) = G i (x i ) + j: j =i G ij (x i , x j ) = log p i (x i |x (i) ) p i (τ i |x (i) ) = A i (x (i) ), B i (x i ) + C i (x i ) .
By taking x (i) = τ (i) = {τ j : j = i}, we obtain:

G i (x i ) = A i (τ (i) ), B i (x i ) + C i (x i ) . (6•1)
Now, let us fix two indices i = j. For ease of exposition and without loss of generality, we may assume i = 1 and j = 2. The previous calculations also lead to Q(x 1 , x 2 , τ 3 , . . . , τ n ) -Q(τ 1 , x 2 , τ 3 , . . . , τ n ) = G 1 (x 1 ) + G 12 (x 1 , x 2 ) = A 1 (x 2 , τ 3 , . . . , τ n ), B 1 (x 1 ) + C 1 (x 1 ) .

Therefore, G 12 (x 1 , x 2 ) = A 1 (x 2 ), B 1 (x 1 ) ,

where we have set A 1 (x 2 ) = A 1 (x 2 , τ 3 , . . . , τ n ) -A 1 (τ 2 , τ 3 , . . . , τ n ) .

In an analogous manner and switching the indices 1 and 2, we finally obtain for all x 1 , x 2 ∈ E, G 12 (x 1 , x 2 ) = A 1 (x 2 ), B 1 (x 1 ) = G 21 (x 2 , x 1 ) = A 2 (x 1 ), B 2 (x 2 ) ; that is,

B T 1 (x 1 )A 1 (x 2 ) = A T 2 (x 1 )B 2 (x 2 ) , (6•2)
where A 2 (x 1 ) = A 2 (x 1 , τ 3 , . . . , τ n ) -A 2 (τ 1 , τ 3 , . . . , τ n ) .

Next, Condition [C] for i = 2 means that there exist l elements of E, Y = {y 1 , ..., y l }, such that the l×l matrix B 2 (Y) = (B 2 (y 1 ), . . . , B 2 (y l )) is invertible. We also write A 1 (Y) = (A 1 (y 1 ), . . . , A 1 (y l )). Then, upon substituting x 2 = y j , for j = 1, . . . , l, into (6•2) , A T 2 (x 1 )B 2 (Y) = [A T 2 (x 1 )B 2 (y 1 ), . . . , A T 2 (x 1 )B 2 (y l )] = [B T 1 (x 1 )A 1 (y 1 ), . . . , B T 1 (x 1 )A 1 (y l )] = B T 1 (x 1 )A 1 (Y).

Therefore,

A T 2 (x 1 ) = B T 1 (x 1 )β 12 (Y) , where β 12 (Y) = A 1 (Y)[B 2 (Y)] -1 .
Consequently, G 12 can be written as

G 12 (x 1 , x 2 ) = B T 1 (x 1 )β 12 (Y)B 2 (x 2 ) .
The left hand side of this equality does not depend on Y, so β 12 (Y) ≡ β 12 is a constant matrix and we obtain, G 12 (x 1 , x 2 ) = B T 1 (x 1 )β 12 B 2 (x 2 ) . (6•3)

By exchanging the indices, we also have G 21 (x 2 , x 1 ) = B T 2 (x 2 )β 21 B 1 (x 1 ). As G 12 (x 1 , x 2 ) = G 21 (x 2 , x 1 ), for all x 1 , x 2 , we must have β 12 = β T 21 . Furthermore, Q(x) -Q(τ 1 x) = G 1 (x 1 ) + j =1 G 1j (x 1 , x j ). We use eqs. (6•1) and ( 6•3) in this expression and obtain, A T 1 (τ (1) )B 1 (x 1 ) + C 1 (x 1 ) + j =1

B T 1 (x 1 )β 1j B j (x j ) = A T 1 (x (1) )B 1 (x 1 ) + C 1 (x 1 ), which is equivalent to

α T 1 B 1 (x 1 ) + j =1
B T j (x j )β j1 B 1 (x 1 ) = A T 1 (x (1) )B 1 (x 1 ) .

That is,

α 1 + j =1 β 1j B j (x j ) -A 1 (x (1) ) T B 1 (x 1 ) = 0.
Hence, applying Condition [C] in the same manner as above, we obtain Equation (2•3) for i = 1.

Proof of Proposition 1

We have only to check that the conditional distributions of the field with potentials (2•4) and (2•5) are those given by [B2] and (2•3). This follows from:

Q(x) -Q(τ i x) = G i (x i ) + j:j =i G ij (x i , x j ) = α i , B i (x i ) + C i (x i ) + j =i B T i (x i )β ij B j (x j ) = A i (x (i) ), B i (x i ) + C i (x i ) = log p i (x i |x (i) ) p i (τ i |x (i) )
.

  The model involves 6 parameters (a, b, d 1 , d 2 , d 3 , d 4 ). The integrability conditions (3•4) and (3•5) become d 1 , . . . , d 4 ≤ 0 ; (1 + a) ∧ (1 + b) > -2(log 2)

Figure 1 :Figure 2 :

 12 Figure 1: Gaussian Q-Q plots of the estimates from 1600 independent runs. a). Lattice size n = 16 2 . b). Lattice size n = 64 2 .

Table 2 :

 2 64 × 64. Average bias and standard deviations of the estimates are displayed in Table2. We can see that the bias are quite large in the case of the smallest lattice size n = 8 2 and significantly reduced when n = 64 2 . Bias averages and standard deviations of the parameter estimates for the beta auto-model with four nearest neighbours, various lattice sizes and from 1600 independent runs in each case.

	Parameter	a	b	d 1	d 2
	True values	16.6	18.9	-4.5	-4.5
	8*8	Bias average 2.1640 4.5885 -0.4970 -0.0491
		St. deviation 6.6384 7.6895 3.8361 3.4149
	16*16	Bias average 0.3574 0.8581 -0.0434 -0.0510
		St. deviation 2.3882 2.3416 1.3288 1.3376
	32*32	Bias average 0.0260 0.2171 0.0273 -0.0066
		St. deviation 1.1393 1.1719 0.6372 0.6219
	48*48	Bias average 0.0261 0.0852 -0.0210 0.0166
		St. deviation 0.7267 0.7263 0.4130 0.4359
	56*56	Bias average 0.0319 0.0365 -0.0140 -0.0027
		St. deviation 0.6466 0.6547 0.3693 0.3619
	64*64	Bias average 0.0307 0.0357 -0.0069 -0.0085
		St. deviation 0.5554 0.5713 0.3031 0.3179

Acknowledgement. This work originated from several discussions with Xavier Guyon. The authors are also grateful to a referee whose detailed comments have lead to several improvements of the manuscript.

Proof of Proposition 2

We need only to prove the admissibility of Q. Let ξ = (1, 1) T and w(x) = B(x)-(log 2)ξ = (log x, log(1 -x)) T . We have

For all i = j, since w T (x i )β ij w(x j ) ≤ 0 and ξ T β ij ξ ≤ 0, we have

where R n is a constant, depending only on the parameters α i . Therefore, up to a constant factor, e Q is bounded above by a product of n independent beta densities that are well defined, since from (3•4) and (3•5), the exponents of the factors x i and (1 -x i ) are all greater than -1. Hence e Q is integrable over (0, 1) n .

Proof of Theorem 2

Since the A(x V i , θ)'s are linear functions of the parameters in θ, and e x is a convex function, the parameter space Θ is a convex set in R q . Moreover, it is not difficult to see that this linear dependence also implies that the Hessian matrix of U n (θ) is everywhere nonnegativedefinite. Hence U n is a convex function of θ.

In the case of a translation-invariant specification, the extremal elements of G s (θ 0 ) coincide with the stationary ergodic Gibbs measures. Moreover, every element of G s (θ 0 ) is a convex combination of its ergodic (extremal) elements [START_REF] Ya | Theory of Phase Transitions: Rigorous Results[END_REF]): consider a probability measure w defined on the set G * s (θ 0 ) of ergodic elements of G s (θ 0 ), then we have

Define the convergence set of the pseudo-likelihood estimator

If for all ergodic elements ν it holds that ν(A) = 1, we clearly have µ θ 0 (A) = 1. Therefore, without any loss of generality, we can focus on proving the result for µ θ 0 ergodic. Next, by Assumption 1 and the ergodic theorem, the following limit exists almost-surely (µ θ 0 ),

Moreover,

where D KL (P, Q) = log(P/Q)dP is the Kullback-Leibler divergence . Furthermore, K(θ) = 0 if and only if θ = θ 0 under Assumption 3 of the Theorem.

Therefore, standard arguments for convex estimating functions imply that the estimator θ n is strongly consistent (see [START_REF] Senoussi | Statistique asymptotique presque-sûre de modèles statistiques convexes[END_REF], or Guyon (1995) Theorem 3.4.4).

Proof of Proposition 3

We need only to check condition 2 of Theorem 2. Note that the parameter sets A 4 and A 8 are subsets of those defined in Equations (3•7) and (3•9), respectively. The advantage here is that for any θ ∈ A 4 (or A 8 ), the parameters A(x V i , θ) of the local beta conditional distributions are nonnegative, componentwisely. Consequently, the local contrast function {R(x W 0 , θ)} is a continuous function on the compact set [0, 1] |W 0 | × Θ (previously it could be discontinuous at the boundary 0 and 1). It follows that R is bounded, thus integrable. The conclusion follows.


Paul Brunet
email: paul@brunet-zamansky.fr

Reversible Kleene Lattices

Keywords: F.1.1 Models of Computation, F.3.2 Semantics of Programming Languages Kleene algebra, Automata, Petri nets, Decidability, Complexity. Digital Object Identifier 10.4230/LIPIcs

We investigate the equational theory of reversible Kleene lattices, that is algebras of languages with the regular operations (union, composition and Kleene star), together with the intersection and mirror image. Building on results by Andréka, Mikulás and Németi from 2011, we construct the free representation of this algebra. We then provide an automaton model to compare representations. These automata are adapted from Petri automata, which we introduced with Pous in 2015 to tackle a similar problem for algebras of binary relations. This allows us to show that testing the validity of equations in this algebra is decidable, and in fact ExpSpace-complete.

Introduction

We are interested in algebras of languages, equipped with the constants empty language (0), unit language (1, the language containing only the empty word), the binary operations of union (+), intersection (∩), and concatenation (•), and the unary operations of Kleene star (_ ) and mirror image, also called converse, (_ N ). We call these algebras reversible Kleene lattices. Given a finite set of variables X, and two terms e, f built from variables and the above operations, we say that the equation e = f (respectively inequation e ≤ f ) is valid if the corresponding equality (resp. containment) holds universally. A free representation is a set M together with a map h from terms to elements of M such that e = f is valid if and only if h maps e and f to the same element of M.

It is well known that to any term over this syntax, one can associate a regular language, and that comparing regular languages is decidable. In fact, the problem of comparing regular expressions with intersection with respect to regular language equivalence is ExpSpacecomplete [START_REF] Fürer | The complexity of the inequivalence problem for regular expressions with intersection[END_REF]. The difference with the work presented here is that we are considering equations which are stable under substitution. Formally, this means that we do not interpret the letter a as the singleton language {a}, but rather as a universally quantified variable ranging over all languages. What is remarkable however is that testing the validity of equations in reversible Kleene lattices is still an ExpSpace-complete problem, as we show in this paper. Several fragments of this algebra have been studied: Kleene algebra (KA) [START_REF] Conway | Regular algebra and finite machines[END_REF]: if we restricts ourselves to the operators of regular expressions (0, 1, +, •, and _ ), then the free representation is the set of regular languages, with the usual definition of the language of an expression. Testing the validity of equations in KA is thus a PSpace-complete problem [START_REF] Meyer | The equivalence problem for regular expressions with squaring requires exponential space[END_REF][START_REF] Stephen | Representation of Events in Nerve Nets and Finite Automata[END_REF]. Kleene algebra with converse (KAC) [START_REF] Stephen | Notes on equational theories of relations[END_REF]: if we add to KA the converse operation, then the free representation consists of regular expressions over a duplicated alphabet, with a letter a denoting the converse of the letter a. The associated decision problem is still in PSpace. Identity-free Kleene lattices (KL -) [START_REF] Andréka | The equational theory of Kleene lattices[END_REF]: this algebra stems from the operators 0, +, •, ∩ and _ + , where the latter is the non-zero iteration. Andréka Mikulás and Németi studied this fragment, and showed that the free representation of this algebra consists of languages of series-parallel graphs, downward closed with respect to some graph preorder. We reformulated their results with Pous [START_REF] Brunet | Petri Automata for Kleene Allegories[END_REF], and introduced a new class of automata, called Petri automata, able to recognise these languages of graphs. In [START_REF] Brunet | Petri Automata for Kleene Allegories[END_REF] we provided a decision procedure to compare these automata, thus yielding an ExpSpace decision procedure for the equational theory of this algebra. It is in fact ExpSpace-complete, thanks to some simple adaptation of a result by Fürer [START_REF] Fürer | The complexity of the inequivalence problem for regular expressions with intersection[END_REF].

The present work is then an extension of identity-free Kleene lattices, by adding unit and mirror image. The addition of mirror image is fairly simple, relying mainly on ideas from [START_REF] Stephen | Notes on equational theories of relations[END_REF]. However, the seemingly small addition of 1 yields some complications. In fact, in [START_REF] Andréka | The equational theory of Kleene lattices[END_REF][START_REF] Brunet | Petri Automata for Kleene Allegories[END_REF] there is a free representation of Kleene allegories, an algebra over the same signature as reversible Kleene lattices, but whose intended model is binary relations rather than languages. In this context, adding 1 means moving from series-parallel graphs to graphs of tree-width 2, which might have cycles. This is a significant problem for automata based decision procedures.

In the context of languages, adding 1 yields other problems. However, the free representation we get for reversible Kleene lattices remains more tractable than that of Kleene allegories. In particular we do not create cycles in series parallel graphs, but rather have to collect additional information. Let us illustrate the kind of reasoning we develop to study these algebras with the following inequation:

c • (1 ∩ a) ≤ a • c.
(

On the left hand side (LHS), the term 1 ∩ a appears. This term is either equal to 1 if the empty word belongs to language a, or 0 otherwise. In the first case, the LHS is equal to c and we have 1 ≤ a, meaning that c = 1 • c ≤ a • c. In the second case the LHS is equal to 0, which is contained in a • c as well. The key observation here is that the second case does not really matter: in a term build out of concatenations, intersections, converse, variables and units, if 0 appears somewhere then the term will always evaluate to 0 and thus be contained in any other term. The free representations we develop for union-free terms consist of pairs of a representation of a 1-free term and a set of language variables which are assumed to contain the empty word. This allows us to make the reasoning we used to study (1) automatic. Following an approach similar to [START_REF] Brunet | Petri Automata for Kleene Allegories[END_REF], we construct in Section 2 the free representation of reversible Kleene lattices, and introducing a new Petri net-based automata model we show in Section 3 that testing the validity of equations is a decidable problem, and in fact an ExpSpace-complete one. We conclude and list some perspectives in Section 4.

Basic definitions and notations

For a pair p = x, y , we denote by π 1 (p) = x the first projection, and by π 2 (p) = y the second projection. The set of functions from a set A to a set B is written A → B, and the set of partial functions from A to B is written A B. The number of elements of a finite set A is written |A|. The empty word is denoted by ε, and the set of words over the alphabet Σ is Σ . If w = x 1 . . . x n is a word of length n, w[i, j] is the word x i . . . x j if i j, and undefined otherwise. If f is a function from some set X to {0, . . . , n}, x, y are elements of X, and if f (x) f (y), we use the notation Let X be a finite set of variables, we define Ȧ := A ∪ {a N | a ∈ A} for every subset A ⊆ X. The set Ẋ is called the duplicated alphabet, we let α, β range over Ẋ. Expressions over X are given by the following grammar:

w f [x, y] for the word w[f (x) , f (y)]. G (a) := a G (a • b) := a b G ((a • b) ∩ c) := a b c G (a • (b ∩ c)) := a b c
e, f ::= 0 | 1 | x | e N | e + f | e • f | e ∩ f | e . (x ∈ X)
The set of expressions over X is written E X . The size of an expression e, written |e|, is its number of symbols, i.e. the number of vertices in its syntax tree. Most of the time, we will implicitly assume that the converse operator only appears as x N , with x ∈ X. This is not restrictive, as every expression can be transformed linearly such that this property holds. Given a second alphabet Σ, an interpretation is a map σ : X → P (Σ ) which associates to every variable a a language σ (a). This map can be uniquely extended to a homomorphism σ : E X → P (Σ ) defined inductively:

σ (0) = ∅ σ (1) = {ε} σ (a) = σ (a) σ (e N ) = σ (e) N = {x n . . . x 1 | x 1 . . . x n ∈ σ (e)} σ (e + f ) = σ (e) ∪ σ (f ) σ (e • f ) = σ (e) • σ (f ) σ (e ∩ f ) = σ (e) ∩ σ (f ) σ (e ) = σ (e) = {w 1 . . . w n | w i ∈ σ (e)} .
We say that e = f (respectively e ≤ f ) is valid, and write Lang |= e = f (resp. Lang |= e ≤ f ), when for every interpretation σ, we have σ (e) = σ (f ) (resp. σ (e) ⊆ σ (f )).

It is interesting to note that as decision problems, the validity of equations and that of inequations are equivalent. Indeed, the following equivalences hold:

Lang |= e = f ⇔ Lang |= e ≤ f ∧ Lang |= f ≤ e Lang |= e ≤ f ⇔ Lang |= e + f = f.

2

The free representation of reversible Kleene lattices

Intuitions

First introduced in the context of relation algebra [START_REF] Andréka | The equational theory of union-free algebras of relations[END_REF][START_REF] Freyd | Categories, Allegories[END_REF], directed labelled 2-pointed graphs can be used to describe the algebra of languages over the signature •, ∩ . First, we associate to every term u over this signature such a graph G (u). See Figure 1 for examples. The set of such graphs is equipped with a preorder: G is smaller than H if there is a graph homomorphism from H to G. Such a homomorphism is illustrated in Figure 2, with dotted arrows. Already, this gives us a clue as to the (in)equational theory: the inequation u ≤ v is valid if and only if G (u) is smaller than G (v). Moving to identity-free Kleene lattices, i.e. to the signature 0, +, •, ∩, _ + , we associate to every term e a set G (e) of such graphs, and then take its downward closure G (e) ↓ with respect to the preorder. This yields the free representation of this algebra: the equation e = f is valid if and only if G (e) ↓ = G (f ) ↓.

To move from identity free Kleene lattices to reversible Kleene lattices, two steps are necessary: we need to add the converse, and to add the constant 1. The first step is somewhat straightforward, thanks to results by Ésik et al. [START_REF] Stephen | Notes on equational theories of relations[END_REF]: they showed that the free representation of the algebra of languages with the regular operations together with converse is simply the set of regular languages over a duplicated alphabet, where we add for every letter a new letter representing its converse. This approach works well in our setting, by considering graphs labelled with the duplicated alphabet.

For the second step, we draw our inspiration from Lemma 3.4 in [START_REF] Andréka | The equational theory of Kleene lattices[END_REF], that established that every term in E X is equivalent to a finite sum of terms of the form (1 ∩ a ∩ b . . .) • e, where a, b, • • • ∈ X are letters, and 1 does not appear in e. For every interpretation σ : X → P (Σ ), if there is some variable x ∈ {a, b, . . . } such that ε / ∈ σ (x), then the interpretation of 1 ∩ a ∩ b ∩ . . . is ∅. Otherwise, if the empty word is in the interpretation of each of the a, b, . . . , then the interpretation is {ε}. If we now look at the interpretation of the whole term, this means that:

σ ((1 ∩ a ∩ b ∩ . . .) • e) = ® σ (e) if ∀x ∈ {a, b, . . . } , ε ∈ σ (x) ; ∅ otherwise.
Consider now an inequation f 1 ≤ f 2 , where

f i = (1 ∩ a i,1 ∩ • • • ∩ a i,ni ) • e i for i ∈ {1, 2}. If there exists a variable x ∈ {a 2,1 , . . . , a 2,n2 } \ {a 1,1 , . . . , a 1,n1 }, we can build an interpretation σ such that (1) ε / ∈ σ (x) and (2) σ (f 1 ) = ∅.
The first condition ensures that the image of f 2 will be ∅, hence the inequation is not valid. Thus for the inequation to be valid, we need that {a 2,1 , . . . , a 2,n2 } ⊆ {a 1,1 , . . . , a 1,n1 }. Furthermore, for every σ such that there is an a 1,i whose interpretation does not contain the empty word, the image of f 1 will be ∅, which is trivially contained in the image of the f 2 . We reach the following equivalence: 2) for every interpretation σ such that the empty word is in the interpretation of every a 1,j , we have σ (e 1 ) ⊆ σ (e 2 ). This means that we need to compare 1-free expressions under the assumption that certain variables contain the empty word. This is the intuitions behind what we call weak graphs. Weak graphs are pairs of a graph and a set of test variables. They are equipped with a preorder relation , which relates G, A and H, B if B ⊆ A and there is a map ϕ from H to G such that every edge labelled outside of A is preserved, but edges labelled with tests in A are either preserved or contracted. Such a map is shown in Figure 3.

f 1 ≤ f 2 is valid if and only if (1) {a 2,1 , . . . , a 2,n2 } ⊆ {a 1,1 , . . . , a 1,n1 } and (
We then have theorems similar to those for identity free Kleene lattices and series parallel graphs, in the sense that for every pair of terms u, v over the syntax •, ∩, 1, _ N , if we denote by WG (u) , WG (v) their associated weak graphs, u ≤ v is valid if and only if P. Brunet XX:5 WG (u) WG (v). Furthermore, if we associate to every expression e in E X a downwards closed set of weak graphs e , the equation e = f is valid if and only if e = f .

Weak terms

We define the following two sets of terms over the alphabet X:

Ground terms: u, v ∈ GT X ::= 1 | a | a N | u • v | u ∩ v. Simple ground terms: u, v ∈ GT -X ::= a | a N | u • v | u ∩ v.
We call the variables of the term u, and write var (u), the set of variables a ∈ X such that a or a N appears in u. We call weak terms the elements of the set (GT -X ∪ {1}) × P (X), that is simple ground terms or 1 indexed with a set of test variables. The set of weak terms is written W T X . This set is equipped with two products, denoted by • and , defined as follows:

1 A • 1 B := 1 A∪B 1 A • u B = u A • 1 B := u A∪B u A • v B := (u • v) A∪B 1 A 1 B := 1 A∪B 1 A u B = u A 1 B := 1 A∪B∪var (u) u A v B := (u ∩ v) A∪B .
Given an interpretation σ :

X → P (Σ ), the interpretation σ (u A ) of the weak term u A is either ∅ if ∃a ∈ A : ε / ∈ σ (a)
, or σ (u) otherwise. We define a translation τ from ground terms to weak terms:

τ (u • v) := τ (u) • τ (v) τ (u ∩ v) := τ (u) τ (v) ∀u ∈ {1} ∪ Ẋ, τ (u) := u ∅ .
This translation is faithful, in the sense that the following holds:

Lemma 1. ∀u ∈ GT X , ∀σ : X → P (Σ ) , σ (u) = σ • τ (u) .
Proof (Sketch). The proof relies on the fact that for every pair of weak terms x, y we have:

σ (x • y) = σ (x) • σ (y) σ (x y) = σ (x) ∩ σ (y) .
We then conclude by a simple induction on u. For concision, the full proof is omitted here.

We can also define a converse translation κ : W T X → GT X which associate to a weak term u {a1,...,an} the ground term (1

∩ a 1 ∩ • • • ∩ a n ) • u.
It is immediate to check that for every term x ∈ W T X and every interpretation σ we have σ (x) = σ • κ (x).

Weak graphs

A graph G in our setting is a tuple V G , E G , i G , o G , where V G is a finite set of vertices, E G ⊆ V G × Ẋ × V G
is a set of labelled and directed edges, and i G , o G ∈ V G are two vertices, called the input and output of the graph. Term graphs must further be series parallel [START_REF] Valdes | The recognition of series parallel digraphs[END_REF], i G must be the unique source vertex (i.e. with no incoming edge), and o G the unique sink vertex (i.e. with no outgoing edge). We let G, H range over graphs. Term graphs can be sequentially composed, by identifying the output of the first graph with the input of the second one, or composed in parallel, by identifying the inputs of both graphs and identifying theirs outputs. These two compositions are respectively denoted by ; and |. The set l (G) of labels of a graph G is defined as the set of letters a ∈ X such that there is an edge in E G labelled with either a or a N .

The graph of a simple ground term u, written G (u), is a term graph defined inductively:

G (α) := α G (u • v) := G (u) ; G (v) G (u ∩ v) := G (u) | G (v) .
We define the graph 1 as . Notice that it is not a term graph, as it is not series parallel. We call weak graph a pair whose left part is either a term graph or 1, and whose right part is a set of test variables. We denote the weak graph G, A by G A . For every weak term x we associate a weak graph WG (x) as one would expect:

WG (1 A ) := 1 A WG (u A ) := G (u) A .
The weak graph G A is smaller than H B , written G A H B , if B ⊆ A and there exists a function ϕ :

V H → V G such that ϕ (i H ) = i G , ϕ (o H ) = o G ,
and for every edge x, α, y in E H , either ϕ (x) , α, ϕ (y) ∈ E G or α ∈ Ȧ and ϕ (x) = ϕ (y). The relation is a preorder. We will show in the next section that for any two ground terms u and v, the following holds:

Lang |= u ≤ v ⇔ WG (τ (u)) WG (τ (v)) .
The first important lemma is the following. It generalises [1, Lemma 2.5] by including 1 and _ N , thus moving from series parallel graphs to weak graphs. Lemma 2. ∀u ∈ W T X , there exists a word w u and an interpretation σ u such that for every

v ∈ W T X , w u ∈ σu (v) ⇔ WG (u) WG (v). Proof. Let WG (u) = V u , E u , i u , o u , A . Let µ : V u → {1, . . . , |V u |} be a bijective map such that x, α, y ∈ E u ⇒ µ (x) < µ (y) 1 . In particular, µ (i u ) = 1 and µ (o u ) = |V u |. Let n = 2 × (|V u | -1)
, and Σ u an alphabet composed of n distinct letters x 1 , . . . , x n .

We define w u = x 1 x 2 . . . x n , and f :

V u → {0, . . . , n} such that f (x) = 2 (µ (x) -1). Notice that f (i u ) = 0 and f (o u ) = n. We now define σ u : σ u (a) :=    w f u [x, y] x, a, y ∈ E u ∪ ¶ w f u [x, y] N x, a N , y ∈ E u © ∪ {ε} if a ∈ A w f u [x, y] x, a, y ∈ E u ∪ ¶ w f u [x, y] N x, a N , y ∈ E u © if a / ∈ A Notice that for every α ∈ Ẋ, ε ∈ σ u (α) ⇔ α ∈ Ȧ, and that if x = y then w f u [x, y] ∈ σ u (α) if and only if x, α, y ∈ E u . Let v = t B ∈ W T X .
First, suppose that ∃a ∈ B \ A. We know that ε / ∈ σ u (a), meaning that σu (v) = ∅. We also know by definition of that WG (u) WG (v). Thus the equivalence holds, as both sides are false. In the following, we thus assume that B ⊆ A.

If t = 1, then σu (v) = {ε}. This means that w u ∈ σu (v) if and only if w u = ε. By definition, this is equivalent to n = 0, which is again equivalent to |V u | = 1 thus to u = 1 A . It is not hard to check that the only graph G such that G A 1 B is 1 itself, thus proving the desired equivalence.

The other case is when t is a simple ground term. Then an induction much like in the proof of [1, Lemma 2.5] allows to conclude. We omit this part of the proof here.

The other important lemma is a generalisation of [1, Lemma 2.3]. It will allow us to factor any interpretation of u through the weak graph WG (u). Lemma 3. For every simple ground term u, every interpretation σ : X → P (Σ ), and every word w ∈ Σ of length n:

w ∈ σ (u) ⇔ ∃ϕ : V u → {0, . . . , n} : ® ϕ (i u ) = 0 ∧ ϕ (o u ) = n x, α, y ∈ E u ⇒ w ϕ [x, y] ∈ σ (α) .
It can be proved by a simple induction on u; for concision, we omit this proof.

1 Remember that both term graphs and 1 are directed acyclic graphs.

P. Brunet

XX:7

Freeness results

We can now establish our first freeness result:

Theorem 4. ∀x, y ∈ GT X , WG (τ (x)) WG (τ (y)) ⇔ Lang |= x ≤ y.
Proof. The statement of the theorem is equivalent to the following, thanks in part to Lemma 1: ∀x, y ∈ W T X , WG (x) WG (y) ⇔ ∀Σ, ∀σ : X → P (Σ ) , σ (x) ⊆ σ (y). We let x = u A and y = v B , and proceed to prove both implications. Suppose WG (x) WG (y), let σ be an interpretation, and w a word of length n. The case of 1 being trivial, we consider here the case where both u and v are simple ground terms. Assume w ∈ σ (x), then we need to prove that w ∈ σ (y). First notice that because σ (x) = ∅ it must be the case that ∀a ∈ A, ε ∈ σ (a). By Lemma 3, we have a function

ϕ : V u → {0, . . . , n} such that ϕ (i u ) = 0, ϕ (o u ) = n, and x, α, y ∈ E u ⇒ w ϕ [x, y] ∈ σ (α).
By definition of , we also have a function ψ :

V v → V u such that ψ (i v ) = i u , ψ (o v ) = o u , and for every edge x, α, y in E v , either ψ (x) , α, ψ (y) ∈ E u or α ∈ Ȧ and ψ (x) = ψ (y). We define Φ = ϕ • ψ. Now we may check that Φ (i v ) = ϕ (i u ) = 0; Φ (o v ) = ϕ (o v ) = n; and if x, α, y ∈ E v , then either ψ (x) , α, ψ (y) ∈ E u , which means w Φ [x, y] = w ϕ [ψ (x) , ψ (y)] ∈ σ (α);
or α ∈ Ȧ and ψ (x) = ψ (y), which entails w Φ [x, y] = ε ∈ σ (α). Using Lemma 3 again, we get that w ∈ σ (v). Because B ⊆ A, we also have that σ (y) = σ (v). Hence σ (x) ⊆ σ (y).

For the converse, we now assume that WG (x) WG (y). Using Lemma 2, we know that w x ∈ σx (x) and that w x / ∈ σx (y). This proves that σx (x) ⊆ σx (y).

We define the set of weak terms e of an expression e by structural induction:

0 := ∅ 1 := {1 ∅ } α := {α ∅ } e + f := e ∪ f e • f := {u • v | u ∈ e ∧ v ∈ f } e ∩ f := {u v | u ∈ e ∧ v ∈ f } e := {u 1 • • • • • u n | n 0 ∧ ∀0 i n, u i ∈ e }
The downward closure S of a set of weak terms S is the set of weak terms x such that there exists a weak term y ∈ S satisfying WG (x) WG (y). The function is a closure operator. The set of downward closed sets of weak terms is the free representation of reversible Kleene lattices:

Theorem 5. ∀e, f ∈ E X : e ⊆ f ⇔ Lang |= e ≤ f .
Proof. We use the fact that for every interpretation σ,

σ (e) = u∈ e σ (u) = u∈ e σ (u) .
This can be proved using [1, Lemma 2.1], and Lemmas 1 and 2 and Theorem 4. Suppose e ⊆ f , and let σ be an interpretation.

σ (e) = u∈ e σ (u) ⊆ u∈ f σ (u) = σ (f ) .
For the converse, suppose e ⊆ f . Because is a closure operator, this means e ⊆ f . Let u ∈ e \ f . By Lemma 2, we have w u ∈ σu (u) ⊆ σ u (e), but because u / ∈ f , for every v ∈ f , we have WG (u) WG (v) thus w u / ∈ σu (v). Hence w u is not in the set v∈ f σu (v) = σ u (f ).

Decidability and complexity

To decide the equational theory of identity-free Kleene lattices, we used Petri automata [START_REF] Brunet | Petri Automata for Kleene Allegories[END_REF]. This was a new style of automaton, which was designed to recognise sets of series parallel graphs. We modify this model slightly to recognise weak graphs, provide a construction to build automata out of expressions, and an algorithm to decide language containment (up-to closure by ) for these automata. This algorithm itself is inspired by the simulation algorithm for simple Petri automata. We conclude this section by showing that the problem is complete of the class ExpSpace.

Weak Petri automata

A weak Petri automaton is a Petri automaton [START_REF] Brunet | Petri Automata for Kleene Allegories[END_REF][START_REF] Brunet | Algebras of Relations: From algorithms to formal proofs[END_REF] whose transitions are labelled with sets of letters2 . Formally, an automaton A over the finite alphabet X is a triple P, T, ι where P is a finite set of places, ι ∈ P is the initial place, and T ⊆ P (P ) × P (X) × P Ẋ × P is a set of transitions. Each transition t ∈ T is composed of three parts: its input ▹ t ⊆ P , its set of tests Ê t ⊆ X, and its output t ▹ ⊆ Ẋ × P . It will also be useful to write π 2 (t ▹ ) for the set of output places of t, i.e. p ∈ P ∃α ∈ Ẋ : α, p ∈ t ▹ . The transition t is called final if t ▹ = ∅, and initial if ▹ t = {ι}. We will add a few constraints on this definition along the way, but we need more definitions to state them. An example of such an automaton is depicted in Figure 4. The graphical representation used here draws round vertices for places and rectangular vertices for transitions, with the incoming and outgoing arcs to and from the transition corresponding respectively to the inputs and outputs of said transition. The set of tests of a transition is written inside the rectangle. The initial place is denoted by an unmarked incoming arc.

Runs and reachable states.

We define the operational semantics of weak Petri automata. Let us fix for the remainder of this section an automaton A = P, T, ι . A state of this automaton is a set of places. In a given state S ∈ P (P ), a transition t is enabled if ▹ t ⊆ S. In this case, we may P. Brunet XX:9 fire t, leading to a new state S = (S \ ▹ t) ∪ π 2 (t ▹ ). This will be denoted in the following by S t --→ A S . We extend this notation to sequences of transitions in the natural way: if S 0 t 1 --→ A S 1 and S 1 t 2 ;...;t n ------→ A S n then we write S 0 t 1 ;t 2 ;...;t n -------→ A S n . In this case we say that S 0 , t 1 ; t 2 ; . . . ; t n , S n is a valid run, or simply run, from S 0 to S n . If S 0 = {ι} then the run is initial and if S n is empty then it is final. A run which is both initial and final is called accepting. An accepting run of the automaton from Figure 4 is depicted in Figure 5. A state S is reachable in A if there is an initial run leading to S.

We may now state the first two constraints we impose on automata: if S is reachable in A and S t --→ A S , then (S \ ▹ t) ∩ π 2 (t ▹ ) = ∅, and for each transition t ∈ T , and every triple p, α, β ∈ P × Ẋ × Ẋ, we have: { α, p , β, p } ⊆ t ▹ ⇒ α = β. These constraints correspond to the classic Petri net property of safety, also called one-boundedness.

Remark. These constraints are decidable: the set of transitions is finite, and because reachable states are subsets of a fixed finite set, there are only finitely many. Thus checking whether an automaton satisfies these two requirements only entails a finite number of tests.

We introduce some attributes of a run R:

its input I R , its output O R , its excess E R , its tests A R , and its internal labels Λ R . Let R = S 0 t 1 --→ A S 1 . . . t n
--→ A S n be a valid run in some automaton A. I R is the set of tokens (places) in S 0 which are consumed during the run; E R is the rest of the tokens from S 0 , those which are not moved; Λ R is the set of labels appearing in some t ▹ i such that the associated token is consumed later on; A R is the union of the sets of tests of R's transitions; and O R is the set of outputs which are not consumed in the remainder of the run. Formally:

I R := {p ∈ S 0 | ∃i : p ∈ ▹ t i } O R := ¶ α, p ∃i : α, p ∈ t ▹ i ∧ Ä ∀j > i, p / ∈ ▹ t j ä© A R := i Ê t i E R := S 0 \ I R Λ R := ¶ α ∃p, ∃i < j : α, p ∈ t ▹ i ∧ p ∈ ▹ t j © .
In the example run of Figure 5, we have

I R = {1}, E R = ∅, O R = ∅, A R = {a}, and Λ R = {a, b, c}.

Traces

The trace language of an automaton can be obtained by extracting from every accepting run a weak graph, called its trace. Consider an accepting run {ι} , t 0 ; . . . ; t n , ∅ . The graph of its trace is constructed by creating a vertex k for each transition t k of the run. We add an edge k, a, l whenever there is some place q such that a, q ∈ t ▹ k , and t l is the first transition after t k in the run with q among its inputs. The set of tests of the trace is A R . The trace of the run in Figure 5 is presented in Figure 6. The definition we give below is a generalisation for arbitrary valid runs, which coincides with the informal presentation we just gave on accepting runs.

Let R = S, t 0 ; . . . ; t n , S be a run in A. For every k and p ∈ π

2 (t ▹ k ) \ S , we define ν (k, p) = min {l | l > k and p ∈ ▹ t l } .
The trace of R, denoted by G (R), is the pair G R , A R , where G R has vertices V R = {0, . . . , n} ∪ S and edges defined by:

E R = { k, a, l | a, p ∈ t ▹ k and (l = p ∧ p ∈ S ) ∨ (l = ν (k, p))} .
The language L (A) of an automaton A is the set of traces of accepting runs of A. In the following, we will only consider automata such that if G, A ∈ L (A), then either G is either isomorphic to 1 or is a term graph: that is, if G A is a weak graph.

From expressions to automata

In this section, we show how to build inductively from an expression e an automaton A e whose language is L (A e ) = WG ( e ), following [START_REF] Brunet | Algebras of Relations: From algorithms to formal proofs[END_REF]. For 0, 1 and atoms, we give a graphical description of the automata:

A 0 := 0 A 1 := 0 ∅ A α := 1 0 ∅ ∅ α
For the inductive cases, let A e = P e , T e , ι e and A f = P f , T f , ι f , and suppose P e ∩ P f = ∅.

Intuitively, the automaton for e + f is the union of A e and A f , where we copy the initial transitions of A f so that they start from ι e instead of ι f . Formally:

A e+f = P e ∪ P f , T e ∪ T f ∪ T, ι e , where T = ¶¨{ ι e } , Ê t, t ▹ ∂ ¨{ι f } , Ê t, t ▹ ∂ ∈ T f © .
For the product, we want an automaton

A e•f such that L (A e•f ) = L (A e ) • L (A f
). This property is satisfied by the automaton P e ∪ P f , T + e ∪ T f ∪ T, ι e where T + e is the set of non-final transitions in T e , and

T = { ▹ t, A ∪ B, t ▹ | ▹ t, A, ∅ ∈ T e ∧ {ι f } , B, t ▹ ∈ T f }.
Instead of defining directly an automaton for e , we give an automaton for the non-zero iteration e + , and then define A e to be A 1∪e + . Using the last two constructs, the automaton A e + is easy to define:

A e + = P e , T e ∪ { ▹ t, A ∪ B, t ▹ | ▹ t, A, ∅ ∈ T e ∧ {ι e } , B, t ▹ ∈ T e } , ι e .
Finally, we then define A e∩f to be the automaton

P e ∪ P f ∪ {ι} , T 1 ∪ T 2 ∪ T 3 ∪ T 4 , ι
, where ι is a fresh place, and:

T 1 is the set of non-initial, non-final transitions of T e and T f ;

T 2 is the set of triples ¨{ι} , Á t 1 ∪ Á t 2 , t ▹ 1 ∪ t ▹ 2 ∂ such that t 1 (resp. t 2 ) is initial but not final in T e (resp. T f ); T 3 is the set of triples ¨▹t 1 ∪ ▹ t 2 , Á t 1 ∪ Á t 2 , ∅ ∂ such that t 1 (resp. t 2 ) is final but not initial in T e (resp. T f ); T 4 is the set of triples {ι} , A, ∅ such that 1 A ∈ e ∩ f .
This definition is effective, as the set of A ⊆ X such that 1 A ∈ e can be computed in space O |e| × 2 |X| . Using the proofs for Petri automata as a guideline, it is a simple exercise to check that the correctness of the construction, that is L (A e ) = WG ( e ).

Comparing automata

The algorithm to compare weak Petri automata relies on the notion of simulation. Similarly to many finite transition systems, the language of an automaton A is included in that of the automaton B if B can simulate A.

Definition 6 (Simulation).

Let A 1 = P 1 , T 1 , ι 1 and A 2 = P 2 , T 2 , ι 2 be two automata, we say that A 2 can simulate A 1 if there exists a function associating to every subset of X a set of triples from P (P 1 ) × P (X) × P (P 2 P 1 ), such that: (We denote the fact that the triple S, B, E is contained in the image by of the set A by

S B A E.) (correspondence) if S B A E and η ∈ E then range (η) ⊆ S; (initialisation) {ι 1 } ∅ A {[ι 2 → ι 1 ]}; (totality) if ∅ A A E then ∃η ∈ E : dom (η) = ∅; (progress) if S B A E and S t --→ A1 S , then S B∪Ê t A E
, where E is the set of all η such that there is a map η in E, and a run R in A 2 from dom (η) to dom (η ) s.t.:

I R = {p | η (p) ∈ ▹ t} Λ R ∪ A R ⊆ Ȧ ∀ α, p ∈ O R , α, η (p) ∈ t ▹ ∀p ∈ E R , η (p) = η (p) . P. Brunet XX:11 Lemma 7. L (A 1 ) ⊆ L (A 2 ) if and only if A 2 can simulate A 1 .
Proof. We start by showing the right to left direction: suppose that A 2 can simulate A 1 , as witnessed by the function , and consider an accepting run R = S 0 , t 1 ; . . . ; t n ; S n in A 1 :

S 0 = {ι 1 } ∀1 i n, S i-1 ti --→ A1 S i S n = ∅.
We write B i = j<i Á t j . Using the relations Bi A R , we can find a sequence of E i (for 0 i n)

such that S i Bi A R E i , E 0 = {[ι 2 → ι 1 ]},
and there is some η n ∈ E n which has an empty domain. Backtracking from this η n using the progress condition allows us to find a sequence of maps (η i ) 0 i n , with domains (T i ) 0 i n such that there are valid runs R i in A 2 from T i-1 to T i , and satisfying:

T 0 = {ι 2 } T n = ∅ I Ri = {p | η i-1 (p) ∈ ▹ t i } Λ Ri ∪ A Ri ⊆ ȦR ∀ α, p ∈ O Ri , α, η i (p) ∈ t ▹ i ∀p ∈ E Ri , η i-1 (p) = η i (p) .
We now build the run R by concatenating the R i s. We obtain an accepting run in A 2 , whose set of tests is i A Ri ⊆ A R . To any transition t j in R , the function ϕ associates the index i of the run R i from which this transition was extracted. The function ϕ witnesses G (R) G (R ).

For the converse direction, we prove an intermediary result. Let R = S 0 , t 1 ; . . . ; t n , S n be an accepting run in A 1 and R be an accepting run from A 2 such that G (R) G (R ), with ϕ as the witnessing function. Notice that if the transition t i is a cause of t i+1 in R (i.e. they cannot be exchanged without changing the trace), either ϕ (i) = ϕ (i + 1), or t ϕ(i) is a cause of t ϕ(i+1) in R, thus ϕ (i) < ϕ (i + 1). This means that we may permute transitions in R without changing the trace, to obtain a run R such that i < j ⇒ ϕ (i) ϕ (j). Now, the sets of transitions sharing the same value ϕ (i) are contiguous, meaning that R can be split as the sequence of sub-runs R 1 ; . . . ; R n , such that ϕ maps every transitions in R i to i. (It may be the case that some of these runs are empty.) As G (R) G (R ), we know that A R ⊆ A R , which means that ∀i, A Ri ⊆ A R . Inside the run R i , we know that the internal edges of the graph of R i are labelled with letters from A R , as both their extremities are mapped to i. This means Λ Ri ⊆ ȦR .

We know define the η i . First, we set η 0 (ι 2 ) = ι 1 , and ∀p ∈ E Ri , η i-1 (p) = η i (p). If on the other hand α, p ∈ O Ri , let k be the index in R corresponding to the output state of R i , and j = ν R (p, k). As j cannot be in R i , we know ϕ (j) > ϕ (k). Thus, in the graph of R there is an edge ϕ (k) , α, ϕ (j) . By definition of the graph of a run, there must be a pair α, q ∈ t ▹ ϕ(k) such that ν R (q, ϕ (k)) = ϕ (j). Then this q is a suitable choice for η i (p). It is then a simple matter of unfolding the definitions to check that:

I Ri = {p | η i-1 (p) ∈ ▹ t i } ∀ α, p ∈ O Ri , α, η i (p) ∈ t ▹ i ∀p ∈ E Ri , η i-1 (p) = η i (p) .
This means that whenever we have R and R accepting runs from respectively A 1 and A 2 s.t. G (R) G (R ), we can find a sequence of η i satisfying all four conditions of a simulation. Thus, if L (A 1 ) ⊆ L (A 2 ), for every reachable state S of A 1 , we set B A to relate S to the set of all maps η such that there is an index i, an accepting run R in A 1 , and an accepting run R of A 2 satisfying (1) A R = A, [START_REF] Andréka | The equational theory of union-free algebras of relations[END_REF] Proof. The equational theory of identity-free Kleene lattices being already ExpSpacecomplete [7, Proposition 10.2], we know the problem at hand to be ExpSpace-hard.

Let e, f ∈ E X , we ask whether Lang |= e ≤ f . By Theorem 5, this reduces to testing if e ⊆ f , which is equivalent to e ⊆ f by the properties of the closure operator. Using the construction in Section 3.2, this is amounts to checking if L (A e ) ⊆ L (A f ). This later question can be decided by looking for a simulation function, thanks to Lemma 7.

We now inspect the space complexity of this method. Let n, m, x be respectively the size of e, the size of f and the size of the alphabet. By analysing each step in Section 3.2, we get that the number of places of A e is less than 2 × n (similarly for A f ). The number of transitions is harder to work out from the construction, but because T ⊆ P (P ) × P (X) × P Ẋ × P , we know it is bounded by 2 2n+x+2x×2n . Using Savitch's theorem [START_REF] Walter | Relationships between nondeterministic and deterministic tape complexities[END_REF], we only need to show that there is a non-deterministic semi-algorithm to refute the existence of a simulation, which uses only exponential space in n, m and x. Here is such a procedure:

1. choose A ⊆ X; 2. start with S = {ι 1 }, B = ∅ and E = {[ι 2 → ι 1 ]}; 3. if S, B = ∅,
A and E does not contain a map η whose domain is empty return False; 4. choose t ∈ T 1 such that ▹ t ⊆ π 1 (S), fire t from S, and update B as Ê t ∪ B; 5. update E according to the progress condition in Definition 6; 6. go to step 3. All of these computations can be performed using exponential space. For instance, S, being a pair of a set of places in A e and a set of letters, can be stored in space 2n log (2n) × x log (x), and E only needs space (2n + 1)

2m × 2m log (2n + 1).

Conclusion

We showed that the free representation of reversible Kleene lattices consists of downward closed sets of weak terms, or equivalently of downward closed sets of weak graphs. By considering a suitable variation of Petri automata, and producing an algorithm to decide language containment of these automata, we showed that testing the validity of equations in reversible Kleene lattices is an ExpSpace-complete problem.

The results we obtained here could be naturally extended in a number of ways. We would like to add to our model some features of programming languages which have been studied independently, among which tests [START_REF] Kozen | Kleene algebra with tests[END_REF], and nominal structures [START_REF] James | Freshness and name-restriction in sets of traces with names[END_REF][START_REF] Dexter Kozen | Completeness and incompleteness in nominal Kleene algebra[END_REF][START_REF] Dexter Kozen | Nominal Kleene coalgebra[END_REF][START_REF] Brunet | A formal exploration of Nominal Kleene Algebra[END_REF]. Although Kleene algebra is known not to be finitely axiomatisable [START_REF] Nikiforovych | On defining relations for the algebra of regular events[END_REF], several authors have proposed semi-axiomatisations [START_REF] Kozen | A completeness theorem for Kleene Algebras and the algebra of regular events[END_REF][START_REF] Conway | Regular algebra and finite machines[END_REF][START_REF] Salomaa | Two complete axiom systems for the algebra of regular events[END_REF]. A complete axiomatisation of Kleene algebra with converse, relative to an axiomatisation of KA, is also known [START_REF] Ésik | Equational properties of Kleene algebras of relations with conversion[END_REF]. As far as we know, no axiomatisation of reversible Kleene lattices exists. We believe the free representation we defined in Section 2 could help establishing such an axiomatisation. Since we provide here an algorithm, it would be interesting to implement it. Such a procedure could fit in very well in a proof assistant such as Coq.

Although the weak Petri automata introduced in this paper were just a means to an end, we are wondering whether this might be an interesting model of computation in itself. We are confident that we could reuse to technology of boxes introduced in [START_REF] Brunet | Petri automata[END_REF][START_REF] Brunet | Algebras of Relations: From algorithms to formal proofs[END_REF] to get a Kleene theorem for these automata. Their semantics could also be reformulated with transitions labelled with weights chosen from a finite lattice (instead of sets of letters from the alphabet).

D Omitted proof: Lemma 3

We proceed by induction on u.

If u ∈ Ẋ, its graph has only two vertices, and a single edge whose label is u itself. Thus ϕ (i u ) = 0 ∧ ϕ (o u ) = n completely defines ϕ; and x, α, y ∈ E u ⇒ w ϕ [x, y] ∈ σ (α) just means w[0, n] ∈ σ (u). As w[0, n] = w, we are done.

For u ∩ v, by induction w ∈ σ (u ∩ v) is equivalent to the existence of two functions ϕ 1 : V u → {0, . . . , n} and ϕ 2 : V v → {0, . . . , n} satisfying the conditions of the right hand side. It is then a simple matter to check that these to functions can be merged into an appropriate ϕ, and that any acceptable ϕ : V u∩v → {0, . . . , n} could be split into ϕ 1 and ϕ 2 .

For the sequential product, by definition w ∈ σ (u 1 • u 2 ) is equivalent to the existence of a pair of words w 1 , w 2 ∈ σ (u 1 ) × σ (u 2 ) such that w = w 1 w 2 . By induction, we get that for k ∈ {1, 2}, w k ∈ σ (u k ) if and only if there is a map ϕ k such that ϕ k (i u k ) = 0, ϕ k (o u k ) = |w k |, and x, α, y ∈ E u k ⇒ w ϕ k [x, y] ∈ σ (α). We need to show that this last condition is equivalent to the existence of a single ϕ : V u1•u2 → {0, . . . , n}. Building such a ϕ from ϕ 1 and ϕ 2 is simple: we define

ϕ (x) := ® ϕ 1 (x) if x ∈ V u1 ; ϕ 2 (x) + |w 1 | otherwise.
If on the other hand we have ϕ : V u1•u2 → {0, . . . , n} such that ϕ (i u1•u2 ) = 0 ∧ ϕ (o u1•u2 ) = n and x, α, y ∈ E u1•u2 ⇒ w ϕ [x, y] ∈ σ (α), then we define w 1 and w 2 as respectively w ϕ [i u1 , o u1 ] and w ϕ [i u2 , o u2 ], and ϕ 1 (x) := ϕ (x), ϕ 2 (x) := ϕ (x) -ϕ (i u2 ).

E

Omitted proof: uniformity lemma By Theorem 4 we get that for every u such that WG (u) WG (v),we have σ (u) ⊆ σ (v). This ensures that:

= a -= a N -= ∅ 1 -= {∅} e + f -= e -∪ f - e • f -= ¶ A ∪ B A, B ∈ e -× f -© e -= ¶ A 1 ∪ • • • ∪ A n A i ∈ e -© e ∩ f -= ¶ A ∪ B A, B ∈ Ä e -× Ä f -∪ S (f ) ää ∪ Ä S (e) × f -ä© .
A simple induction allows one to check that these sets satisfy the following properties:

S (e) = {A ∪ var (u) | u A ∈ e } e -= {A | 1 A ∈ e } .
Furthermore, they can be effectively computed in space exponential in the size of X, and linear in the size of e.

Figure 1 Figure 2

 12 Figure 1 Graphs associated to terms.

Figure 3

 3 Figure 3 Weak graph morphism: G, {a} H, ∅

Figure 5

 5 Figure 4 Weak Petri automaton.

Figure 6

 6 Figure 6 Trace of R.

8 .

 8 j<i Á t j = B, (3) S = S i , (4) G (R) G (R ) and (5) the construction we just provided produces η i = η. The theory of reversible Kleene lattices is ExpSpace-complete.

First,

  We define the set of ground terms βe as in[START_REF] Andréka | The equational theory of Kleene lattices[END_REF] by structural induction:β0 := ∅ β1 := {1} βα := {α} βe + f := βe ∪ βf βe • f := {u • v | u ∈ βe ∧ v ∈ βf } βe ∩ f := {u ∩ v | u ∈ βe ∧ v ∈ βf } βe := {u 1 . . . u n | n 0 ∧ ∀0 i n, u i ∈ βe } It is straightforward to check that e = {τ (u) | u ∈ βe }.By [1, Lemma 2.1] we have that σ (e) = u∈ βe σ (u) thus using Lemma 1 and the fact that e = {τ (u) | u ∈ βe } we get:

17 F

 17 Computing the set of tests of an expression.We define inductively two sets of sets of variables associated with every expression:S (0) = ∅ S (1) = {∅} S (a) = S (a N ) = {{a}} S (e + f ) = S (e) ∪ S (f ) S (e • f ) = S (e ∩ f ) = {A ∪ B | A, B ∈ S (A) × S (f )} S (e ) = {A 1 ∪ • • • ∪ A n | A i ∈ S (e)} 0 -

In the following, we use the definitions from[START_REF] Brunet | Algebras of Relations: From algorithms to formal proofs[END_REF]. They differ slightly from those from[START_REF] Brunet | Petri Automata for Kleene Allegories[END_REF], despite being overall equivalent.

A Restriction of the use of converse

We define the following mutually recursive functions:

B

Omitted proof: Lemma 1

Proof. If u ∈ {a, a N } then var (u) = {a}, and because ε = ε N we have:

P. Brunet

XX:15

Using this fact, the proof of Lemma 1 by structural induction is straightforward: by definition of σ we have σ (u ∅ ) = σ (u). This ensures that the lemma holds for all base cases, i.e. 1, a, and a N ; For the sequence:

For the intersection:

(Definitions of τ and •)

C Omitted proof: Lemma 2

For a term s ∈ GT -X , and two vertices x 1 , x 2 ∈ V u , we write Hom s (x 1 , x 2 ) for the set of maps ϕ :

, and for every edge x, α, y in E G(s) , either ϕ (x) , α, ϕ (y) ∈ E u or α ∈ Ȧ and ϕ (x) = ϕ (y). We now prove by induction on t that Hom t (x, y)

and ϕ ∈ Hom s (x, y) means that ϕ (0) = x, ϕ (1) = y, and either x, s, y ∈ E u or s ∈ Ȧ and x = y. If x = y then we've already noticed that x, s, y ∈ E u is equivalent to w f u (x, y) ∈ σ u (s). If on the other hand x = y then w f u (x, y) = ε, and again we know that ε ∈ σ u (s) is equivalent to s ∈ Ȧ. In the end, we get that ∃ϕ ∈ Hom s (x, y) ⇔ w f u (x, y) ∈ σ u (s). For the case s = t • t , we need to use the following property: ∀x, y, ∃ϕ ∈ Hom t•t (x, y) ⇔ ∃z : ∃ ϕ 1 , ϕ 2 ∈ Hom t (x, z) × Hom t (z, y) .

The direct implication is straightforward, and the converse relies on the fact that the graphs of t and t only overlap on the output of t and input of t .

Using this and the induction hypothesis, we get ∃ϕ ∈ Hom t•t (x, y) ⇔ ∃z :

For the last implication, if w f u (x, y) ∈ σ u (t • t ), then there must be w 1 , w 2 ∈ σ u (t) × σ u (t ) such that w f u (x, y) = w 1 w 2 . To conclude, we use the fact that for every simple term s, if a sub-word x i . . . x j of w u is in σ u (s) then either i = j or ∃x, y : f (x) = i ∧ f (y) = j. This can be established by a simple induction on s, and implies that there must be some z such that w 1 = w f u (x, z) and w 2 = w f u (z, y). The last case is the simplest one: ∃ϕ ∈ Hom t∩t (x, y) ⇔ ∃ϕ ∈ Hom t (x, y) ∧ ∃ϕ ∈ Hom t (x, y) ⇔ w f u (x, y) ∈ σ u (t) ∧ w f u (x, y) ∈ σ u (t ) ⇔ w f u (x, y) ∈ σ u (t ∩ t )

We have now established that Hom t (x, y) = ∅ ⇔ w f u (x, y) ∈ σ u (t). To conclude, notice that w u = w f u (i u , o u ), and because B ⊆ A, σu (v) = σ u (t), thus we get w u ∈ σu (v) ⇔ w f u (i u , o u ) ∈ σ u (t) ⇔ ∃ϕ ∈ Hom t (i u , o u ) ⇔ WG (u) WG (v) .