Benoît Barbot

Nicolas Basset

Artifact 2023

Adding probabilities to timed automata enables one to carry random simulation of their behaviors and provide answers with statistical guarantees to problems otherwise untractable. Thus, when just a timed language is given, the following natural question arises: What probability should we consider if we have no a priori knowledge except the given language and the considered length (i.e. number of events) of timed words?

The maximal entropy principle tells us to take the probability measure that maximises the entropy which is the uniform measure on the language restricted to timed word of the given length (with such a uniform measure every timed word has the same chance of being sampled). The uniform sampling method developed in the last decade provides no control on the duration of sampled timed words.

In the present article we consider the problem of finding a probability measure on a timed language maximising the entropy under general linear constraints on duration and for timed words of a given length. The solution we provide generalizes to timed languages a well-known result on probability measure over the real line maximising the Shannon continuous entropy under linear constraints. After giving our general theorem for general linear constraints and for general timed languages, we concentrate to the case when only the mean duration is prescribed (and again when the length is fixed) for timed languages recognised by deterministic timed automata. For this latter case, we provide an efficient sampling algorithm we have implemented and illustrated on several examples.

Introduction

Since their introduction in the early 90's, Timed Automata (TA) are extensively used to model and verify the behaviors of real-timed systems and thoroughly explored from a theoretical standpoint. Several lines of research have been developed to add probabilities to these models. The two main motivations for this are (i) modelling systems that both exhibit real-time and probabilistic aspects, for example network protocols where delays are chosen at random to resolve conflicts, as in CSMA-CD (see e.g. [START_REF] Norman | Model checking for probabilistic timed automata[END_REF][START_REF] Bertrand | Stochastic timed automata[END_REF]); (ii) statistical model checking of TA with the claim of replacing a prohibitively expensive exhaustive verification of the system by a thorough random simulation of the TA with statistical guarantees (see e.g. [START_REF] Budde | A statistical model checker for nondeterminism and rare events[END_REF] and reference therein).

For statistical model checking (or any other approach based on statistics) to make sense, the probability distribution defined on the runs of the TA has to be clearly given, which is not always the case as pointed in [START_REF] Bohlender | A review of statistical model checking pitfalls on real-time stochastic models[END_REF][START_REF] Barbot | Uniform sampling for timed automata with application to language inclusion measurement[END_REF]. In the present article we follow a line of research initiated in [START_REF] Basset | A maximal entropy stochastic process for a timed automaton[END_REF][START_REF] Barbot | Uniform sampling for timed automata with application to language inclusion measurement[END_REF] focusing on Deterministic Timed Automata (DTA), where the aim is to give a constructive answer to the following question inspired by Jayne's maximal entropy principle [START_REF] Jaynes | Information Theory and Statistical Mechanics[END_REF]: What probability should we specify on the runs of a given DTA without any a priori knowledge? Another aim of this approach, which appears equivalent, is to get a sampler as uniform as possible of runs of the DTA, that is, a sampler that gives to runs of the same length the same (density of) probability. The article [START_REF] Basset | A maximal entropy stochastic process for a timed automaton[END_REF] was a first theoretical one that dealt with infinite timed words while [START_REF] Barbot | Uniform sampling for timed automata with application to language inclusion measurement[END_REF] gave more pragmatic algorithms and their implementation to sample timed words of a given finite length. These two probability measures maximize Shannon continuous entropy adapted to probability measures on finite and infinite timed words respectively. The algorithms in [START_REF] Barbot | Uniform sampling for timed automata with application to language inclusion measurement[END_REF] were later implemented in the tool Wordgen [START_REF] Barbot | Wordgen : A timed word generation tool[END_REF] and applied in the context of validation of CPS by generating input signals satisfying a specification given as a DTA [START_REF] Barbot | Falsification of cyber-physical systems with constrained signal spaces[END_REF][START_REF] Barbot | Generation of signals under temporal constraints for CPS testing[END_REF]. With this sampling method, one can choose the length of runs, that is, the number of events occurring in them, but not their duration.

In Section 3, we propose, as a main contribution, a maximal entropy theorem for general linear constraints on duration, that is, the expectations (over the timed words of a DTA of a given length) of some arbitrary constraint functions depending only on duration are prescribed. We were inspired by a classical maximal entropy theorem for real-to-real functions and classical Shannon continuous entropy (see the dedicated chapter of the textbook on information theory [START_REF] Cover | Information theory and statistics[END_REF]). As a second main contribution we propose in Section 4, a procedure for sampling finite timed words of fixed length with random duration such that the mean duration is prescribed. Besides these two main contributions, we introduce, in Section 4, the key concept of Laplace Transform of Volumes (LTV) which generalizes the volume functions of [START_REF] Asarin | Entropy of regular timed languages[END_REF][START_REF] Barbot | Uniform sampling for timed automata with application to language inclusion measurement[END_REF] with an extra parameter. As we will discuss in the conclusion (Section 6), we think that replacing these previous volume functions by LTVs can enable us to extend several results by adding a focus on duration. Last but not least, we implemented our algorithms by extending the tool Wordgen and in this article we provide several experiments in Section 5, one of which features a DTA with thousands of control states.

Before exposing our contributions, we recall preliminaries on timed languages and previous work on max-entropy sampling for DTA in Section 2. Due to space constraints, we move the proof of our results into an appendix.

Preliminaries

In this section, we recall definitions on timed languages, max-entropy probability measure on them and how to sample them.

General timed languages and their measure

Let Σ be a finite alphabet of events. A timed letter (t, a) is a couple of R + × Σ where t represents the delay before the event a happens. A timed word w is a sequence of timed letters. We denote by ε the empty timed word. For the sake of conciseness we often remove commas and parentheses and write

t 1 a 1 • • • t n a n for (t 1 , a 1 ) • • • (t n , a n ).
Such timed word is called of length n and of duration n i=1 t i denoted by θ(w). A timed language is a set of timed words. The universal language is the set of all timed words denoted by (R + × Σ) * . We are mainly interested in timed languages recognized by timed automata described in Section 2.2 below but a large part of our theory can be stated for more general timed language.

For a timed language L and a timed letter ta, we define (ta) -1 L the left derivative of L wrt ta as

(ta) -1 L = {w | taw ∈ L}.
Languages can be defined recursively via defining sub-languages [L] n , n ∈ N which are the restriction to L to words of length n.

[L] n = t a (ta).[(ta) -1 L] n-1 where the base case is [L] 0 = {ϵ} or [L] 0 = ∅. (1)
Example 1. Consider the timed language L = {t 1 at 2 a . . . t n a | ∀i ≥ 1, t i + t i+1 < 1}. This language satisfy (ta

) -1 L = {t 2 a . . . t n a | t 2 < 1 -t ∧ t i + t i+1 < 1} if t < 1 and is empty otherwise.
Timed language as a collection of sets of real-vectors Given a timed language L and n ∈ N, every untimed-word w = a 1 • • • a n ∈ Σ n can be seen as the label for the set

P L (w) = {(t 1 , . . . , t n ) ∈ R n | t 1 a 1 • • • t n a n ∈ L} which is possibly empty.
In the following we only consider timed language for which every P L (w) is a measurable set for the Lebesgue measure. In particular we mostly work with timed language for which every P L (w) is a union of polytopes but our general theorem applies for the general case of measurable sets.

A polytope in dimension n is a subset of R n defined as the set of points whose coordinates satisfy a finite conjunction of linear inequalities, that is, of the form n i=1 α i t i ≤ β. Note we consider non-necessarily bounded polytope e.g.

{t 1 , t 2 | t 1 ≤ 3 ∧ t 2 ≥ 1 ∧ t 1 + t 2 ≥ 3}.
Example 2. The polytopes corresponding to the language of Example 1 are depicted below with their respective volumes. Polytopes up to dimension 4 are displayed. For dimension 4 the projection of the polytope with t 1 = 1 is displayed. polytopes

t 1 t 1 t 2 t 3 t 1 t 2 t 3 t 4 t 2 t 3 t 1 = 1 words ε t 1 a t 1 at 2 a t 1 at 2 at 3 a t 1 at 2 at 3 at 4 a volumes 1 1 1 2 1 3 5 24
Integrating a function over a language, volume and entropy Given a timed language L, n ∈ N and f : L n → R, a real-valued function defined on L n , we use the following notation for the integral of f over L n .

Ln

f (w)dw = w=a1•••an∈Σ n (t1,...,tn)∈P L (w) f (t 1 a 1 • • • t n a n )dt 1 • dt n .
When f is non-negative this value is either a non-negative real or +∞. We say that two functions are equal almost everywhere if the set where they differ is of null measure, that is, Ln 1 f (w)̸ =g(w) dw = 0. In the rest of the paper we will just see as equals functions that are almost everywhere equals. Similarly when we say that a function f is a unique solution of a maximisation problem, it means that all functions almost-everywhere equal to f , and only them, are also a solution of the problem. These conventions will also apply to functions from R to R.

Volumes For a given n, L n is the formal union of subsets P L (w) of R n . The volume of L n denoted Vol(L n ) is the sum of volumes of these sets. When one is infinite then so is Vol(L n ). Equivalently it is just the integral of 1 over L n : Vol(L n ) = Ln 1dw. Volumes can also be characterised recursively by

Vol(∅) = 0, Vol({ε}) = 1, Vol(L n ) = a∈Σ ∞ 0 Vol([(ta) -1 L] n-1 )dt. ( 2
)
PDF on timed languages A probability density function (PDF) over L n is a function f non-negative for which Ln f (w)dw = 1. Given a PDF f , and a function g defined on L n , the expected value of g is denoted by E f (g) and defined by Ln g(w)f (w)dw. We will be mostly interested with the expected duration of timed words of a given language L and PDF f :

E f (θ) = Ln θ(w)f (w)dw.
Entropy of a PDF The entropy of a PDF f on L n is3

H(f ) = E f (-log 2 (f )) = - Ln f (w) log 2 f (w)dw, ( 3
)
This definition is the natural generalisation to timed languages of the Shannon continuous entropy (aka. Shannon differential entropy) for functions from R to R. The following max-entropy theorem, tells us that the uniform PDF (used in [START_REF] Barbot | Uniform sampling for timed automata with application to language inclusion measurement[END_REF] for uniform random sampling) is the unique PDF that maximises the entropy.

Theorem 1. Given a timed language L and n ∈ N such that Vol(L n ) < +∞, the maximal value of the entropy of a PDF on L n is log 2 (Vol(L n )). It is reached by a unique PDF on L n which the uniform PDF on L n : the constant function w → 1/Vol(L n ). This theorem will be a particular case of our main theorem (Theorem 2 of Section 3) where no constraint is given on duration.

Maximal entropy measure and uniform sampling for general timed languages Uniform sampling can be defined over general timed languages based on Eq. ( 2). Exact sampling in L of a word of length n is performed iteratively. When n is equal to 0 the sampling stops otherwise the next letter

a ∈ Σ is chosen with probability ∞ 0 Vol([(ta) -1 L]n-1)dt Vol(Ln)
. Next a delay t is sampled4 from the continuous distribution defined by the Probability Density function

t → Vol([(ta) -1 L]n-1) ∞ 0 Vol([(ta) -1 L]n-1)
. Then a timed word of length n -1 is sampled from the language (ta) -1 L. This scheme needs a practical way of computing PDF which will be the case for timed languages recognized by deterministic timed automata.

Languages recognized by DTA and their measures

In this part we restrict our attention to languages recognised by a DTA. For these languages, we can describe computation of the volume of the language with recursive equations on the structure of the DTA recognising the language.

Fig. 1: Examples of Deterministic Timed Automata

Timed automata A timed automaton (TA) A is defined as a tuple (Σ, X, Q, q 0 , F , ∆) where Σ is a finite set of events; X is a finite set of clocks; Q is a finite set of locations; q 0 is the initial location; F ⊆ Q is a set of final locations; and ∆ is a finite set of transitions. The finite set of clocks X is a finite set of non-negative real-valued variables . A guard is a finite conjunction of clock constraints. For a clock vector x ∈ [0, ∞[ X and a non-negative real t, we denote by x + t the vector x + (t, . . . , t). A transition δ = (δ -, a δ , g δ , r δ , δ + ) ∈ ∆ has an origin δ -∈ Q, a destination δ + ∈ Q, a label a δ ∈ Σ, a guard g δ and a reset function r δ determined by a subset of clocks B ⊆ X. To simplify notation r are overloaded to be both a subset of the clocks set and the function assigning 0 to clocks in the subset. Fig. 1a depicts a TA with two clocks x and y, two locations q 0 , q 1 which are final and two transitions. The transition from q 0 to q 1 is labelled by a is guarded by x < 1 and reset x while the transition from q 1 to q 0 is labelled by a is guarded by y < 1 and reset y. Other examples of TAs are given in Fig. 1b and Fig. 4.

A state s = (q, x) ∈ Q × [0, ∞[ X is
a pair of location and a clock vector. The initial state of A is (q 0 , 0). A timed transition is a pair (t, δ) of a time delay t ∈ [0, ∞[ followed by a discrete transition δ ∈ ∆. The delay t represents the time before firing the transition δ.

A run is an alternating sequence (q 0 , x 0 ) t1,δ1 ---→ (q 1 , x 1 ) . . .

tn,δn

---→ (q n , x n ) of states satisfying that q i is the successor of q i-1 by δ i , the vector x i-1 + t satisfies the guard g δ and x i = r δ (x i-1 + t), (q 0 , x 0 ) is the initial state and q n is a final location. This run is labelled by the timed word (t 1 , a 1 ) • • • (t n , a n ) where for every i ≤ n, a i is the label of δ i . The set of timed words that label all the runs is called the timed language of A. The TA of Fig. 1a recognises the language of Ex. 1.

A deterministic timed automaton (DTA) is a TA where for every location q, transitions starting from q have pairwise disjoint guards or different labels. All TA shown in this paper are DTA.

Max-entropy sampling for DTA In [START_REF] Barbot | Uniform sampling for timed automata with application to language inclusion measurement[END_REF][START_REF] Barbot | Generation of signals under temporal constraints for CPS testing[END_REF][START_REF] Barbot | Falsification of cyber-physical systems with constrained signal spaces[END_REF][START_REF] Barbot | Wordgen : A timed word generation tool[END_REF] algorithms were developed to compute the volume for languages of DTA with some restrictions. Given a DTA, (2) can be instantiated over its zone graph. The first step is to compute the forward-reachability zone graph. The second operation splits the zone graph such that, for any vertex of the graph, for each available transition δ, there exist two functions lb δ and ub δ of the clock vector x such that, for all t ∈ R + , x + t |= g δ is equivalent to t ∈ [lb δ (x), ub δ (x)]. Moreover the bounds lb δ (x) and ub δ (x) are of the form c -x where c ∈ N and x is a clock or zero. Details on the computation of the split operation can be found in [START_REF] Barbot | Uniform sampling for timed automata with application to language inclusion measurement[END_REF]. In the split zone graph equation (2) becomes:

v 0 (l, x) = 1 l∈F and v n (l, x) = δ -=l ub δ (x) lb δ (x) v n-1 δ + , r δ (x + t) dt (4)
Given n, v n (l, x) can be computed in polynomial time with respect to n and the split zone graph size which in the worst case can be exponentially large in the number of clocks. Given n and location l the functions x → v n (l, x) is a polynomial in x. This can be seen by a straightforward recursion since v 0 is a constant and the bound of the integrals to define v n+1 from v n are polynomials.

Since closed-form formulae for v n are efficiently computable, this provides an effective way of sampling using the procedure presented in Section 2.1.

More precisely the k th letter is randomly chosen in state (q, x) by chosing the transition δ = (q, a, g δ , r δ , q ′ ) labelling a with the discrete probability distribution

p k (δ | q, x) = ub δ (x) lb δ (x) v n-k-1 (q ′ , r δ (x + t))dt v n-k (q, x) (5)
and the delay with the PDF:

p k (t | a, q, x) = 1 t∈(lb δ ,ub δ ) v n-k-1 (q ′ , r δ (x + t)) ub δ (x) lb δ (x) v n-k-1 (q ′ , r δ (x + t))dt (6)
Approximate uniform sampling method are presented in [START_REF] Barbot | Uniform sampling for timed automata with application to language inclusion measurement[END_REF] to sample words of large length. One of such method is the receding sampling where to avoid computing the p k in ( 5) and ( 6) when k is close to a too large sampling length m, one use instead p min(n,k) for a n large enough but small compared to m (see [START_REF] Barbot | Uniform sampling for timed automata with application to language inclusion measurement[END_REF] for the details and formal statements).

Max-Entropy Theorem Under Linear Duration Constraints

In previous work on uniform sampling, constraint on duration could not be expressed. Here we are interested to express for instance that the mean and the variance of duration are equals to µ and ν, we write Ln θ(w)p(w)dw = µ and Ln θ 2 (w)p(w)dw = ν + µ 2 . More generally we are given m measurable functions f i : R ≥0 → R and constants a i ∈ R, i = 1..m, and we address the following max-entropy problem: Maximise H(p) under constraints Ln f i (θ(w))p(w)dw = a i for i ∈ {0, . . . , m}, [START_REF] Basset | Counting and generating permutations in regular classes[END_REF] where f 0 is the constant 1 and a 0 = 1, to add the constraints that p is a PDF.

Our solution given in the max-entropy theorem below (Theorem 2) is based on expressing this max-entropy problem on L n as a max-entropy problem for functions of the reals (that take the duration as argument). Before stating this theorem, we first need few definitions and Lemmas.

We say that a function f defined on L n depends only on duration if f = f • θ for some functions on the reals f , that is, for every w ∈ L n , f (w) = f (θ(w)). For a PDF f , "depending only on duration" can be rephrased as "being uniform at fixed duration": for every T , all the timed words of duration T have the same density of probability.

With Lemma 1 we show that integrating a function that depends only on duration, i.e. of the form f • θ, can be expressed as integrating f (T ) with the duration T as the variable of integration multiplied by a weight denoted V L n (T ).

This weight V L n (T ) is the n -1-dimensional5 volume of timed-word of length n restricted to duration T defined by

V L n (T ) = w1•••wn∈Σ n (R ≥0 ) n-1 1 t1w1•••tn-1wn-1(T -t1-•••-tn-1)wn∈L dt 1 • • • dt n-1 . (8)
We will denote V L n (T ) by V n (T ) when L is clear from the context. We will also use the following notation:

L n,T = {w ∈ L n | θ(w) = T } and consider (n -1)-dimensional integral on it: L n,T f (w)dw = w1•••wn∈Σ n (R ≥0 ) n-1 1 w∈L n,T f (w)dt 1 • • • dt n-1 .
In particular

V L n (T ) = L n,T 1dw and hence w → 1/V L n (T ) is the uniform PDF on L n,T Lemma 1. If f = f • θ then Ln f (w)dw = +∞ 0 f (T )V L n (T )dT Remark 1.
We give few cases of interest for this Lemma.

1. If f (w) = 1, then we get Vol(L n ) = +∞ 0 V n (T )dT 2. If f (w) = 1 Vol(Ln) , then T → Vn(T ) Vol(Ln) is a PDF on reals. 3. If f (w) = θ(w)
Vol(Ln) then Ln θ(w)

Vol(Ln) dw = +∞ 0
T Vn(T ) Vol(Ln) dT is the mean duration for the uniform distribution on L n .

A straightforward consequence of Lemma 1, called Lemma 2 below, is that the max-entropy problem is equivalent to a max-entropy problem for functions defined on the reals. In this Lemma p ≪ V n means that ∀T ∈ R ≥0 , V n (T ) = 0 ⇒ p(T ) = 0, and

H Vn (q) = - +∞ 0 q(T ) log 2 q(T ) V n (T ) dT.
Lemma 2. For every PDF of the form p • θ, the function p R :

T → V n (T )p(T ) is a PDF such that H Vn (p R ) = H(p • θ). Moreover p • θ is a solution of (7) iff p R is a solution of Maximise H Vn (p) s.t. +∞ 0 f i (T )p(T )dT = a i for i ∈ {0, . . . , m} and p ≪ V n . (9)
With Lemma 3 we show that given any PDF, one can always find another PDF with higher or equal entropy that depends only on duration. Theorem 2 (Maximal entropy theorem on L n with integral constraints on duration). Given the max-entropy problem (7) with its constraints functions f i and constants a i . If one find constants λ i , (0 ≤ i ≤ m) such that the function p * (w) = exp (λ 0 + m i=1 λ i f i (θ(w))) is a PDF that satisfies the constraints, then the problem admits a unique solution which is p * . Proof. Let p * and λ i as above so that p * satisfies the constraints, then we have to prove that H(p * ) is maximal and unique for this property. First, Lemma 3 implies that we only have to consider PDF q of the form q = q • θ. We show that such PDF q satisfies H(q) ≤ H(p * ) with equality iff q = p * . This is equivalent to show that H Vn (q R ) ≤ H Vn (p R ) with equality iff q R = p R , with p R = p.V n and q R = q.V n since by Lemma 2, H Vn (p R ) = H(p * ) and H Vn (q R ) = H(q).

We adapt a classical proof based on Kulback-Lebler divergence that can be found in [START_REF] Cover | Information theory and statistics[END_REF]. The Kullback-Leibler divergence from p R to q R is the quantity

D(q R ||p R ) = +∞ 0 q R (T ) log q R (T )
p R (T ) dT which is always non-negative, and null iff p R = q R . We will show that D(q

R ||p R ) = H Vn (p R ) -H Vn (q R ) and thus H Vn (p R ) = H Vn (q R ) will be equivalent to p R = q R .
We introduce V n (T ) using the fact that log 2 (q R /p R ) = log 2 q R (T )

Vn(T ) -log 2 p R Vn(T ) : D(q R ||p R ) = +∞ 0 q R (T ) log 2 q R (T ) V n (T ) dT - +∞ 0 q R (T ) log 2 p R (T ) V n (T ) dT
The first integral is -H Vn (q R ), hence it remains to prove that

H Vn (p R ) = -q R (T ) log 2 p R (T )
Vn(T ) . We recall that p R (T )

Vn(T ) = p(T ) = exp ( m i=0 λ i f i (T )), thus +∞ 0 q R (T ) log 2 p R (T ) V n (T ) = 1 ln 2 +∞ 0 q R (T ) m i=0 λ i f i (T ) dT = 1 ln 2 m i=0 λ i +∞ 0 q R (T )f i (T )dT.
Since q R satisfies the constraints this quantity is equal to 1 ln 2 m i=0 λ i a i The same reasoning holds for p, so we can conclude the proof with the equality:

H Vn (p R ) = - 1 ln(2) m i=0 λ i a i = - +∞ 0 q R (T ) log 2 p R (T ) V n (T ) dT.
Theorem 1 is a specialisation of Theorem 2 where there is no constraint on duration. Indeed the function has to be searched as a constant e λ0 with the unique constraint that Ln e λ0 dw = 1, that is, e λ0 = 1/Vol(L n ). As there is no constraint on duration the volume must be finite for this theorem to apply.

Max-entropy theorem with prescribed mean duration

In this section we describe and see how to compute the max-entropy PDF when the mean duration is prescribed. So we will use Theorem 2 with f 1 being the identity function and explain the normalising constant (link between λ 0 and λ 1 ).

Theorem 3 (Maximal entropy theorem for measures on L n with prescribed mean duration). Given a timed language L, length n, duration T mean . If there exist probability measures p that satisfy the constraint E p (θ(w)) = T mean , then there is a unique one p * satisfying this constraint that maximizes the entropy. It is given by

p * (w) = e -sθ(w) v L n,s
where the normalising constant v L n,s is defined by

v L n,s = Ln e -sθ(w) dw = +∞ 0 e -sT V L n (T )dT ( 10
)
with s the unique real such that

1 v L n,s ∂v L n,s ∂s = T mean .
The normalising constant v L n,s defined in equation ( 10) can be interpreted as a Laplace transform of the function V n and hence we call it the Laplace Transform of Volumes (LTV) and s is called the Laplace parameter. In the next section we will propose efficient computation of it which will be the base of a sampling algorithm. As shown above by tuning the Laplace parameter s we can control the mean duration which is defined wrt. the LTV and its derivative. Controlling the variance could be done by adding an extra parameter. Efficient sampling for this latter case is left for future work, and we focus on fixing only the mean duration so working only with the LTV. Once this done, we can characterise the variance (without prescribing it) with the LTV and its derivatives.

Proposition 1 (Characterization of the variance wrt. LTV and its derivatives). Let p * be the PDF given in Theorem 3 and let V ar p * (θ(w)) = E p * (θ(w) 2 ) -E p * (θ(w)) 2 the variance of the duration of timed words sampled with this probability. Then

V ar p * (θ(w)) = ∂ 2 v L n,s ∂s 2 - 1 v L n,s ∂v L n,s ∂s 2 .
Remark 2. Theorem 1 is again a special case. It suffices to take s = 0. We get in addition, a characterisation of the mean of the duration and with Proposition 1 its variance.

The LTV v n can be characterized via a recursive definition:

Proposition 2 (Recursive definition of v n ). v L n,s = a∈Σ +∞ 0 e -st v (ta) -1 L n-1,s dt (11)
This recursive definition is a step towards dynamic programming computation that will be fully possible now when we focus on DTA.

Computing LTV and max-entropy sampling for Timed Automata

Theorem 3 tells us the form of the maximal entropy PDF when a mean duration constraint is imposed. In this section we focus on how to sample this PDF for language recognized by a DTA using the LTVs for languages starting on states of this DTA. This PDF is then used to sample its language.

Computation of LTV as exponential Polynomials for DTA In this section, we describe how LTV can be computed effectively from a timed automaton. This is done by computing LTV recursively and by showing that all computations are performed over exponential polynomials (Def. 1) for which the computation of integral is effective. Here we find a suitable generalisation of the volumes functions used in [START_REF] Asarin | Entropy of regular timed languages[END_REF][START_REF] Basset | A maximal entropy stochastic process for a timed automaton[END_REF][START_REF] Barbot | Uniform sampling for timed automata with application to language inclusion measurement[END_REF] and recall in Section 2. In a nutshell, we multiply by e -st the function which is integrated over the next transition with the delay as integration variable.

In the following we assume that a DTA in split form is given and for every length n, parameter s and state (l, x) we denote by v n,s (l, x) the LTV of the language starting from (l, x) that is v n,s (q, x) = v L (l,x) n,s .

Definition 1 (Exponential Polynomials). Given a variable s and a sequence of variable X = (X i ) n i=1 , we call exponential polynomials, expressions EP (s, X) such that : there exists a finite set S ⊂ {0, 1, . . . , n} × N and a polynomial P i,k for each element of S with P i,k a polynomials over X ∪ { 1 s } with the the convention that X 0 = 0; and EP (s, X) is written in the form

EP (s, X) = (i,k)∈S P i,k 1 s , X e s(Xi-k)
Proposition 3. For every location q and length n, x → v n,s (q, x) is an exponential polynomials. It can be computed in polynomial time using dynamic programming from the following recursive equations:

v 0,s (l, x) = 1 l∈F and v n,s (l, x) = δ -=l ub δ (x) lb δ (x) v n-1,s δ + , r δ (x + t) e -st dt. ( 12
)
Random sampling using the LTV

The sampling follows the same line as in for the unconstrained case (Section 2.1) where the probability distributions for discrete and continuous choice ( 5) and ( 6) are replaced by

p k,s (a | q, x) = ub δ (x) lb δ (x) v n-k-1,s (q ′ , r δ (x + t))e -st dt v n-k,s (q, x)
; and ( 13)

p k,s (t | a, q, x) = 1 (lb δ ,ub δ ) v n-k-1,s (q ′ , r δ (x + t))e -st ub δ (x) lb δ (x) v n-k-1,s (q ′ , r δ (x + t))e -st dt . ( 14
)
5 Experiments

We have implemented our approach in the tool Wordgen [START_REF] Barbot | Wordgen : A timed word generation tool[END_REF], which required developing a data structure for exponential polynomials, implementing the LTV computation and the estimation of parameters s. These developments are freely available with the GPLv3 licence. This section contains experiments on small timed automata (Example 3 and 4) and a case study on a larger automaton (Example 5).

Example 3. We compute the LTVs of the language defined in Example 1 recognized by the timed automaton depicted in Figure 1a. After computing the split zone graph, the number of locations is still 2. We show the LTVs computed for small n in both of these locations and in the initial one in the following table.

(q, x)\n 0 1 2 (q 0 ,(x,y)) 1

1-e -s(1-x)) s

1-e -s(1-x)) s 2

+ (x-1) s e -s (q 1 ,(x,y)) 1

1-e -s(1-y) s

1-e -s(1-y)) s 2

+ (y-1) s e -s If we restrict to timed words of length 2, sampling with the parameter s = 0 (using Taylor expansion) provides a uniform distribution in the triangle. The expected duration is 1 v2,s(q0,(0,0)) ∂v2,s ∂s (q 0 , (0, 0)). For s ̸ = 0 it is 2+2s+s 2 -2e s s+s 2 -se s . Using Taylor expansions in s = 0 of both the numerator and the denominator one can show that the limit when s → 0 is 2 3 . Figure 2 shows plots of the sampling from this language with different mean durations. We observe a shift of the concentration of points along the axis y = x. Note that the time duration of 0.9 is obtained with a negative value of s. This is allowed when all clocks are bounded and thus V n (T ).

Example 4. In this example, we are interested in the language recognized by the automaton of Figure 1b. We want to generate words of length 3(n = 3) with a mean time duration of 5.5. There are only two possible untimed words which are aaa and bbb. One can see that their corresponding polytopes are [0, 1) 3 and (2, +∞) 3 . In particular, timed words are either of duration < 3 or > 6, so there are no timed words of the target duration 5.5. However, a mean duration of 5.5 can be reached by computing and taking the appropriate value for the parameter s, that is, 0.52. By sampling 100 000 words with this parameter, we obtain the histogram depicted in Figure 3 with an average duration of 5.50116.

E(T ) = 0.4, s ≈ 4.34 s = 0, E(T ) = 2 3 E(T ) = 0.9, s ≈ -8.70
Fig. 2: Sample 50000 timed words t 1 at 2 a from the language of Example 1 (the DTA is in Figure 1a) with t 1 in the abscissa and t 2 in the ordinate. Fig. 3: Histogram of duration of 100000 words sampled from the automaton in Figure 1b.

Example 5 (Train Gate). We illustrate the scalability of our method using the well-known Train Gate example described extensively in the Uppaal Tutorial [START_REF] Behrmann | A tutorial on uppaal[END_REF]. This example does not involve a single automaton but a network of timed automata synchronized by their transitions. The semantics of such a network is a single timed automaton whose state space is the cross product of each automaton. This synchronisation semantics is explained in [START_REF] Behrmann | A tutorial on uppaal[END_REF] and implemented in the tool Uppaal, thus we will use the same notation as in this tool.

In this model, N trains want to cross a one-way bridge repeatedly. Each train is modeled as a timed automaton with one clock. The bridge is modeled as a FIFO scheduler, which stops trains or clears them for crossing. The timed automaton for each train is depicted in Figure 4(left) where id is instantiated as an identifier for the train. This automaton is replicated N times with an independent copy of clock x. The clock x is reset on every edge (omitted in the figure). Note that the states Safe and Stop are unbounded. Figure 4(right) depicts the scheduler whose size depends on the number of trains. The FIFO queue is implemented by an array of identifiers of size N and four functions pop, push, front and last that modify it.

In Table 1 we show the performance of the tool Wordgen in sampling a thousand runs of this automaton of expected duration 50. The number N of trains and parameter n are shown in the first two columns. As there is one clock per train, the number of zones grows exponentially with N , while the splitting only double the number of zones. The computation time is dominated by the computation of v n,s (l, x). The sampling time is proportional to the number of trajectories and requires the evaluation of large polynomials for the sampling of timed distributions. As expected, the computation of the zone graph and split

Safe Appr Stop Start Cross appr[id]! x ≤ 10 stop[id]? go[id]? 7 ≤ x x ≤ 15 3 ≤ x ≤ 5, leave[id]! 1 0 ≤ x ≤ 2 0 Q0 Q1 Q2Stop Q1Free Q2 Q3Stop Q2Free Q3 • • • appr[id]? push(id) leave[id]? pop() appr[id]? push(id) stop[last()]! leave[id]? pop() go[f ront()]! appr[id]? push(id) stop[last()]! leave[id]? pop() go[f ront()]!
Fig. 4: The automaton on the left depicts the timed automaton for each train where the clock x is reset on every edge. The automaton on the right depicts the scheduler.

zone graph is small, compared to the other computations. The memory appears to be a computational bottleneck as the number of terms in each v n,s (l, x) grows exponentially with the number of clocks and they need to be computed on each location. By changing the expected duration of timed words, we observe very different behaviors of the system. Figure 5 depicts two timed words sampled from the Train Gate example with 3 trains and n = 10 and of length of length m = 40 using receding sampling. Figure 5(a) depicts a timed word sampled with expected duration 80 while Figure 5(b) depicts a timed word sampled with expected time duration 240. We can see that in Figure 5(b) the system is saturated since there is almost always a train in the locations Start or Cross which have a lower bound on their waiting time, and the synchronisation blocks other events. In Figure 5(a) we observe that the system stay in a state where all trains are in location Safe for some time where there are no constraints (no lower nor upper bound) thus trains evolve more independently.

Conclusion and Future work

In this article, we address the problem of characterizing probability measures of maximal entropy for timed words of a fixed length of timed languages under duration constraints. We focus our attention on constraint on mean duration, which leads us to define and propose a method for efficiently computing Laplace Transform of Volumes, a key theoretical tool to sample timed word wrt. the maximal entropy measure. Several experiments are provided to illustrate our sampling algorithm.

Ongoing and future work The LTV we compute are Laplace transforms of functions V n (T ) which can be called the volume of timed words with fixed duration T . These functions are crucial in our theoretical development of Section 3 but are not computed in this current article. An ongoing work is to write recursive characterization of such functions that could be turned into a sampler of timed words of exact duration T . The computation of closed form formulae for V n (T ) could be used to sample the PDF of the form p R (T ) = p(T )V n (T ), which, coupled with a uniform sampler of exact duration T , would provide a max-entropy sampler for the general linear constraints of Theorem 2. Another promising research direction is to revisit the results of [START_REF] Basset | A maximal entropy stochastic process for a timed automaton[END_REF][START_REF] Asarin | Entropy of regular timed languages[END_REF] with the operator underlying the definition of the LTV. With this approach we aim at defining maximal entropy measure for infinite timed words with a prescribed frequency of event, e.g. 0.7 events per time unit. Finally, another possible extension is to consider max-entropy measures when the length is also random. For this we would like to adapt Boltzmann sampling algorithms ( [START_REF] Duchon | Boltzmann samplers for the random generation of combinatorial structures[END_REF]) to our settings. A first adaptation of such a sampling for a very particular subclass of timed languages (used for random sampling of permutations) was proposed in [START_REF] Basset | Counting and generating permutations in regular classes[END_REF]. This latter work though was not concerned at all with duration of timed words (nor entropy).

Theorem 2 (Maximal entropy theorem on L n with integral constraints on duration). Given the max-entropy problem (7) with its constraints functions f i and constants a i . If one find constants λ i , (0 ≤ i ≤ m) such that the function p * (w) = exp (λ 0 + m i=1 λ i f i (θ(w))) is a PDF that satisfies the constraints, then the problem admits a unique solution which is p * . Proof. Let p * and λ i as above so that p * satisfies the constraints, then we have to prove that H(p * ) is maximal and unique for this property. First, Lemma 3 implies that we only have to consider PDF q of the form q = q • θ. We show that such PDF q satisfies H(q) ≤ H(p * ) with equality iff q = p * . This is equivalent to show that H Vn (q R ) ≤ H Vn (p R ) with equality iff q R = p R , with p R = p.V n and q R = q.V n since by Lemma 2, H Vn (p R ) = H(p * ) and H Vn (q R ) = H(q).

We adapt a classical proof based on Kulback-Lebler divergence that can be found in [START_REF] Cover | Information theory and statistics[END_REF]. The Kullback-Leibler divergence from p R to q R is the quantity

D(q R ||p R ) = +∞ 0 q R (T ) log q R (T )
p R (T ) dT which is always non-negative, and null iff p R = q R . We will show that D(q R ||p R ) = H Vn (p R ) -H Vn (q R ) and thus H Vn (p R ) = H Vn (q R ) will be equivalent to p R = q R . We introduce V n (T ) using the fact that log 2 (q R /p R ) = log 2 q R (T )

Vn(T ) -log 2 p R Vn(T ) : D(q R ||p R ) = +∞ 0 q R (T ) log 2 q R (T ) V n (T ) dT - +∞ 0 q R (T ) log 2 p R (T ) V n (T ) dT The first integral is -H Vn (q R ), hence it remains to prove that H Vn (p R ) = -q R (T ) log 2 p R (T )
Vn(T ) . We recall that p R (T )

Vn(T ) = p(T ) = exp ( m i=0 λ i f i (T )), thus +∞ 0 q R (T ) log 2 p R (T ) V n (T ) = 1 ln 2 +∞ 0 q R (T ) m i=0 λ i f i (T ) dT = 1 ln 2 m i=0 λ i +∞ 0 q R (T )f i (T )dT.
Since q R satisfies the constraints this quantity is equal to 1 ln 2 m i=0 λ i a i The same reasoning holds for p, so we can conclude the proof with the equality:

H Vn (p R ) = - +∞ 0 p R (T ) log 2 p R (T ) V n (T ) dT = - 1 ln(2) m i=0 λ i a i = - +∞ 0 q R (T ) log 2 p R (T ) V n (T ) dT ⊓ ⊔ Proposition 2 (Recursive definition of v n ). v L n,s = a∈Σ +∞ 0 e -st v (ta) -1 L n-1,s dt (15)
Proof.

v L n,s = a∈Σ • • • an∈Σ +∞ 0 1 ta•••tnan∈Ln e -s(t+t2•••+tn) dtdt 2 • • • dt n = a∈Σ +∞ 0 a2∈Σ • • • an∈Σ +∞ 0 • • • +∞ 0 1 ta•••tnan∈Ln e -s(t2•••+tn) dt 2 • • • dt n e -st dt
Then it suffices to remark than ta

• • • t n a n ∈ L n iff t 2 a 2 • • • t n a n ∈ ((ta) -1 L) n-1 ⊓ ⊔
Theorem 3 (Maximal entropy theorem for measures on L n with prescribed mean duration). Given a timed language L, length n, duration 8 T mean , among the probability measures p that satisfy the constraint E p (θ(w)) = T mean , there is a unique one p * that maximizes the entropy. It is given by The first equality holds because the integrated function v L n,s is non-negative. ⊓ ⊔

The following Lemma is useful in the proof of proposition 3.

Lemma 3 (Folk, see [START_REF] Moll | Special Integrals of Gradshteyn and Ryzhik: the Proofs[END_REF] page 82). The primitive function of e ax x n wrt. x is n!e ax n k=0 (-1) k x n-k (n -k)!a k+1 Proposition 3. For every location q and length n, x → v n,s (q, x) is an exponential polynomials. It can be computed in polynomial time using dynamic programming from the following recursive equations: v 0,s (l, x) = 1 l∈F and v m,s (l, x) = δ -=l ub δ (x)

lb δ (x)
v m-1,s δ + , r δ (x + t) e -st dt.

(17)

Proof. ( 12) is a consequence of [START_REF] Budde | A statistical model checker for nondeterminism and rare events[END_REF] where we use the language starting from states and their corresponding LTV. We reason by induction and assume that the results holds at some rank m -1 for some m (and every location q): and show it at rank m. The base case is straightforward since the function is v 0,s (l, x) is the constant 1 or 0 depending on whether the location is final or not. We use the recursive characterisation [START_REF] Cover | Information theory and statistics[END_REF]. A sum of exponential polynomial is clearly an exponential polynomial so it suffices to show that every integral in [START_REF] Cover | Information theory and statistics[END_REF] gives an exponential polynomial. There are two cases to compute the integral:

1. x i ∈ r δ : P (i,k) 1 s , r δ (x + t) e -st dt as t → P (i,k) 1 s , r δ (x + t) is a polynomials in t, applying classical results on Laplace Transform of polynomials (See for example [START_REF] Moll | Special Integrals of Gradshteyn and Ryzhik: the Proofs[END_REF] page 82, recalled in the appendix) we get: e -sk (e -s ub δ (x) P (1/s, x) -e -s lb δ (x) P (1/s, x))

where P is a polynomial. We recall that the bounds lb δ (x) and ub δ (x) are both of the form = c -x i for some constant c and clock x i , so the whole expression is an exponential polynomial. P (i,k) (r δ (x + t))dt as e s(xi-k) is a constant with respect to t. We assume that P (i,k) is nonnull otherwise (i, k) can be removed from S. It cannot be the case that ub δ (x) = +∞ otherwise the integral would give an infinite value which is not possible because the LTV corresponding to the language starting from (q, x) is well defined (at least for positive s) and satisfies [START_REF] Cover | Information theory and statistics[END_REF]. Hence ub δ is like lb δ a polynomial (of degree 1), and hence the integral is a polynomial as integral with polynomial bound of a polynomial. ⊓ ⊔

  {x} a, y < 1, {y} (a) A TA with 2 clocks x and y, 2 states and 2 transitions. The transitions are guarded by an upper-bound of 1. This automaton recognises the language of Ex-< 1, {x} b, 2 < x, {x} a, x < 1, {x} b, 2 < x, {x} (b) A TA with a single clock recognising either words in a n with delays bounded by 1 or words in b n with delays of at least 2.

Lemma 3 .

 3 Let p be a PDF on L n and 6 p : T → 1 Vn(T ) L n,T p(w)dw then H(p) ≤ H(p • θ) with equality if and only if p = p • θ.

  Timed words with an expected duration of 240 time units and 40 events (s ≈ 0.1098). Timed words with an expected duration of 80 time units and 40 events (s ≈ 0.9070).

Fig. 5 :

 5 Fig. 5: Timed words sampled from the Train Gate example. The state of trains are in ordinates.

  ∂s = T mean .Proof. Applying the theorem tells us that p * (w) = e λ0+λ1θ(w) with Ln e λ0+λ1θ(w) dt = 1 and Ln θ(w)e λ0+λ1θ(w) dt = T mean . We let s = -λ 1 and let v L n,s = e -λ0 = Ln e -sθ(w) dt which by Lemma 1 is also equal to +∞ 0 e -sT V L n (T )dT . The expected duration is by definition:We can express this with the derivatives of v L n,s = Ln e -sθ(w) dw. Indeed, e -sθ(w) dw = -v L n,s T mean .

  δ (x + t) e s(r δ (x+t)i-k) e -st dt = e -sk ub δ (x) lb δ (x)

2 .

 2 x i / ∈ r δ : ub δ (x) lb δ (x) P (i,k) 1 s , r δ (x + t) e s(r δ (x+t)i-k) e -st dt = e s(xi-k) ub δ (x) lb δ (x)

Table 1 :

 1 Each experiment samples 1000 timed words of length n and expected duration 50

	N n	number of locations		time (sec)		memory
		reachability split	reach+split distribution sampling
	1 10	9	9	0	0	0.07	6.2 MB
	2 10	51	70	0.01	0	0.13	34.8 MB
	3 10	1081	1826	0.12	9.04	2.6	1.7 GB
	4 10	28353	53534	7.2	647	466	51.9 GB
	5 10	88473	178414	35	Out of Memory > 64GB
	5 7	88473	178414	35	408	205	52.4 GB

In this definition the usual convention that 0 log 2 0 = 1 applies.

One could also sample the delay before the action, this would lead at the end to the same probability distribution on timed words.

The timed words of duration T have their timed vector (t1, . . . , tn) belonging to the hyperplane t1 + . . . + tn = T which have a null volume. That is why we do not integrate over the last delay which is fixed and equal to T -t1 -• • • -tn-1

Here p generalises the previous concept it was used for: when p depends only on duration then p = p • θ.

Here p generalises the previous concept it was used for: when p depends only on duration then p = p • θ.

⋆ This work was financed by the ANR MAVeriQ (ANR-20-CE25-0012)

A Appendix

In this appendix, we give the omitted proofs of the results presented above after recalling their statement.

We do the change of variables that replace t n with T -t 1 -. . . -t n-1 and leave unchanged the others t i . This change of variables has a Jacobian equals to 1 and so no multiplicative constant appears.

Let p be a PDF on L n and 7 p :

Proof. We first regroup timed word with respect to duration in the definition of H(p):

p(w) log p(w)dwdT

We use Jensen's inequality with the strictly convex function φ : x → x log 2 x the uniform PDF on L n,T : w → 1 Vn(T ) and the function p:

Multiplying by -V n (T ) and integrating wrt. T we get

The last equality being an application of Lemma 1. To have equality H(p) = H(p • θ) we must have equality in the Jensen's inequality which is only possible if p(w) is constant on L n,T . This means that p depends only on duration which is equivalent to p = p • θ.

⊓ ⊔