Lingmin Liao
email: lingmin.liao@u-pec.fr

Micha L Rams
email: rams@impan.pl

UPPER AND LOWER FAST KHINTCHINE SPECTRA IN CONTINUED FRACTIONS

Keywords:

For an irrational number x ∈ [0, 1), let x = [a1(x), a2(x), • • • ] be its continued fraction expansion. Let ψ : N → N be a function with ψ(n)/n → ∞ as n → ∞. The (upper, lower) fast Khintchine spectrum for ψ is defined as the Hausdorff dimension of the set of numbers x ∈ (0, 1) for which the (upper, lower) limit of 1 ψ(n) n j=1 log aj (x) is equal to 1. The fast Khintchine spectrum was determined by Fan, Liao, Wang, and Wu. We calculate the upper and lower fast Khintchine spectra. These three spectra can be different.

Introduction

Each irrational number x ∈ [0, 1) admits a unique infinite continued fraction expansion of the form x = 1 a 1 (x) + 1 a 2 (x) + 1

a 3 (x) + . . . , (1.1)
where the positive integers a n (x), called the partial quotients of x, can be generated by using the Gauss transformation T : [0, 1) → [0, 1) defined by T (0) := 0, and T (x) := 1 x (mod 1), for x ∈ (0, 1).

In fact, let a 1 (x) = ⌊x -1 ⌋ (⌊•⌋ stands for the integer part), then a n (x) = a 1 (T n-1 (x)) for n ≥ 2. For simplicity, (1.1) is often written as

x = [a 1 , a 2 , • • • ].
For any irrational number x ∈ (0, 1), its Khintchine exponent is defined by the limit (if it exists)

ξ(x) := lim n→∞ log a 1 (x) + • • • + log a n (x) n . (1.2)
Khintchine [START_REF] Khintchine | Metrische Kettenbruchprobleme[END_REF] (see also [9, p. 93]) proved that for Lebesgue almost all points x, we have ξ(x) = 1 0 log a 1 (x) (1 + x) log 2 dx = log(2.6854...) =: ξ 0 .

Though Khintchine did not use ergodic theory in his orignal proof, his result is a consequence of Birkhoff Ergodic Theorem, by the fact that the Gauss transformation T is ergodic with respect to the measure dx/((1 + x) log 2) and that the average in (1.2) can be written as a Birkhoff ergodic average.

From a multifractal point of view, one is also interested in the sets of points with a given Khintchine exponent which is different from ξ 0 . The Hausdorff dimension (denoted by dim H ) of the level sets

E(α) := x ∈ [0, 1) : lim n→∞ log a 1 (x) + • • • + log a n (x) n = α , α > 0,
was calculated in [START_REF] Fan | On Kintchine exponents and Lyapunov exponents of continued fractions[END_REF]. It turns out that the Khintchine spectrum, i.e., the function α → dim H E(α) is a real-analytic curve increasing on [0, ξ 0 ] and decreasing on (ξ 0 , ∞). Further, the Hausdorff dimension of E(+∞) is equal to 1/2, which means that there are lots of numbers with infinite Khintchine exponent. This thus leads to the question of detailed classification of numbers with infinite Khintchine exponent. Let α > 0 and let ψ : N → N such that ψ(n)/n → ∞ as n → ∞. We consider the following subsets of E(+∞):

E(ψ, α) := x ∈ [0, 1) : lim n→∞ log a 1 (x) + • • • + log a n (x) ψ(n) = α α > 0.
The so-called fast Khintchine spectrum, i.e., the Hausdorff dimension of E(ψ, 1) was obtained in [START_REF] Fan | On the fast Khintchine spectrum in continued fractions[END_REF]. Let ψ and ψ be two functions defined on N. We say ψ and ψ are equivalent

if ψ(n) ψ(n) → 1 as n → ∞. Define β = β(ψ) := lim sup n→∞ ψ(n + 1) ψ(n) . (1.3)
The authors of [START_REF] Fan | On the fast Khintchine spectrum in continued fractions[END_REF] proved the following theorem.

Theorem 1.1 ([5], Theorem 1.1). Let ψ : N → N with ψ(n)/n → ∞ as n → ∞. If ψ is equivalent to a nondecreasing function, then E(ψ, 1) = ∅ and dim H E(ψ, 1) = 1 1 + β(ψ)
.

Otherwise, E(ψ, 1) = ∅.

We remark that the level α = 1 of the level set E(ψ, 1) in Theorem 1.1 can be replaced by any level α > 0. In fact, observing that for all α > 0,

E(ψ, α) = E( ψ, 1) with ψ = α -1 • ψ and that β( ψ) = β(ψ), we obtain dim H E(ψ, α) = dim H E( ψ, 1) = 1 1 + β( ψ) = 1 1 + β(ψ) , ∀α > 0.
Similarly, when ψ is not equivalent to a nondecreasing function, we have E(ψ, α) = ∅ for all α > 0.

In this note, we consider the following sets

E(ψ) = x ∈ [0, 1] : lim sup n→∞ log a 1 (x) + • • • + log a n (x) ψ(n) = 1 , (1.4) and E(ψ) = x ∈ [0, 1] : lim inf n→∞ log a 1 (x) + • • • + log a n (x) ψ(n) = 1 . (1.5)
Their Hausdorff dimensions are called upper and lower fast Khintchine spectra.

Remark that we only consider the level α = 1 here, since for other levels the Hausdorff dimension will not change, as in Theorem 1.1.

Our main result is as follows.

Theorem 1.2. Assume that ψ :

N → N satisfies ψ(n)/n → ∞ as n → ∞. Write lim inf n→∞ log ψ(n) n = log b and lim sup n→∞ log ψ(n) n = log B. (1.6) Assume b, B ∈ (1, ∞]. Then dim H E(ψ) = 1 1 + b and dim H E(ψ) = 1 1 + B .
We remark that b ≤ B ≤ β. The first inequality is directly from the definitions (1.6). For the second, by (1.3), for any small ε > 0, there exists n 0 such that ψ(i + 1)/ψ(i) ≤ β + ε for all i ≥ n 0 . Then

ψ(n) = ψ(n 0 ) • n-1 i=n 0 ψ(i + 1) ψ(i) ≤ ψ(n 0 ) • (β + ε) n-n 0 .
Hence the second inequality follows from the definition (1.6) of B. However, one can construct some ψ such that the three values b, B and β are all different.

We also remark that from Theorem 1.2, the sets E(ψ) and E(ψ) are always nonempty.

Our result can be considered as a contribution to the multifractal analysis of Birkhoff sums (averages) of dynamical systems. In history, the first multifractal analysis of Birkhoff averages may be due to Besicovitch who studied the frequencies of digits in binary expansions. Let x ∈ [0, 1] and let x = .x 1 x 2 . . . , with x i ∈ {0, 1} denote its binary expansion. Besicovitch ([1, p. 322]) obtained the Hausdorff dimension of the following level sets

x ∈ [0, 1] : lim sup n→∞ x 1 + • • • + x n n ≤ α , α ∈ [0, 1/2].
Let (X, d) be a metric space, T be a (piecewise) continuous transformation on X, and φ : X → R be a real-valued (piecewise) continuous function. The Hausdorff dimension of the level sets of Birkhoff averages:

x ∈ X : lim

n→∞ φ(x) + φ(T x) + • • • + φ(T n x) n = α , α ∈ R,
were widely studied ( [START_REF] Olivier | Analyse multifractale de fonctions continues[END_REF][START_REF] Fan | Recurrence, dimension and entropy[END_REF][START_REF] Pesin | The multifractal analysis of Birkhoff averages and large deviations[END_REF]). In [6, Theorem 3.3], a multifractal analysis result of the above level sets replacing lim by lim sup and lim inf was established for the full shift over two symbols and was applied to the study of dynamical Diophantine approximation.

In contrast to continued fractions, in symbolic dynamical systems of finitely many symbols there is no fast spectrum since the Birkhoff averages are usually bounded (for example, when φ is continuous). Thus the fast spectra studied in this note and in [START_REF] Fan | On Kintchine exponents and Lyapunov exponents of continued fractions[END_REF][START_REF] Wu | On the distribution for sums of partial quotients in continued fraction expansions[END_REF][START_REF] Xu | On sums of partial quotients in continued fraction expansions[END_REF][START_REF] Liao | Subexponentially increasing sum of partial quotients in continued fraction expansions[END_REF] are new subjects for continued fractions and can have generalization in symbolic dynamical systems of infinitely many symbols.

The result of [START_REF] Fan | A multifractal mass transference principle for Gibbs measures with applications to dynamical Diophantine approximation[END_REF]Theorem 3.3] shows that in symbolic dynamical systems with finitely many symbols, the multifractal spectra remain the same when lim is replaced by lim sup or lim inf. However, our main result Theorem 1.2 proves that in the case of fast Khintchine spectra, if we change lim to lim sup or lim inf, the result changes essentially. This uncovers a new phenomenon in continued fractions and in symbolic dynamical systems of infinitely many symbols.

Preliminaries

For any n ≥ 1 and (a

1 , a 2 , • • • , a n ) ∈ N n , define I n (a 1 , a 2 , • • • , a n ) = x ∈ [0, 1) : a 1 (x) = a 1 , • • • , a n (x) = a n ,
which is the set of numbers starting with (a 1 , • • • , a n ) in their continued fraction expansions, and is called a basic interval of order n. The length of a basic interval will be denoted by

|I n |. Proposition 2.1 ([9], p. 66, p. 68). For any n ≥ 1 and (a 1 , • • • , a n ) ∈ N n , (2.1) 2 n n k=1 a k -2 ≤ |I n (a 1 , • • • , a n )| ≤ n k=1 a k -2
.

The following lemma is used to calculate the lower bound of the Hausdorff dimension of E(ψ).

Let ℓ ≥ 2 be some fixed real number and {s n } n≥1 be a sequence of real numbers such that s n ≥ 1. Set

F ({s n } ∞ n=1 ; ℓ) := x ∈ [0, 1) : s n ≤ a n (x) < ℓs n , for all n ≥ 1 . Lemma 2.2 ([4], Lemma 3.2). Under the assumption that s n → ∞ as n → ∞, one has dim H F ({s n } ∞ n=1 ; ℓ) = 2 + lim sup n→∞ log s n+1 log s 1 s 2 • • • s n -1 .
We remark that the Hausdorff dimension of the set F ({s n } ∞ n=1 ; ℓ) does not depend on ℓ. The original version of Lemma 2.2 asks for the sequence {s n } and the number ℓ to be positive integers. However, a slight modification of the proof also works for real numbers.

In fact, Lemma 2.2 has a more general form. Let s := {s n } n≥1 and t := {t n } n≥1 be two sequences of real numbers such that s n ≥ 1, t n > 1 for all n ≥ 1. Consider the following set

F (s, t) := x ∈ [0, 1) : s n ≤ a n (x) < s n t n , for all n ≥ 1 .
Naturally, we do need to assume that for each n there is an integer between s n and s n t n , otherwise F (s, t) would be empty.

Lemma 2.3. Assume that F (s, t) = ∅, s n → ∞ as n → ∞, and lim n→∞ log(t n -1) log s n = 0.
Then

dim H F (s, t) = 2 + lim sup n→∞ log s n+1 log s 1 s 2 • • • s n -1 .
The proof of Lemma 2.3 is essentially contained in the proof of the lower bound of the dimension of E(ψ) in Subsection 3.2. So the details are left for the reader. A special case of Lemma 2.3 can be found in [START_REF] Liao | Subexponentially increasing sum of partial quotients in continued fraction expansions[END_REF]Lemma 2.3].

The next lemma will be used to obtain the upper bound of the Hausdorff dimensions of E(ψ) and E(ψ).

Lemma 2.4 ([11], Main Theorem). For any a > 1, b > 1, dim H x ∈ [0, 1] : a n (x) ≥ a b n , ∀n ≥ 1 = dim H x ∈ [0, 1] : a n (x) ≥ a b n , for infinitely many n = 1 b + 1 .
3. Proofs

Dimension of E(ψ).

We first calculate the Hausdorff dimension of E(ψ) as defined in (1.4). We will only give the proof for 1 < b < ∞. The case b = ∞ can be obtained by a standard limit procedure. Upper bound: For x ∈ E(ψ), let S n (x) := log a 1 (x) + • • • + log a n (x). Then for any δ > 0, there are infinitely many n's such that

(3.1) S n (x) ≥ ψ(n)(1 -δ).
For each such n there exists an i ≤ n such that

(3.2) log a i (x) ≥ ψ(n) 2n (1 -δ).
Moreover, for infinitely many i's we can find n ≥ i satisfying (3.1) such that (3.2) holds. Indeed, if i 0 was the largest i with this property, for every n > i 0 satisfying (3.1) we would have

S n (x) = S i 0 (x) + n k=i 0 +1 log a k (x) < S i 0 (x) + 1 -δ 2 ψ(n) and hence, ψ(n) < 2(1 -δ) -1 S i 0 (x).
Thus ψ(n) for n satisfying (3.1) would be uniformly bounded. This contradicts the assumption ψ(n)/n → ∞.

By the definition (1.6) of b, for any small ε > 0 (ε

< (b-1)/100 is enough) we have ψ(n) > (b -ε) n > 1 and (b -ε) n (1 -δ)/2n > (b -2ε
) n for all n large enough. Thus, by (3.2) there are infinitely many i's, such that

log a i (x) > (b -ε) n 2n (1 -δ) > (b -2ε) n ≥ (b -2ε) i .
It then follows that the set E(ψ) is included in the set

x ∈ [0, 1] : a i (x) > e (b-2ε) i , for infinitely many n .

By Lemma 2.4, the Hausdorff dimension of E(ψ) is bounded by 1/ 1 + (b -2ε) from above. Letting ε → 0, we obtain the upper bound.

Lower bound: We will construct a Cantor type subset of E(ψ).

We want to construct a sequence {c n } n≥1 of positive real numbers such that

(3.3) lim sup n→∞ log c 1 + • • • + log c n ψ(n) = 1, and
(3.4) lim sup n→∞ log c n+1 log c 1 + • • • + log c n ≤ b -1 + ε.
The condition (3.3) will be used to construct points in E(ψ) while the condition (3.4) will be helpful for estimating the Hausdorff dimension.

Let us begin by defining an auxiliary function

φ(n) = min k≥n ψ(k).
As ψ(n) → ∞, φ(n) is well defined for all n. Obviously, φ ≤ ψ and φ is a nondecreasing function. One can easily check that there exist infinitely many n's for which φ(n) = ψ(n). One more property that we will soon use is 1) and

(3.5) φ(n) = ψ(n) =⇒ φ(n) = min k≥n ψ(k) = min k>n ψ(k) = φ(n + 1). Let c 1 = e φ(
c 2 = min e φ(2) c 1 , c b-1+ε 1 .
Assume that c n-1 has already been well defined, then set

c n = min e φ(n) n-1 k=1 c k , n-1 k=1 c b-1+ε k . (3.6)
Observe that as φ is nondecreasing, c n ≥ 1 for all n ≥ 1.

We can check that lim sup

n→∞ log c n+1 log c 1 + • • • + log c n ≤ lim sup n→∞ log n k=1 c b-1+ε k log n k=1 c k = b -1 + ε.
Thus (3.4) holds.

To prove (3.3) we will need several steps. By the definition (1.6) of b, we claim that

c n = e φ(n) n-1 k=1 c k for infinitely many n. (3.7)
Indeed, if it is not true then for some N and for all n ≥ N we have , which together with (3.9) and φ ≤ ψ is in contradiction with (1.6).

Observe now that by (3.5) and (3.6), if the equality in (3.7) holds for some n such that φ(n) = ψ(n) then it will hold for n + 1 as well (and c n+1 = 1). Since φ(n) = ψ(n) infinitely often, repeating this argument until we get to some n + k for which φ(n + k) = ψ(n + k), we prove

c n = e ψ(n) n-1 k=1 c k for infinitely many n. (3.10)
Denoting by {n j } the sequence of numbers satisfying (3.10), we get lim sup

n→∞ log c 1 + • • • + log c n ψ(n) ≥ lim sup j→∞ log c 1 + • • • + log c n j ψ(n j ) = 1.
On the other hand, by (3.6), lim sup

n→∞ log c 1 + • • • + log c n ψ(n) ≤ lim sup n→∞ log c 1 + • • • + log c n φ(n) ≤ 1.
Hence (3.3) holds. Define

E({c n }) := {x ∈ [0, 1) : c n ≤ a n (x) < 2c n , for all n ≥ 1}.
Since ψ(n)/n → ∞ as n → ∞, by (3.3), E({c n }) ⊂ E(ψ). Now we would like to apply Lemma 2.2 to estimate the Hausdorff dimension of E({c n }). However, observe that (3.3) does only imply that lim sup c n = ∞, but not that c n → ∞. For example, if ψ (or φ) has a long plateau then we can find many n's with c n = 1, and hence for a function ψ with infinitely many long plateaux there might exist a subsequence c n i ≡ 1. On the other hand, to apply Lemma 2.2 we need the condition c n → ∞ as n → ∞. So, some modifications on the subset E({c n }) are needed.

By the condition that ψ(n)/n → ∞ as n → ∞, we can choose an increasing sequence

{n k } ∞ k=1 such that for each k ≥ 1 ψ(n) n ≥ k 2 , when n ≥ n k . Take α n = 2 if 1 ≤ n < n 1 and α n = k + 1, when n k ≤ n < n k+1 . Let k(n) be such that n k(n) ≤ n < n k(n)+1 . Then lim n→∞ log α 1 + • • • + log α n ψ(n) ≤ lim n→∞ n • (k(n) + 1) n • k(n) 2 = 0 and lim n→∞ log α n+1 log α 1 + • • • + log α n ≤ lim n→∞ log(n + 1) n • log 2 = 0.
Since c n ≥ 1 and α n ≥ 2 for all n ≥ 1, we have

log c n ≤ log(c n + α n ) ≤ log c n + 2 log α n ∀n ≥ 1.
So, by taking s n = c n + α n for each n ≥ 1, we get s n → ∞ as n → ∞ and lim sup

n→∞ log s 1 + • • • + log s n ψ(n) = 1. Define E({s n }) := {x ∈ [0, 1) : s n ≤ a n (x) < 2s n , for all n ≥ 1}. Then E({s n }) ⊂ E(ψ). As s n → ∞ as n → ∞, by Lemma 2.2, we have dim H E({s n }) = 2 + lim sup n→∞ log s n+1 log s 1 + • • • + log s n -1 . Note that lim sup n→∞ log s n+1 log s 1 + • • • + log s n = lim sup n→∞ log(c n+1 + α n+1 ) log(c 1 + α 1 ) + • • • + log(c n + α n ) ≤ lim sup n→∞ log c n+1 + 2 log α n+1 log(c 1 + α 1 ) + • • • + log(c n + α n ) ≤ lim sup n→∞ log c n+1 log c 1 + • • • + log c n + lim sup n→∞ 2 log α n+1 log α 1 + • • • + log α n ≤ b -1 + ε. Hence, dim H E(ψ) ≥ dim H E({s n }) ≥ 1 b + 1 + ε .

Dimension of E(ψ).

As in the calculation of the Hausdorff dimension of E(ψ), we will only give the proof for 1 < B < ∞ and the easy case B = ∞ is left for the reader.

Upper bound: By the definition (1.6) of B, for any ε > 0, there is a sequence {n i } such that

ψ(n i ) > (B -ε) n i . Denoting S n (x) = log a 1 (x) + • • • + log a n (x), for all x ∈ E(ψ), for any δ > 0, we have S n (x) ≥ ψ(n)(1 -δ), ∀n ≥ 1. Thus S n i (x) ≥ (B -ε) n i (1 -δ). Then there exists j ≤ n i such that (3.11) log a j (x) ≥ (B -ε) n i (1 -δ)/2n i > (B -2ε) j .
By the same argument as in the previous subsection, we have infinitely many such j's for which we can find n i satisfying (3.11). Thus by Lemma 2.4, the Hausdorff dimension of E(ψ) is bounded by 1/(1 + (B -2ε)) from above.

The upper bound then follows by letting ε → 0.

n i log ψ(n) log log A i slope= log(B + ε) t i Figure 1. Finding A i .
Lower bound: As in the previous subsection, a Cantor type subset of E(ψ) will be constructed.

For any ε > 0, define

A i = sup n≥i exp{ψ(n)(B + ε) i-n }. (3.12) Since lim sup n→∞ log ψ(n) n
= log B, we have for n large enough

ψ(n) ≤ (B + ε/2) n .
This implies

ψ(n)(B + ε) i-n ≤ (B + ε/2) n (B + ε) i-n → 0 (n → ∞).
Hence in the definition (3.12) of A i the supremum is achieved. Denote by t i ≥ i the smallest number for which A i = exp{ψ(t i )(B + ε) i-t i }. Figure 1 shows a way to find t i and A i .

We remark that such defined A i is the smallest function satisfying

(3.13) A i+1 ≤ A B+ε i and A i ≥ e ψ(i) .
Let

Z := lim inf n→∞ n i=1 log A i ψ(n) .
By (3.13), we have

Z ≥ lim inf n→∞ log A n ψ(n) ≥ 1.
We will use these A i and Z to construct our Cantor type subset. Before the construction, let us prove the following proposition. Proposition 3.1. We have Z < ∞.

Proof. Remark that for many consecutive i's the t i will be the same. More precisely, t i = t i+1 = • • • = t t i . Let {ℓ j } be the sequence of all t i 's in the increasing order, without repetitions. Notice that for these ℓ j , we have log A ℓ j = ψ(ℓ j ), and for k ∈ (ℓ j-1 , ℓ j ],

log A k = ψ(ℓ j )(B + ε) k-ℓ j . Thus for 0 < ε < B -1 (3.14) ℓ j k=ℓ j-1 +1 log A k = ℓ j k=ℓ j-1 +1 ψ(ℓ j )(B + ε) k-ℓ j ≤ B + ε B + ε -1 • ψ(ℓ j ).
Denote S n ψ := n k=1 ψ(k). Proposition 3.1 follows directly from the following two lemmas. Lemma 3.2. We have

lim inf n→∞ S n ψ ψ(n) < ∞.
Proof. For ε > 0, we will show that there exist infinitely many n, such that ψ(n) > εS n-1 ψ. If this was not true, then for all large n we would have

S n ψ = S n-1 ψ + ψ(n) ≤ (1 + ε)S n-1 ψ.
Thus by Stolz-Cesàro Theorem lim sup

n→∞ log S n ψ n ≤ lim sup n→∞ log S n ψ -log S n-1 ψ n -(n -1) ≤ log(1 + ε),
which is impossible since we have lim sup

n→∞ log S n ψ n ≥ lim sup n→∞ log ψ(n) n = B > log(1 + ε).
Denote by {n j } a sequence such that ψ(n j ) > εS n j -1 ψ. Then

S n j ψ ψ(n j ) = S n j -1 ψ + ψ(n j ) ψ(n j ) ≤ 1 + 1 ε < ∞,
and the conclusion follows.

Lemma 3.3. The following limit is finite:

lim inf j→∞ S ℓ j ψ ψ(ℓ j ) < ∞.
Proof. Denote L := lim inf n→∞ Snψ ψ(n) . Fix 0 < ε < B -1 and let {m k } be the sequence such that

S m k ψ ψ(m k ) ≤ L + ε.
Each m k is in some (ℓ j-1 , ℓ j ], hence for this j

S ℓ j ψ = S m k ψ + ℓ j i=m k +1 ψ(i) ≤ (L + ε)ψ(m k ) + ℓ j i=m k +1 ψ(i) ≤ (L + ε) ℓ j i=m k ψ(i). By definition of ℓ j , for i ∈ [m k , ℓ j ] ⊂ (ℓ j-1 , ℓ j ] ψ(i) ≤ 1 (B + ε) ℓ j -i ψ(ℓ j ), Thus S ℓ j ψ ≤ B + ε B + ε -1 • (L + ε)ψ(ℓ j ).
The result then follows.

By (3.14)

ℓ j k=1 log A k ≤ C • S ℓ j ψ. Hence Z ≤ lim inf j→∞ ℓ j k=1 log A k ψ(ℓ j ) ≤ C S ℓ j ψ ψ(ℓ j ) < ∞,
which completes the proof of Proposition 3.1

Now we continue the construction of the subset and the estimation of the lower bound.

Choose a sequence where

ε i → 0 such that lim n→∞ n i=1 log(1 ± ε i ) ψ(n) = 0, (3.15) lim n→∞ | n i=1 log(2ε i )| log A n+1 = 0, ( 3
W i := [A 1/Z i (1 -ε i ), A 1/Z i (1 + ε i )].
Observe that the condition (3.16) implies the condition (3.17) for all i large enough. Observe also that for large i, (3.16) and (3.17) say only that ε i is greater than some negative power of A i (which is increasing superexponentially fast) while the condition (3.15) is satisfied for all decreasing sequences, so there is no problem to find such a sequence {ε i } satisfying all the conditions (3.15)-(3.17).

Denote by E the set of numbers x such that for all i, a i (x) is in the interval W i . By (3.17), E is nonempty. By (3.15), for all

x ∈ E lim inf n→∞ n j=1 log a j (x) ψ(n) = lim inf n→∞ 1 Z n j=1 log A j ψ(n) = 1.
So E ⊂ E(ψ). Now we will estimate the Hausdorff dimension of E from below. To this end, we define a probability measure µ on E. For each position, we distribute the probability evenly. That is, for each possible a i , we give the probability

p i = 1 1 + |[⌈A 1/Z i (1 -ε i )⌉, ⌊A 1/Z i (1 + ε i )⌋]| ≈ 1 2ε i A 1/Z i .
Here and in what follows, we follow [START_REF] Jordan | Increasing digit subsystems of infinite iterated function systems[END_REF]. For simplicity we give only the main term of the calculations.

By the probability distribution, for each basic interval I n = I n (a 1 , . . . a n ), we have

µ(I n ) = n i=1 p i ≈ n i=1 (2ε i A 1/Z i ) -1 .
By (2.1),

|I n | ≈ n i-1 (A 1/Z i ) -2 .
To calculate the local dimension of x ∈ E we will use a smaller interval D n included in I n : (3.18)

D n = ∪ a n+1 ≥A 1/Z n+1 (1-ε n+1 ) I n+1 (a 1 , • • • , a n a n+1 ). Since a i ∈ [A 1/Z i (1 -ε i ), A
The last ≈ follows from (3.16).

On the other hand, the length of the interval D n is

|D n | ≈ |I n | • A -1/Z n+1 . Thus -log |D n | ≈ -log |I n | + 1 Z log A n+1 ≈ -2 log µ(D n ) + 1 Z log A n+1 . Hence -log µ(D n ) -log |D n | ≈ -log µ(D n ) -2 log µ(D n ) + 1 Z log A n+1 = 1 2 + 1 Z log A n+1 -log µ(Dn)
.

Then by (3.18), we obtain

lim inf n→∞ -log µ(D n ) -log |D n | ≥ 1 2 + (B + ε -1) = 1 B + 1 + ε .
Therefore the lower bound follows from the Frostman Lemma (see [2, Principle 4.2]).

-MUTADIS (France). M.Rams was partially supported by the MNiSW grant N201 607640 (Poland).

  .16) and for each i W i ∩ N = ∅, (3.17)

( 1 +

 1 ε i )] and A i grows super-exponentially, the Hausdorff dimension will be determined by calculating the local dimension lim infn→∞ log µ(D n ) log |D n | .(See Section 4 of Jordan and Rams[START_REF] Jordan | Increasing digit subsystems of infinite iterated function systems[END_REF].) On the one hand,log µ(D n ) =log µ(I n ) =By the property that A i+1 ≤ A B+ε i , we deduce that for big n,log µ(D n ) ≥ ε) i log A n+1 ≈ 1 Z(B + ε -1) log A n+1 .

Acknowledgements. The authors thank Bao-Wei Wang for the fruitful discussions. L. Liao was partially supported by the ANR, grant 12R03191A


Nicolas David
email: nicolas.david1@univ-nantes.fr

Didier Claude Jard
email: claude.jard@univ-nantes.fr

Didier Lime
email: didier.lime@ec-nantes.fr

Olivier Henri Roux
email: olivier-h.roux@irccyn.ec-nantes.fr

Discrete Parameters in Petri Nets

Keywords: Petri net, Parameters, Coverability

come

Introduction

The introduction of parameters in models aims to improve genericity. It also allows the designer to leave unspecified aspects, such as those related to the modeling of the environment. This increase in modeling power usually results in greater complexity in the analysis and verification of the model. Beyond verification of properties, the existence of parameters opens the way to very relevant issues in design, such as the computation of the parameters values ensuring satisfaction of the expected properties.

We chose to explore the subject on concurrent models whose archetype is that of Petri nets. We consider discrete parameterisation of markings (the number of tokens in the places of the net) or weight of arcs connecting the input or output places to transitions. We call these Petri nets parameterised nets or PPNs.

We consider the general properties of coverability and, to a lesser extent, reachability (that are often the basis for the verification of more specific properties).

First issues are:

-Is there a value of the parameters such that the property is satisfied? -Is the property satisfied for all possible values of the parameters?

Given the modeling power offered by PPNs, we first study the decidability of these issues. Since in the general case, they are undecidable, we then examine decidable subclasses.

Related work. There is not much work on Petri nets with parameters. One example is regular model checking [START_REF] Bouajjani | Regular model checking[END_REF] for algorithmic verification of several classes of infinite-state systems whose configurations can be modeled as words over a finite alphabet. The main idea is to use regular languages as the representation of sets of configurations, and finite-state transducers to describe transition relations. This is only possible for particular examples including parameterised systems consisting of an arbitrary number of homogeneous finite-state processes connected in a regular topology, and systems that operate on linear data structures. Parameters are also introduced in models such as predicate Petri nets [START_REF] Lindqvist | Parameterized reachability trees for predicate/transition nets[END_REF], in the aim to have more concise models, in particular to take into account symmetries in the model [START_REF] Chiola | A symbolic reachability graph for coloured petri nets[END_REF]. Domains of values are generally finite. Parameterised verification on timed systems has also been studied in several papers since its introduction by Alur et al. in [START_REF] Alur | Parametric real-time reasoning[END_REF]. Parameterisation of time uses continuous parameters. In this paper, we focus on discrete parameters on untimed Petri nets.

The remainder of the paper is structured as follows: Section 2 re-visites the semantics of Petri Nets and introduces discrete parameters in Petri Nets. Section 3 presents the undecidability results. Section 4 introduces subclasses of our parameterised models. Section 5 answers decidability results over those subclasses and underlines issues encountered with reachability. Section 6 concludes and points to future work.

Definitions

Notations N is the set of natural numbers. N * is the set of positive natural numbers and N ω is the classic union N ∪ {ω} where for each n ∈ N, n + ω = ω, ω -n = ω, n < ω and ω ≤ ω. Z is the set of integers. Let X be a finite set. 2 X denotes the powerset of X and |X| the size of X. Let V ⊆ N, a V-valuation for X is a function from X to V . We therefore denote V X the set of V-valuations on X. Given an alphabet Σ, we denote as Σ the union Σ ∪ { } where is the silent action. Given a set X, let k ∈ Z and x ∈ X, we define a linear expression on X by the following grammar:

λ ::= k | k * x | λ + λ.
Given a linear expression λ on X and a N-valuation ν for X, ν(λ) is the integer obtained when replacing each element x in X from λ, by the corresponding value ν(x).

Petri Nets and Marked Petri Nets

Definition 1 (Petri Net) A Petri Net is a 4-tuple N = (P, T, P re, P ost) where P is a finite set of places, T is a finite set of transitions, P re and P ost ∈ N |P |×|T | are the backward and forward incidence matrices, such that P re(p, t) = n with n > 0 when there is an arc from place p to transition t with weight n and P ost(p, t) = n with n > 0 when there is an arc from transition t to place p with weight n.

Given a Petri Net N = (P, T, P re, P ost), we denote P re(•, t) (also written • t) as the vector (P re(p 1 , t), P re(p 2 , t), ..., P re(p |P | , t)) i.e. the t th column of the matrix P re. The same notation is used for P ost(•, t) (or t • ).

Definition 2 (Marking) A marking of a Petri Net N = (P, T, P re, P ost

) is a vector m ∈ N |P | . If m ∈ N |P | is a marking, m(p i )
is the number of tokens in place p i . We can define a partial order over markings.

Definition 3 (Partial Order) Let N be a Petri Net such that N = (P, T, P re, P ost), let m and m be two markings of N . We define ≤ as a binary relation such that ≤ is a subset of

N |P | × N |P | defined by: m ≤ m ⇔ ∀p ∈ P, m(p) ≤ m (p) (1) Definition 4 (Marked Petri Net) A marked Petri Net (PN) is a couple S = (N , m 0 )
where N is a Petri Net and m 0 is a marking of N called the initial marking of the system.

An example of marked Petri Net is given in Figure 1.

p1 p2 p3 t2 2 t1 3 • (.) = t1 t2   1 1 0 2 0 0   p1 p2 p3
(.) • = t1 t2   0 0 3 0 0 1   p1 p2 p3 m0 =   2 0 0   Fig. 1. A Marked Petri Net

Operational Semantics

Augmenting Petri Nets with markings leads to the notion of enabled-transitions and firing of transitions. Given a marked Petri Net S, a transition t ∈ T is said enabled by a marking m when m ≥ P re(•, t).

Definition 5 (PN Semantics)

The semantics of PN is a transition system

S T = (Q, q 0 , →) where, Q = N |P | , q 0 = m 0 , →∈ Q × T × Q such that, m ti → m ⇔ m ≥ • t i m = m -• t i + t • i (2)
This relation holds for sequences of transitions:

-

m w → m if

Parametric Petri Nets

We would like to use less rigid modeling in order to model systems where some data are not known a priori. Therefore, in this subsection, we extend the previous definitions by adding a set of parameters P ar. Working with Petri nets and discrete parameters leads to consider two main situations: the first one involves parameters on markings, by replacing the number of tokens in some places by parameters, the second one involves parameters as weights. The same parameter can be used in both situations. Using parameters on markings can be easily understood as modeling an unfixed amount of resources that one may want to optimise. Let us consider a concrete example to illustrate parameterised weights. In a production line, we consider two operations: first, to supply raw material, we need to unpack some boxes containing an amount λ 1 of resources, as depicted in Figure 2, and at the end, we need to pack end products in boxes of capacity λ 2 , as in Figure 3. This is part of a whole packaging process that one may want to optimise. The level of abstraction induced by parameters permits to leave those values unspecified in order to perform an early analysis.

p1 p2 t λ1
• (.) = t1 t2   1 1 0 λ2 0 0   p1 p2 p3 (.) • = t1 t2   0 0 λ1 0 0 λ3   p1 p2 p3 Fig. 4. A Parametric Petri Net
Intuitively, a parametric Petri net is a Petri net where the number of tokens involved in a transition is parameterised as depicted in Figure 4.

Definition 8 (Parametric marking) Given a parametric Petri Net N P = (P, T, P re, P ost, P ar), a parametric marking is a |P |-dimensional vector µ of linear expressions on N ∪ P ar.

Modeling with parameters means using parameters over weights and markings rather than setting numeric values everywhere. Therefore we may also use a parametric initial marking. Definition 9 (parametric PN or PPN) A parametric marked Petri Net (PPN) is a couple, SP = (N P, µ 0 ) where N P is a Parametric Petri Net and µ 0 is the parametric initial marking of N P.

PPNs can be used to design systems where some parts have not been analysed or where we need to keep flexibility. We now need to define a way to instantiate classic Petri nets from our parametric marked Petri Nets, in order to define a semantics.

Definition 10 (Parametric Semantics) Let SP = (P, T, P re, P ost, P ar, µ 0 ) be a PPN, we consider the set of valuations N P ar . Let ν ∈ N P ar , we define ν(SP) as the PN obtained from SP by replacing each parameter λ ∈ P ar by ν(λ), its valuation by ν, i.e. ν(SP) = (P, T, P re , P ost , m 0 ) where ∀i ∈

[[1, |P |]], ∀j ∈ [[1, |T |]],
P re (i, j) = P re(i, j) if P re(i, j) ∈ N ν(P re(i, j)) if P re(i, j) ∈ P ar

P ost (i, j) = P ost(i, j) if P ost(i, j) ∈ N ν(P ost(i, j)) if P ost(i, j) ∈ P ar (4)

m 0 (i) = µ 0 (i) if µ 0 (i) ∈ N ν(µ 0 (i)) if µ 0 (i) is a linear expression on P ar (5)
A marked Petri Net is an instance of a parametric marked Petri net.

Parametric problems

We can define several interesting parametric problems on PPNs. In fact, the behaviour of a PPN is described by the behaviours of all the PNs obtained by considering all possible valuations of the parameters. It seems therefore obvious to ask, in a first time, if there exists valuations for the parameters such that a property holds for the corresponding instance and its dual, i.e., if every instance of the parametric marked Petri Net satisfies the property. Given a class of problem P (coverability, reachability,...), SP a PPN and φ is an instance of P, parameterised problems are written as follows:

Definition 11 (P-Existence problem) (E -P): Is there a valuation ν ∈ N P ar s.t. ν(SP) satisfies the property φ ?

Definition 12 (P-Universality problem) (U -P): Does ν(SP) satisfies the property φ for each ν ∈ N P ar ?

This paper focuses on reachability and coverability issues.

Definition 13 (Reachability) Let S = (N , m 0 ) = (P, T, P re, P ost, m 0 ) and m a marking of S, S reaches m iff m ∈ RS(S).

Definition 14 (Coverability) Let S = (N , m 0 ) = (P, T, P re, P ost, m 0 ) and m a marking of S, S covers m if there exists a reachable marking m of S such that m is greater or equal to m i.e.

∃m ∈ RS(S)s.t. ∀p ∈ P, m (p) ≥ m(p) (6)
We recall that reachability [START_REF] Mayr | An algorithm for the general petri net reachability problem[END_REF] and coverability [START_REF] Karp | Parallel program schemata[END_REF] are decidable on classic Petri nets. In the context of parametric Petri nets, coverability leads to two main problems presented previously, that is to say: the existence problem, written (E -cov) and the universal problem, written (U -cov). For instance, (U -cov) asks: "Does each valuation of the parameters implies that the valuation of the parametric P/T net system covers m ?" i.e.

m is U -coverable in SP ⇔ ∀ν ∈ N P ar , ∃m ∈ RS(ν(SP)) s.t. m ≥ m (7)
We can similarly define E -reach and U -reach for parameterised reachability.

Undecidability Results for the General Case

In their paper suming-up results of decidability for reset-nets and corresponding subclasses, Dufourd, Finkel and Schnoebelen noticed that "Reachability is known to become undecidable as soon as the power of Petri nets is increased" [START_REF] Dufourd | Reset nets between decidability and undecidability[END_REF], for instance, adding reset arcs [START_REF] Araki | Some decision problems related to the reachability problem for Petri nets[END_REF] or inhibitor arcs [START_REF] Jones | Complexity of some problems in Petri nets[END_REF] makes reachability undecidable. In this section, we focus on showing that adding parameters to PN leads to undecidability. More specifically, (U -cov) and (E -cov) are undecidable on PPNs.

As we will proceed by reduction to the halting problem (and counter boundedness problem) for counter machines to answer our problem, we first recall some definitions. A 2-Counters Machine has a pointer and a tape which contains finite number of instructions in three types: increment, decrement and zero-test. The pointer reads the tape to execute increment or decrement instructions sequentially. When the pointer reaches a zero-test instruction, then it will jump to a certain position on the tape and continue. Formally, it consists of two counters c 1 , c 2 , a set of states P = {p 0 , ...p m }, a terminal state labelled halt and a finite list of instructions l 1 , ..., l s among the following list:

increment: increase c k by one and go to next state, where k ∈ {1, 2} decrement: decrease c k by one and go to next state, where k ∈ {1, 2} zero-test: if c k = 0 go to state p j else go to state p l , where p j , p l ∈ P ∪ {halt} and k ∈ {1, 2}

We can assume without restriction that the counters are non negative integers i.e. that the machine is well-formed in the sense that a decrement instruction is guarded by a zero-test and that the counters are initialised to zero. It is well known that the halting problem (whether state halt is reachable) and the counters boundedness problem (whether the counters values stay in a finite set) are both undecidable as proved by Minksy [START_REF] Minsky | Computation: Finite and Infinite Machines[END_REF].

Theorem 1 (Undecidability of E -cov on PPN) The E -coverability problem for PPN is undecidable 1 .

Proof. We proceed by reduction from a 2-counters machine. Given a Minksy 2-counters machine M, we construct a PPN that simulates it, SP M , as follows.

-Each counter c i is modeled by two places C i and ¬C i . The value of the counter is encoded by the number of tokens in C i . -For each state p of P ∪ {halt} a 1-bounded place p is created in the net.

-The instructions of the previous definition are modeled by the transitions and arcs depicted in Figure 5. -A unique additional place π with an additional transition θ serves to initialise the net. The initial marking is composed of one token in π and one token in the place p corresponding to the initial state p of M.

Initially, only θ can be fired, which leads to the initial configuration of the machine (state p 0 and counters values null), with one token in p 0 , no tokens in C 1 and C 2 and a parameterised number of tokens in ¬C i . The value of this parameter will therefore represent the upper bound of the counter over the instructions sequence. We have to verify that each time m(C i ) + m(¬C i ) = λ. First we show that SP M simulates M by verifying the behaviour of each instruction: 1 We can be more accurate by specifying that we need at least 1 parameter used on 6 distinct arcs. The question remains opened for fewer parameterised arcs ... -Increment instruction: As C i models the counter, the transition C i + + adds one token in C i , removes one token from ¬C i and changes the current state by removing the token from p i and adding a token in p j . The error states is marked iff the incrementation instruction is performed whereas we have already reached the upper bound over the execution. This state will be useful for the second proof. -Decrement instruction: As C i models the counter, the transition C i -removes one token from C i , adds one token in ¬C i and changes the current state by removing the token from p i and adding a token in p j . We recall the machine is well-formed. -Zero Test: As C i models the counter, and as we know the sum of tokens available in C i and ¬C i , there is no token in C i iff there are λ tokens in ¬C i . According to this test the current state is updated by removing the token from p i and adding a token in p j or p k . The value of the counter is left unchanged.

E Coverability is undecidable : We will show that given a 2-counters machine M, (a) M halts (it reaches the halt state) iff (b) there exists a valuation ν such that ν(SP M ) covers the corresponding p halt place.

-(a) ⇒ (b) First, let us assume that M halts. As M halts, the execution of the machine is finite. On this execution the two counters are bounded by c lim1 and c lim2 . Let c lim be the maximum of those two values. Let ν be the valuation such that ν(λ) = c lim . By the previous explanation, SP M simulates M. Moreover, the valuation ν ensures that SP M does not reach a deadlock state where p error is marked. Therefore, when M reaches halt, SP M will add 1 token in p halt . So, a marking where there is one token in p halt is coverable. -(b) ⇒ (a) We proceed by contrapositive. Let us assume that M does not halt. We want to show that there is no valuation ν such that ν(SP M ) adds a token in p halt . Let us consider the two following distinct alternatives:

• If the counters are bounded along the execution, either the value of λ is less than the maximum value of the counters and error will be reached during some increment resulting in a deadlock, or the value of λ is big enough so that error is never marked, but, in this case, then, as the machine does not halt, it means that it does not reach halt. So there is no instruction that leads to halt in M. Therefore, according to the previous explanation, there is no transition that adds a token in p halt . • If at least one counter is not bounded, then for any given valuation ν,

we will reach an instruction inc(c i ), where i is 1 or 2, and c i = ν(λ). Therefore, a token will be added in p error leading to a deadlock. So SP M will not cover a terminal state.

The undecidability of the halting problem on the 2-counters machine gives the undecidability of the E -coverability problem.

Theorem 2 (Undecidability of U -cov on PPN) The U -coverability problem for PPN is undecidable.

Proof. U Coverability is undecidable:

We proceed by reduction from a 2-counters machine. We use the same construction as in the previous proof. We denote m error the marking were m error (p) = 0 for each p ∈ P except m error (p error ) = 1. We will show that given a 2-counter machine M, (a) the counters are unbounded along the instructions sequence of M (counters boundedness problem) iff (b) for each valuation ν, ν(SP M ) covers the m error .

-(a) ⇒ (b) First, let us assume that on a given instruction sequence, one counter of M is unbounded. By the second alternative considered in the proof for E -cov we proved that for any valuation, a token will be added in p error . -(b) ⇒ (a) Reciprocally, by contrapositive, we want to show that if the counters are bounded, there exists a valuation ν such that ν(SP M ) does not cover m error . This comes directly from the previous proof. As the counters are bounded along the instructions sequence, we consider a valuation ν such that ν(λ) = c lim where c lim is an upper bound of the values of the counters. By construction, there is no possibilities to add a token in p error , otherwise, it means that SP M took an incrementation transition meaning that c lim is not an upper bound.

The undecidability of the counters boundedness problem on the 2-counters machine gives the undecidability of the U -coverability problem.

4 Subclasses of Parametric Petri Nets

Introducing Subclasses

On the one hand, our parametric model increases the modeling power of Petri nets but on the other hand, using parameters leads to complex models where properties become undecidable. In order to obtain parameterised models that are easier to analyse and therefore can be used in practice, we should reduce the power of modeling. We will therefore introduce some subclasses of the PPN in which we restrict the use of parameters to only markings, which could be used to model arbitrary number of identical processes, to only output arcs, which, we will see, is a bit more general or to only input arcs, which could model synchronizations among arbitrary numbers of identical process, and finally some combinations of those.

The following subclasses have therefore a dual interest. From a modeling point of view, restrict the use of parameters to tokens, output or input can be used to model concrete examples such as respectively processes or synchronisation of a given number of processes. From a theoretical point of view, it is interesting to introduce those subclasses of PPN in a concern of completeness of the study.

Definition 15 (P-parametric PN) A P-parametric marked Petri Net (P-PPN), SP = (N P, µ 0 ) where N P is a Parametric Petri Net such that P re and P ost ∈ N |P |×|T | and µ 0 is a parametric marking of N P.

A P-PPN is a classic Petri net with a parametric initial marking.

Definition 16 (T-parametric PN) A T-parametric Petri Net (T-PPN),

SP = (N P, m 0 ) where N P is a Parametric Petri Net and m 0 is a marking of N P Intuitively, using parameters on outputs means we will create parametric markings. To complete this study, we can extract a subclass in which parameters involved in the Pre matrix and parameters involved in the Post matrix correspond to disjoints subsets of parameters. i.e. par(P re) ∩ par(P ost) = ∅ where par is the application that maps to the set of parameters involved in a matrix (or a vector). We call this subclass distinctT-PPN2 . We can even refine the subclass of distinctT-PPN by considering the two distinct classes of Pre-Tparametric PPN (preT-PPN), where P ost ∈ N |P | and Post-T-parametric PPN (postT-PPN), where P re ∈ N |P | .

As we introduced several subclasses, it is interesting to study whether one of this subclass is more expressive than the other. We will show that P-PPN and postT-PPN are related. Therefore, we introduce here some useful definitions. Our translations add silent actions that detail the beahviour of the Petri nets. Therefore, we introduce a labelling function Λ from the set of transitions T to → m depending on the context3 . For instance, m * → m means that m leads to m by using zero or more internal -transitions. Given two markings m and m we write:

m α → m ⇔ m * → α → * → m with α = (8)
Definition 17 (Weak-Simulation) Given two labelled marked Petri nets,

S 1 = (P 1 , T 1 , F 1 , Λ 1 , Σ , m 0 1 ) and S 2 = (P 2 , T 2 , F 2 , Λ 2 , Σ , m 0 2 ), a binary relation R ⊆ N |P1| × N |P2| is a simulation if ∀(m 1 , m 2 ) ∈ R ⇔ ∀α ∈ Σ and m 1 s.t. m 1 α → m 1 , ∃m 2 s.t. m 2 α → m 2 and (m 1 , m 2 ) ∈ R (9)
If we can find a weak-simulation R ⊆ N |P1| ×N |P2| such that (m 0 1 , m 0 2 ) ∈ R we say that S 2 weakly simulates S 1 , which means intuitively that S 2 can match all the moves of S 1 . Moreover if we can find another weak-simulation R ⊆ N |P1| × N |P2| such that S 1 weakly simulates S 2 , we say that S 1 and S 2 are weakly co-similar.

Definition 18 (Weak-Bisimulation) Given two labelled PN,

S 1 = (P 1 , T 1 , F 1 , Λ 1 , Σ , m 0 1 ) and S 2 = (P 2 , T 2 , F 2 , Λ 2 , Σ , m 0 2 ), a binary relation R ⊆ N |P1| ×N |P2| is a weak-bisimulation 4 if ∀(m 1 , m 2 ) ∈ R ⇔          -∀α ∈ Σ and m 1 s.t. m 1 α → m 1 there is m 2 s.t. m 2 α → m 2 and (m 1 , m 2 ) ∈ R -∀α ∈ Σ and m 2 s.t. m 2 α → m 2 there is m 1 s.t. m 1 α → m 1 and (m 1 , m 2 ) ∈ R (10)
Two labelled Petri Nets S 1 and S 2 are weakly bisimilar if there is a weak bisimulation relating their initial markings. In the sequel, every transition called θ is mapped to by Λ whereas for a transition called t, Λ(t) = t. If the original PPN, SP = (P, T, P re, P ost, P ar, Λ, µ 0 ), has a set of transition T and T denotes the set of transition of the constructed PPN, SP = (P , T , P re , P ost , P ar, Λ , µ 0 ) then T = T ∪ Θ with T ∩ Θ = ∅. For each t ∈ T , Λ(t) = t and for each θ in Θ, Λ(θ) = .

Translating P-PPN to postT-PPN

In order to simulate the behaviour of parameterised places, we translate those places in a parameterised initialisation process that needs to be fired before firing any other transitions in the net. The idea relies on using a new place π and a new transition θ enabled by this place, such that θ • initializes a P-PPN, as showed in Figure 7. We define the initial marking m 0 = (0, ..., 0, 1) i.e. ∀p ∈ P , m 0 (p) = 0 and m 0 (π) = 1. We will show that SP and SP are weakly-bisimilar by showing that each behaviour of SP can be done in SP if we begin by firing θ and reciprocally. Note that each path in SP = (P, T, P re, P ost, P ar, Λ, µ 0 ) can be done in SP = (P , T , P re , P ost , P ar, Λ , m 0 ) by adding θ at the beginning. And reciprocally, each path in SP begins by θ so is written θ.w where w is a path in SP.

Proof. Let ν ∈ N P ar a valuation of the parameters. We want to show that ν(SP) and ν(SP ) are weakly bisimilar. Let ν(µ 0 ) be the parametric initial marking of ν(SP) and ν(m 0 ) = m 0 the initial marking of ν(SP ). The only transition firable from m 0 is θ and m 0 θ → ν(µ 0 ) as shown in Figure 7. From ν(µ 0 ), SP and SP are isomorphic. So ν(SP 1 ) and ν(SP 2 ) are weakly-bisimilar.

Those results underline that using parameters on outputs is more powerfull than using parameters on markings. We can conclude that T-PPN are more expressive than PPN.

Translating postT-PPN to P-PPN

We will show that from a postT-PPN, SP 1 = (P 1 , T 1 , P re 1 , P ost 1 , P ar 1 , Λ 1 , m 0 1 ) we can construct a P-PPN, SP 2 = (P 2 , T 2 , P re 2 , P ost 2 , P ar 2 , Λ 2 , µ 0

2 ) that weaklysimulates the behaviours of the postT-PPN. Reciprocally, the postT-PPN also weakly-simulates the behaviours of the P-PPN built.

For each transition t and place p such that the arc (t, p) is weighted by a parameter, we construct the net depicted in Figure 8 which replace this arc5 . Therefore, T 1 ⊆ T 2 . As previously, we introduce two labelling functions Λ 1 and Λ 2 from T 1 (resp. T 2 ) to T such that, for each t ∈ T 1 , Λ 1 (t) = Λ 2 (t) = t and Λ 2 (t) = otherwise (i.e. for each t ∈ T 2 \T 1 ). Lemma 4 ∀ν ∈ N P ar , ν(SP 1 ) and ν(SP 2 ) are weakly cosimilar.

Proof. We will prove the 2 weak-simulations.

-∀ν ∈ N P ar , ν(SP 2 ) simulates ν(SP 1 ). Let us consider ν ∈ N P ar , ν(SP 1 ) has the following behaviour: each time t is fired, ν(λ) tokens are created in p. In SP 2 , it is possible to generates ν(λ) tokens in p after firing the sequence t θ

ν(λ) t,p,1 θ t θ ν(λ)
t,p,2 , labeled t * . Moreover, this sequence resets the sub-net constructed for the weak-simulation. As the other transitions of the network are not affected, monotony gives directly the weak-simulation. -∀ν ∈ N P ar , ν(SP 1 ) simulates ν(SP 2 ). Reciprocally, a marking with ν(λ) tokens in p allows to simulate the behaviours of every marking such that m(p) ≤ ν(λ) according to monotony therefore, the reachable markings induced by creating less than ν(λ) tokens in SP 2 are simulated by the one with ν(λ) tokens, and therefore by SP 1 . As the other transitions of the network are not affected, monotony gives directly the weak-simulation.

Therefore, SP 1 and SP 2 are weakly co-similar.

Remark 1. This is not a weak bisimulation. Indeed, if SP 2 adds 3 tokens in p (leading to a marking m 2 ) whereas SP 1 adds ν(λ) = 4 tokens in p (leading to a marking m 1 ). Then any transitions needing more than 3 tokens could only be fired from m 1 in SP 1 only. Here the two simulations relations are not reciprocal: m 1 would simulates m 2 but m 2 would not.

Decidability Results

We will now consider the parameterised properties defined in Section 2 and the different subclasses of parameterised models of Section 4. Table 1 sums up the results that we present in this section.

Study of Parameterised Coverability

The easiest proofs rely on monotony. Indeed, some instances simulate other instances. We recall that the zero valuation (written 0) is the valuation that maps every parameter to zero.

Lemma 5 Decidability of U -coverability on postT-PPN (resp. P-PPN) can be reduced to a test with the zero valuation.

Proof. For postT-PPN and P-PPN, the zero valuation is the one allowing the lowest amount of behaviours for coverability i.e. it is the most restrictive valuation for coverability. Indeed, considering a marking m that we try to cover, m is U -coverable if and only if there is a firing sequence w such that m 0 w → m1 ≥ m in the 0-instanced postT-PPN (or P-PPN). Formally, given a postT-PPN or a P-PPN SP and a marking m, we have: ∃ν s.t. m is not coverable in ν(SP) iff m is not coverable in 0(SP) Indeed, for any valuation ν we can fire w in the ν-instanced PPN, leading to a marking m2 ≥ m1 by monotony. Moreover, on the instance of a PPN (i.e. on a PN), the coverability is known decidable, so we can answer to the problem on the zero instanced postT-PPN (or P-PPN). If the answer is no, then we have found a counter example. Else, monotony directly implies that using a greater valuation ν will provide at least behaviours covering the current ones. The winning behaviour that allowed to answer yes for the zero-instance will still works on this ν-instance. So every instance will satisfy the coverability.

Therefore we can claim that U -cov is decidable on postT-PPN and P-PPN. Let us consider E -cov for the same subclasses.

Theorem 6 E -cov is decidable on P-PPN.

Proof. Decidability of E -cov on P-PPN:

We consider a P-PPN, SP 1 . We will now build a PN S 2 with token-canons that will supply the parameterised places of SP 1 as depicted in Figure 9. Each tokencanon consists in two places π p , π p and two transitions θ p , θ p . θ p supplies p of S 2 . Moreover, each transition of SP 1 is added as an input and an output of π p , meaning that the net is blocked as long as every θ p has not been fired. This is repeated for each place initially marked by a parameter. We initialize S 2 with 1 token in each π p . So for each valuation ν of SP 1 , firing the sequence θ ν(λp) p θ p for each parameterised place p leads to a marking m 2 equals to the valuation of the initial marking of SP 1 . Moreover, the θ-transitions added have been fired, so every π p is marked. The two nets have now the same behaviour. This shows that S 2 simulates any valuation of SP 1 . Therefore, the existence of a valuation such that a given marking is covered can be reduced to the coverability of the same marking (completed with 0 for each π p and 1 for each π p added) which is known decidable as a classic coverability problem on an unbounded Petri net. Proof. Decidability of E -cov on postT-PPN: We proved in previous section that postT-PPN and P-PPN are weakly-cosimilar. Therefore, given a postT-PPN we can built a P-PPN which is weakly-co-similar. Moreover, as coverability can be reduced to firing transition (by adding an observer transition), weak-simulation holds coverability. Theorem 6 gives us the decidability.

Theorem 8 E -cov is decidable for preT-PPN.

Proof. E -cov for the preT-PPN is decidable: Let us consider a preT-PPN and a marking m that we try to cover. For an input transition with a weight of zero, we do not require the input place to be marked. Therefore, in terms of input parameters, by monotony, the zero valuation is the most permissive one for firing. Thus, there is at some valuation a firing sequence w such that m 0 w → m 1 ≥ m if and only if we can fire w in the 0-instanced one, leading to a marking m 2 ≥ m 1 . Formally, given a preT-PPN SP, we have:

m 0 w → m 1 ≥ m in ν(SP) iff m 0 w → m 2 ≥ m in 0(SP) with m 2 ≥ m 1
Informally, it means that the zero instance of the preT-PPN has the greatest amount of behaviours (in terms of coverability). Therefore it is the one which is necessary and sufficient to satisfy the E -cov of m, meaning that if it does not satisfy the property, monotony implies that any instance of the preT-PPN will not satisfy either. If the 0-instanced net covers m, we have a witness for the E -cov.

Corollary 9 E -cov is decidable for distinctT-PPN.

Proof. E -cov for the distinctT-PPN is decidable: As we can create a partition over P ar between P ar P re and P ar P ost , respectively sets of parameters involved on inputs and outputs which are disjoint. We can consider the partial valuation 0 |P ar P re , which maps every parameter of P ar P re to 0. We therefore get a postT-PPN on which the problem is decidable. Moreover, the post-PPN built is the one with the greatest amount of behaviours for coverability as explained previously. Considering that, if we cannot find any instance of this postT-PPN satisfying the property, we cannot find any instance of this distinctT-PPN satisfying it either.

Study of Parameterised Reachability

In classic Petri nets decidability of reachability certainly implies decidability of coverability. Indeed, given a marked Petri Net and a coverability problem, we can construct another marked Petri Net over which the previous coverability problem is equivalent to a reachability problem. Actually, with notations of Fig- It is clear that the same can be done for P P N , which implies that decidability of E -reachability implies decidability of E -coverability and decidability of U -reachability implies decidability of U -coverability. Section 3 provides therefore the undecidability of (E -reach) and (U -reach) in the general case of P P N .

Theorem 10 E -reach is decidable on P-PPN.

Proof. We can trivially adapt the conclusion of the proof of Theorem 6. We keep the same construction: the existence of a valuation such that a given marking is reached can be reduced to the reachability of the same marking (completed with 0 for each π p and 1 for each π p added) which is known decidable as a classic reachability problem on an unbounded Petri net.

Nevertheless, for the other subclasses, the decidability of reachability is more complex. Intuitively, increasing the valuation used to instanciate a preT-PPN (resp. a postT-PPN) leads to disable (resp. enable) transitions, i.e. the coverability of a marking, but this is not sufifcient to deduce the exact number of tokens involved, i.e. reachability. It is obvious that using the 0-valuation leads to enable the firing of t in any case, so it allows to cover any amount of tokens in p 2 . In Figure 11(a), the coverability set is CS 0 = {m|m ≤ (2, 1, ω)}. On the other hand, increasing the valuation leads to potentially disable t. We will therefore reduce the coverability set as we strengthen the pre-condition to fire t: in Figure 11 Equivalent observations rise from the study of Figure 12. When increasing the valuation, we may fire at least the same transitions, therefore, the coverability set is increasing: Figure 12(a) can cover any markings lower or equal to (2, 0) and can reach the set {(2, 0), (1, 0), (0, 0)} whereas Figure 12(b) can cover markings lower or equal to (2, 0),(1, 1) or (0, 2) but can reach the set {(2, 0)(1, 1)(0, 2)}.

Conclusion

Main results

In this paper, we have introduced the use of discrete parameters and suggested parametric versions of the well known reachability and coverability problems. The study of the decidability of those problems leads to the results summed up in Figure 13 for coverability (Classes inside a dashed outline are decidable for the two corresponding parametric coverability problems). We recall that the other results are presented in Tab 1.

Future work

If we have strong intuitions for several empty cases such as decidability of U -Coverability on preT-PPN and distinctT-PPN which would join the intuition that using the same parameters on inputs and outputs considerably increases the power of modeling of classic Petri nets, a deeper study should be carried to answer the decidability of Parametric-Reachability for instance. Being able to treat these parameterised models constitutes a scientific breakthrough in two ways:

-It significantly increases the level of abstraction in models. We will therefore be able to handle a much larger and therefore more realistic class of models. -The existence of parameters can also address more relevant and realistic verification issues. Instead of just providing a binary response on the satisfaction or not of an expected property, we can aim tosynthetise constraints on the parameters ensuring that if these constraints are satisfied, the property is satisfied. Such conditions for the proper functioning of the system are essential information for the designer.

  w is the empty word and m = m m wt → m if ∃m , m w → m ∧ m t → m where w ∈ T * and t ∈ T . Definition 6 (Reachability set) Given a PN, S = (N , m 0 ), the reachability set of S, RS(S) is the set of all reachable markings of S i.e. RS(S) = {m | ∃w ∈ T * , m 0 w → m}

Fig. 2 .Fig. 3 .

 23 Fig. 2. Unpacking raw material

Fig. 5 .

 5 Fig. 5. Modeling a counter with PPN

Fig. 6 .

 6 Fig. 6. Subclasses of PPN

Fig. 7 .

 7 Fig. 7. From P-PPN to postT-PPN

Fig. 8 .

 8 Fig. 8. From postT-PPN to P-PPN

Fig. 9 .

 9 Fig. 9. From PPN to PN

Fig. 11 .

 11 Fig. 11. Several instances of a preT-PPN

  Figure11presents a preT-PPN. It is obvious that using the 0-valuation leads to enable the firing of t in any case, so it allows to cover any amount of tokens in p 2 . In Figure11(a), the coverability set isCS 0 = {m|m ≤ (2, 1, ω)}.On the other hand, increasing the valuation leads to potentially disable t. We will therefore reduce the coverability set as we strengthen the pre-condition to fire t: in Figure11(b), the coverability set is CS 1 = {m|m ≤ (2, 1, 0) ∨ m ≤ (1, 0, 1)} ⊆ CS 0 ,and in Figure 11(c), we have CS 2 = {m|m ≤ (2, 1, 0) ∨ m ≤ (0, 0, 1)} ⊆ CS 1 . Nevertheless, this strengthening of the pre-condition, does not imply general consequences in terms of reachability sets. Indeed, in Figure 11(a), the reachability set is {(2, 1, n)|n ∈ N}, whereas in Figure 11(b) we can reach {(2, 1, 0), (1, 0, 1)} and in Figure 11(c), we can reach {(2, 1, 0), (0, 0, 1)}.

Fig. 12 .

 12 Fig. 12. Several instances of a postT-PPN

Fig. 13 .

 13 Fig. 13. What is decidable among the subclasses ? (for coverability)

Table 1 .

 1 Decidability results for parametric coverability and reachability

		U -problem		E -problem
		Reachability Coverability Reachability Coverability
	preT-PPN	?	?	?	D
	postT-PPN	?	D	?	D
	PPN	U	U	U	U
	distinctT-PPN	?	?	?	D
	P-PPN	?	D	D	D

Studying the undecidability proof, it is relevant to think that using different parameters for the input and the output would reduce the modeling power.

Indeed, if we consider the alphabet A equals to the set of the transition T of the Petri Net, and L as the identity function, the two definitions are equivalent. Using labelling is more general and allows to introduce non deterministic behaviours.

There exists several definitions of bisimulation, for instance preserving deadlocks or epsilon-branching, but the one we use is sufficient for our purpose.

Notice that if several labeled arcs come from the same transition, some places and transitions of the Figure8should be duplicated according to indices

Acknowledgement

We wish to thank the anonymous reviewers, who helped us to improve the paper by their suggestions.

* Work partially supported by ANR project PACS (ANR-14-CE28-0002) and Pays de la Loire research project AFSEC.