Nathalie Bertrand
email: nathalie.bertrand@inria.fr

Patricia Bouyer
email: bouyer@lsv.ens-cachan.fr

Thomas Brihaye
email: thomas.brihaye@umons.ac.be

Quentin Menet
email: quentin.menet@umons.ac.be

Christel Baier
email: baier@tcs.inf.tu-dresden.de

Marcus Gr Össer
email: groesser@tcs.inf.tu-dresden.de

AND MARCIN Jurdzi Ński

Bouyer, Brihaye, Menet, Baier, Grösser Jurdzi Bertrand

Ński

STOCHASTIC TIMED AUTOMATA

Keywords: 2012 ACM CCS: [Theory of computation]: Semantics and reasoning-Program reasoning-Program verification; [Software and its engineering]: Software organization and properties-Software functional properties-Formal methods-Model checking Timed automata, Model checking, Probability, Topology

A stochastic timed automaton is a purely stochastic process defined on a timed automaton, in which both delays and discrete choices are made randomly. We study the almost-sure model-checking problem for this model, that is, given a stochastic timed automaton A and a property ϕ, we want to decide whether A satisfies ϕ with probability 1. In this paper, we identify several classes of automata and of properties for which this can be decided. The proof relies on the construction of a finite abstraction, called the thick graph, that we interpret as a finite Markov chain, and for which we can decide the almost-sure model-checking problem. Correctness of the abstraction holds when automata are almost-surely fair, which we show, is the case for two large classes of systems, singleclock automata and so-called weak-reactive automata. Techniques employed in this article gather tools from real-time verification and probabilistic verification, as well as topological games played on timed automata.

Introduction

Timed automata and their extensions. In the last twenty years a huge effort has been made to design expressive models for representing computerised systems. As part of this effort the model of timed automata [START_REF] Alur | Automata for modeling real-time systems[END_REF][START_REF] Alur | A theory of timed automata[END_REF] has been proposed in the early 90's as a suitable model for representing systems with real-time constraints. Numerous works have focused on that model, and it has received an important tool support, with for instance the development of tools like Uppaal [BDL + 06] or Kronos [BDM + 98].

Given the success of the timed-automata-based technology for verifying real-time systems, several extensions have been proposed, with the aim of representing more faithfully real systems. They include timed games [START_REF] Asarin | Controller synthesis for timed automata[END_REF] for modeling control problems and priced timed automata [ALP01, BFH + 01, BFLM11] for modeling various quantities in timed systems, like energy consumption.

Stochastic extensions of timed automata. Many applications like communication protocols require models integrating both real-time constraints and randomised aspects (see e.g. [START_REF] Stoelinga | Fun with FireWire: A comparative study of formal verification methods applied to the IEEE 1394 root contention protocol[END_REF]). The development of such models and corresponding verification algorithms is a challenging task, since it requires combining techniques from both fields of real-time verification and probabilistic verification. In the literature we distinguish two main different approaches.

A first approach consists in modeling the system as a purely stochastic process, and to express soft real-time constraints in the property that is checked. A model of choice for the system is that of continuous-time Markov chains (CTMC for short), while a rather wide spectrum of property formalisms has been considered, going from the logic CSL (continuous stochastic logic) and extensions thereof [ASSB00, BHHK03, DHS09, ZJNH11] to (deterministic) timed automata [START_REF] Chen | Model-checking of continuous-time Markov chains against timed automata specifications[END_REF]. In this context several exact and approximate model-checking algorithms have been developed.

Another approach consists in integrating both features into a complex model (e.g. an extension of timed automata or Petri nets with stochastic evolution rules), and to analyse this model. This allows one to represent hard timing contraints such as deadlines. In this article we focus on automata-based models, and therefore only review related work on models based on timed automata. Such models include probabilistic timed automata [START_REF] Kwiatkowska | Automatic verification of real-time systems with discrete probability distributions[END_REF] where discrete distributions are assigned to actions and for which the tool Prism [START_REF] Kwiatkowska | PRISM 4.0: verification of probabilistic real-time systems[END_REF] has been developed. Delays or durations of events can also be made randomised. This is done for instance in [START_REF] Alur | Model-checking for probabilistic real-time systems[END_REF][START_REF] Alur | Verifying automata specifications of probabilistic real-time systems[END_REF] and later in [START_REF] Kwiatkowska | Verifying quantitative properties of continuous probabilistic timed automata[END_REF], yielding either independent events and exact model-checking algorithms (for a probabilistic and timed extension of computation tree logic), or approximate model-checking algorithms.

The current work follows this last approach, and surveys and extends results based on the model of stochastic timed automata. This model has been proposed and studied in a series of papers [BBB + 07, BBB + 08, BBJM12]. The semantics of a stochastic timed automaton is a purely stochastic process based on a timed automaton, in which both delays and discrete choices are made randomly. This model has later been extended with nondeterminism and interaction [START_REF] Bouyer | Reachability in stochastic timed games[END_REF][START_REF] Bertrand | Playing optimally on timed automata with random delays[END_REF], but in this article we focus on the original purely stochastic model.

Overview of the contributions. In this article we are interested in the almost-sure model-checking of stochastic timed automata. This problem asks, given a stochastic timed automaton A and a property ϕ, whether A almost-surely satisfies ϕ (that is, with probability 1). Our approach to solve this problem relies on the construction of a finite Markov chain MC(A)1 on which we will check whether ϕ almost-surely holds or not. We will then say that the abstraction MC(A) is correct w.r.t. ϕ whenever ϕ almost-surely holds equivalently in A and in MC(A). Unfortunately, this will not be the case in general, and beyond the introduction of stochastic timed automata, the main goal of this article is to identify subclasses of stochastic timed automata and subclasses of properties for which the abstraction MC(A) is correct.

More precisely, we show that MC(A) is a correct abstraction w.r.t. property ϕ in the following cases: (i) if ϕ is a safety property, (ii) if ϕ is an ω-regular (or LTL) property and A is a single-clock stochastic timed automaton, and (iii) if ϕ is an ω-regular (or LTL) property and A belongs to a subclass of stochastic timed automata called weak reactive. In fact, cases (ii) and (iii) are consequences of a more general result stating that if the runs in a stochastic timed automaton A are almost-surely fair2 , then MC(A) is a correct abstraction. The results then follow from the (highly non trivial) proof that both weak reactive and single-clock stochastic timed automata are almost-surely fair.

We also establish the exact complexity of the almost-sure model-checking problem in the three above cases. More precisely, we prove that the almost-sure model-checking problem is (i) PSPACE-complete on stochastic timed automata against safety properties, (ii) PSPACEcomplete (resp. NLOGSPACE-complete) on single-clock stochastic timed automata against properties given as LTL formulas (resp. ω-regular properties), and (iii) PSPACE-complete on weak reactive stochastic timed automata against ω-regular properties. We finally extend this last result to specifications given as deterministic timed automata. Let us point out that the decidability status of the almost-sure model checking problem for LTL properties on the general class of stochastic timed automata is still an open problem.

A model which relaxes timed automata assumptions. Let us mention that one initial motivation for defining stochastic timed automata was the robustness of timed systems. Indeed, the model of timed automata is an idealised mathematical model, which makes strong assumptions on the behaviour of the represented real system: it assumes for instance infinite precision of the clocks, instantaneous events and communications, whereas a real system will have slightly different behaviours (like measure time with digital clocks). This topic of research is very rich, and many models and results have already been described.

We review some of the frameworks which have been studied in this context, but will not give a long list of references. We better point to a survey made in 2011 [START_REF] Markey | Robustness in real-time systems[END_REF], and to a recent PhD thesis [START_REF] Sankur | Robustness in Timed Automata: Analysis, Synthesis, Implementation[END_REF], which review in details the literature on the subject. Let us first mention two models of implementable controllers proposed in [START_REF] De Wulf | Almost ASAP semantics: From timed models to timed implementations[END_REF] and in [START_REF] Sankur | Shrinking timed automata[END_REF], where constraints and precision of clocks are somewhat relaxed. In this framework, if the model satisfies a property, then, on a simple model of processor, its implementation will also satisfy this property. This implementation model induces a very strong notion of robustness, suitable for really critical systems (like rockets or X-by-wire systems in cars), but maybe too strong for less critical systems (like mobile phones or network applications). Another robustness model has been proposed at the end of the 90's in [START_REF] Gupta | Robust timed automata[END_REF] with the notion of tube acceptance: a metric is put on the set of traces of the timed automaton, and a trace is robustly accepted if and only if a tube around that trace is classically accepted. This language-focused notion of acceptance is however not completely satisfactory for implementability issues, because it does not take into account the structure of the automaton.

In this context, the model of stochastic timed automata alleviates some disadvantages to the strong mathematical assumptions made in timed automata. First, randomising delays and the choice of transitions removes unlikely behaviours (like those requiring satisfaction of very precise clock constraints), and only important and meaningful sets of behaviours are then taken into account in the verification process. Then, the assumptions made in timed automata mentioned above lead to the existence of unreal(istic) behaviours of the model, such as Zeno behaviours 3 that one would like to ignore. We will then realise that, unless the underlying timed automaton is inherently Zeno, the probability of Zeno behaviours will be 0 (at least in the classes of models we have identified). This allows us to convincingly claim that stochastic timed automata can be used as a possible solution for relaxing side-effects of mathematical assumptions made in timed automata.

As a motivating example, we describe a model of the IPv4 Zeroconf protocol using stochastic timed automata, see Figure 1. This protocol aims at configuring IP addresses in a local network of appliances. When a new appliance is plugged, it selects an IP address at random, and broadcasts several probe messages to the network to know whether this address is already used or not. If it receives in a bounded delay an answer from the network informing that the IP is already used, then a new IP address is chosen. It may be the case that messages get lost, in which case there is an error. In [START_REF] Bohnenkamp | Costoptimization of the IPv4 Zeroconf protocol[END_REF], a simple model for the IPv4 Zeroconf protocol is given as a discrete-time Markov chain, which abstracts away timing constraints. Using stochastic timed automata, expressing the delay bound is feasible. The example of Figure 1 illustrates an important feature of stochastic timed automata. Compared to CTMC-like models, stochastic timed automata allow one to express hard timing contraints such as deadlines (constraint x ≤ T in this example). Another important feature of stochastic timed automata, as we will show in this article, is that the almostsure satisfaction of properties is independent of the precise probability distributions over delays. This is a major advantage since it avoids the problem of finding realistic probability distributions which is known to be a difficult task, see e.g. [BDE + 14].

The Cantor topology: a useful tool. In a former paper [START_REF] Varacca | Temporal logics and model checking for fairly correct systems[END_REF], Varacca and Völzer show a strong correspondence between a standard Markov-chain-based probabilistic semantics of a finite automaton, and the Cantor topology over the set of infinite executions of this automaton. They show in particular that almost-sure sets of executions (that is, sets of executions which have probability 1) coincide with topologically large sets of executions. Following this idea we also define a topological semantics à la Cantor for a timed automaton. In our framework, the above equivalence does not always hold, but in many cases however we will be able to prove it. This characterisation is incredibly useful in order to prove our results. The key tool in our techniques is a topological game called Banach-Mazur game [START_REF] Oxtoby | The Banach-Mazur game and Banach category theorem[END_REF].

Related work. The literature on stochastic processes is huge. We already mentioned several related works, but we would like to discuss a bit more the works [START_REF] Donatelli | Model checking timed and stochastic properties with CSL TA[END_REF][START_REF] Chen | Model-checking of continuous-time Markov chains against timed automata specifications[END_REF], which we think are the closest to the current article. In both papers the model is that of CTMCs. Timing constraints are expressed in the properties, either given as deterministic timed automata [START_REF] Chen | Model-checking of continuous-time Markov chains against timed automata specifications[END_REF] or as an extension of CSL called CSL TA [START_REF] Donatelli | Model checking timed and stochastic properties with CSL TA[END_REF], which extends CSL with properties given as single-clock deterministic timed automata.

Paper [START_REF] Chen | Model-checking of continuous-time Markov chains against timed automata specifications[END_REF] is interested in quantitative model-checking, that is, given a CTMC C and a property given as a deterministic (Muller) timed automaton A, the aim is to compute the probability that runs of C are accepted by A. This probability is characterised using Volterra integral equations, which can be transformed into linear equations when A has a unique clock. Therefore quantitative verification can be done for single-clock specifications but can only be approximated in the general case. Our results are somehow incomparable since we allow for a more general model (stochastic timed automata instead of CTMCs) but prove decidability only for the qualitative model-checking problem.

Paper [START_REF] Donatelli | Model checking timed and stochastic properties with CSL TA[END_REF] is interested in model-checking of CTMCs against properties expressed as formulas of CSL TA . This logic involves probability formulas, and uses single-clock deterministic timed automata as predicates. Model-checking of the general logic can be approximated, but if formulas only have qualitative subformulas, the exact model-checking can be decided. We do not consider logics, but we allow general deterministic timed automata in our specifications.

Organisation. Section 2 summarises our notations for timed automata, and specifications languages (such as LTL and ω-regular properties). Section 3 presents stochastic timed automata, the notion of almost-sure satisfaction and the almost-sure model-checking problem, while Section 4 presents the topological semantics and the notion of large satisfaction. In Section 5, we define a finite abstraction of a stochastic timed automaton, named thick graph, which will be essential in order to solve the almost-sure model-checking problem. In Section 6, we show that the topological and the probabilistic semantics coincide first if we restrict to safety properties and then for ω-regular properties but under the restriction that the system is almost-surely fair. In Section 7, we identify two subclasses of stochastic timed automata which are almost-surely fair, namely weak reactive and single-clock. Finally, the algorithmic issues and the complexity results are given in Section 8. To improve readability of the article, technical proofs are postponed to the Appendix. This article presents results from [BBB + 07, BBB + 08, BBJM12] in a uniform way, provides the complete proofs, and generalises the results from [START_REF] Bouyer | Almost-sure modelchecking of reactive timed automata[END_REF] to a larger class of stochastic timed automata.

Preliminaries

2.1. The timed automaton model. We denote by X = {x 1 , . . . , x k } a finite set of clocks. A clock valuation over X is a mapping ν : X → R + , where R + denotes the set of nonnegative reals. We write R X + for the set of clock valuations over X, and 0 X (or simply 0 if X is clear in the context) for the valuation assigning 0 to every clock of X. Given a clock valuation ν and τ ∈ R + , ν + τ is the clock valuation defined by (ν + τ

)(x) = ν(x) + τ for every x ∈ X. If Y ⊆ X, the valuation [Y ← 0]ν is the valuation ν ′ such that ν ′ (x) = 0 if x ∈ Y , and ν ′ (x) = ν(x) otherwise.
A guard over X is a finite conjunction of expressions of the form x ∼ c where x ∈ X is a clock, c ∈ N is an integer, and ∼ is one of the symbols {<, ≤, =, ≥, >}. We denote by G(X) the set of guards over X. The satisfaction relation for guards over clock valuations is defined in a natural way, and we write ν |= g if the clock valuation ν satisfies the guard g. We denote by AP a finite set of atomic propositions.

We now define the timed automaton model, which has been introduced in the early nineties [START_REF] Alur | Automata for modeling real-time systems[END_REF][START_REF] Alur | A theory of timed automata[END_REF].

Definition 2.1. A timed automaton over AP is a tuple A = (L, X, E, I, L) such that: (i) L is a finite set of locations, (ii) X is a finite set of clocks, (iii) E ⊆ L × G(X) × 2 X × L
is a finite set of edges, (iv) I : L → G(X) assigns an invariant to each location, and (v) L : L → 2 AP is a labelling function.

We may omit the labelling function (in case we are only interested in an internal accepting condition, i.e. that only depends on the locations). Note that we could also specify an initial location, but that will not be really useful later, that is why we removed that component from standard timed-automata definition.

If e is an edge of A, we write source(e) (resp. target(e)) the source (resp. target) of e defined by ℓ (resp. ℓ ′ ) if e = (ℓ, g, Y, ℓ ′ ). The semantics of a timed automaton A is a timed transition system T A whose states are pairs s = (ℓ, v) ∈ L × R X + with v |= I(ℓ), and whose transitions are of the form (ℓ, v)

τ,e --→ (ℓ ′ , v ′ ) if there exists an edge e = (ℓ, g, Y, ℓ ′ ) such that for every 0 ≤ τ ′ ≤ τ , v + τ ′ |= I(ℓ), v + τ |= g, v ′ = [Y ← 0]v, and v ′ |= I(ℓ ′ ). We extend the labelling function L to states: L((ℓ, v)) = L(ℓ) for every state (ℓ, v). A finite (resp. infinite) run ̺ of A is a finite (resp. infinite) sequence of transitions, i.e., ̺ = s 0 τ 1 ,e 1 ---→ s 1 τ 2 ,e 2 ---→ s 2 . . .
We write Runs f (A, s 0 ) (resp. Runs(A, s 0 )) for the set of finite runs (resp. infinite runs) of A from state s 0 . If ̺ is a finite run in A, we write last(̺) for the last state of ̺. For s a state of A, (e i ) 1≤i≤n a finite sequence of edges of A, and C a constraint over n variables (t i ) 1≤i≤n , the (symbolic) path starting from s, determined by (e i ) 1≤i≤n , and constrained by C, is the following set of runs:

π C (s, e 1 . . . e n ) = {̺ = s τ 1 ,e 1 ---→ s 1 . . . τn,en ---→ s n ∈ Runs f (A, s) | (τ i ) 1≤i≤n |= C} ,
where (τ i ) 1≤i≤n |= C stands for "τ i 's satisfy the constraint C" with the intuitive meaning.

If C is equivalent to 'true', we simply write π(s, e 1 . . . e n ). Let π C = π C (s, e 1 . . . e n ) be a finite symbolic path, we define the cylinder generated by π C as:

Cyl(π C ) = {̺ ∈ Runs(A, s) | ∃̺ ′ ∈ Runs f (A, s), finite prefix of ̺, s.t. ̺ ′ ∈ π C } .
In the following, we will also use infinite symbolic paths defined, given s a state of A and (e i ) i≥1 an infinite sequence of edges, as:

π(s, e 1 . . .) = {̺ = s τ 1 ,e 1 ---→ s 1 . . . ∈ Runs(A, s)} .
If ̺ ∈ Runs(A, s), we write π ̺ for the unique symbolic path containing ̺. Given s a state of A and e an edge, we define I(s, e) = {τ ∈ R + | ∃s ′ s.t. s τ,e --→ s ′ } and I(s) = e I(s, e). Note that I(s, e) is an interval, whereas I(s) is a finite union of intervals.

The timed automaton A is non-blocking if, for every state s, I(s) = ∅. The timed automaton A is reactive if, for every state s, I(s) = R + ; in this case we may omit the invariant function and simply write A = (L, X, E, L).

2.2.

The timed region automaton. The well-known region automaton construction is a finite abstraction of timed automata which can be used for verifying many properties like ω-regular untimed properties [START_REF] Alur | A theory of timed automata[END_REF]. Roughly, the region automaton of A is the quotient of T A by a finite-index equivalence relation over clock valuations. Here we will use a timed version of this construction, that we define now.

Let A = (L, X, E, I, L) be a timed automaton, and write M for the maximal constant used in guards and invariants in A. We define its region equivalence ≡ A over the set of valuations R X + as follows: given v, v ′ ∈ R X + , v ≡ A v ′ if and only if the following conditions are satisfied: • for every x ∈ X, either v(x), v ′ (x) > M , or ⌊v(x)⌋ = ⌊v ′ (x)⌋, and in the last case, {v(x)} = 0 iff {v ′ (x)} = 0;4 • for every x, y ∈ X such that v(x), v(y) ≤ M , {v(x)} ≤ {v(y)} iff {v ′ (x)} ≤ {v ′ (y)}. This equivalence relation has finite index, the equivalence classes are called regions, and we write R A for the set of regions. If v is a valuation, we write [v] A or simply [v] for the (unique) region to which v belongs. Also, for r a region, guard(r) denotes the minimal guard characterising r.

Remark 2.2. The above region equivalence is the most standard one, but several rougher equivalences could also be used, as soon as they yield a time-abstract bisimilar quotient. For instance, for single-clock timed automata, we will later use a rougher notion of region equivalence [START_REF] Laroussinie | Model checking timed automata with one or two clocks[END_REF] that will improve the complexity of our algorithms.

The timed region automaton of

A is the timed automaton R(A) = (Q, X, T, κ, λ) such that Q = L × R A , and: • κ((ℓ, r)) = I(ℓ), and λ((ℓ, r)) = L(ℓ) for all (ℓ, r) ∈ L × R A ; • T ⊆ (Q × guard(R A ) × E × 2 X × Q), and (ℓ, r) guard(r ′′ ),e,Y --------→ (ℓ ′ , r ′ ) is in T iff there exists e = ℓ g,Y --→ ℓ ′ in E s.t. there exist v ∈ r, τ ∈ R + with (ℓ, v) τ,e --→ (ℓ ′ , v ′ ), v + τ ∈ r ′′ and v ′ ∈ r ′ .
As an example, a timed automaton and its associated timed region automaton are depicted in Figure 2. We recover the usual region automaton of [START_REF] Alur | A theory of timed automata[END_REF] by labelling the transitions BERTRAND, BOUYER, BRIHAYE, MENET, BAIER, GR ÖSSER, AND JURDZI ŃSKI with 'e' instead of 'guard(r ′′ ), e, Y ', and by interpreting R(A) as a finite automaton. The above timed interpretation satisfies strong timed bisimulation properties that we do not detail here. To every finite symbolic path π((ℓ, v), e 1 . . . e n ) in A corresponds a finite set of paths π(((ℓ,

ℓ 0 ℓ 1 ℓ 2 x < 1 , e1 1 < x < 2 , e 2 ℓ 0 ,x=0 ℓ 1 ,x=0 ℓ 1 ,0<x<1 ℓ 2 ,1<x<2 x = 0 , f1 0<x<1, f 2 1 < x < 2 , f 3
[v]), v), f 1 . . . f n ) in R(A)
, each one corresponding to a choice in the regions that are crossed. If ̺ is a run in A, we denote ι(̺) its unique image in R(A). Note that if A is non-blocking (resp. reactive), then so is R(A).

In the rest of the paper we assume that timed automata are non-blocking, even though general timed automata could also be handled (but at a technical extra cost).

2.3. Specification languages. We fix a finite set of atomic propositions AP, and a timed automaton A = (L, X, E, I, L) over AP.

2.3.1.

Properties over AP.. A property over AP is a subset P of Ä 2 AP ä ω . An infinite run

̺ = s 0 τ 1 ,e 1 ---→ s 1 τ 2 ,e 2
---→ . . . satisfies the property whenever L(s 0 )L(s 1 )L(s 2 ) . . . ∈ P . More generally a timed property over AP is a subset

P of 2 AP • Ä R + • 2 AP ä ω . An infinite run ̺ = s 0 τ 1 ,e 1 ---→ s 1 τ 2 ,e 2
---→ . . . satisfies the property P whenever L(s 0 ) τ 1 L(s 1 ) τ 2 L(s 2 ) . . . ∈ P .

In both cases, we write ̺ |= P if ̺ satisfies the property P , and we write:

P A,s def = {̺ ∈ Runs(A, s) | ̺ |= P } .
Remark 2.3. Obviously, timed properties generalise (untimed) ones.

2.3.2. ω-regular properties. ω-regularity is a standard notion in computer science to characterise simple sets of infinite behaviours. We will only define here ω-regularity for untimed properties, though the concept exists for timed properties as well.

Typical ω-regular properties are Büchi and Muller properties. A Büchi property over AP is a(n untimed) property P such that there exists F ⊆ AP with P = {u 0 u 1 . . . | {j | F ∩ u j = ∅} is infinite}. A Muller property over AP is a property P such that there exists

F ⊆ 2 AP with P = {u 0 u 1 . . . | {j | u j ∈ F} is infinite}.
An ω-regular property will be said internal for A whenever there is a bijection β between L and AP, and for each ℓ ∈ L, L(ℓ) is the singleton {β(ℓ)}. That is, this allows to specify which states are visited infinitely often. In that case, we will interpret such properties on timed automata even though no labelling function has been given (it is then implicit). It is well known that (untimed) automata equipped with internal Büchi or Muller acceptance conditions capture untimed ω-regular properties. This is also the case for deterministic Muller automata. 2.3.3. Safety, reachability, and prefix-independent properties. We now define simple ω-regular properties.

According to [START_REF] Chang | Characterization of temporal property classes[END_REF], a property P over AP is a safety property whenever for every

w = u 0 u 1 . . . ∈ Ä 2 AP
ä ω , w / ∈ P iff there exists i such that for every

w ′ = u 0 . . . u i u ′ i+1 u ′ i+2 . . . ∈ Ä 2 AP ä ω , w ′ / ∈ P .
That is, a safety property is violated by a finite prefix. A simple safety property P is characterised by F ⊆ AP, and is defined by

P = {u 0 u 1 . . . | ∀j, u j ∈ F }.
The negation of a safety property is a reachability property: P is a reachability property whenever for every w = u 0 u 1 . . .

∈ Ä 2 AP
ä ω , w ∈ P iff there exists i such that for every

w ′ = u 0 . . . u i u ′ i+1 u ′ i+2 . . . ∈ Ä 2 AP ä ω , w ′ ∈ P .
That is, a reachability property is validated by a finite prefix. A simple reachability property P is characterised by F ⊆ AP, and is defined by

P = {u 0 u 1 . . . | ∃j, u j ∈ F }.
Another interesting notion is the one of prefix-independent property P , which is such that for every

w = u 0 u 1 . . . ∈ Ä 2 AP ä ω , w ∈ P iff for every i, w ′ = u i u i+1 . . . ∈ P . That is,
the property is satisfied or not independently of its prefix. In particular, Büchi and Muller properties are prefix-independent. Note that a property P is prefix-independent if and if its validity only depends on the set of elements of 2 AP which is encountered infinitely often.

2.3.4.

The temporal logic LTL. We consider the linear temporal logic LTL [START_REF] Pnueli | The temporal logic of programs[END_REF] over AP, defined inductively as:

LTL ∋ ϕ ::= p | ϕ ∨ ϕ | ϕ ∧ ϕ | ¬ϕ | ϕ U ϕ
where p ∈ AP is an atomic proposition. We use classical shorthands like tt

def = p ∨ ¬p, ff def = p ∧ ¬p, F ϕ def = tt U ϕ, and G ϕ def = ¬F (¬ϕ).
We assume the reader is familiar with the semantics of LTL, that we interpret here on infinite runs of a timed automaton.

Each formula ϕ of LTL gives rise to a property P ϕ , in the sense given above. Let

w = u 0 u 1 . . . ∈ Ä 2 AP
ä ω , then:

w ∈ P p ⇔ p ∈ u 0 w ∈ P ϕ 1 ∨ϕ 2 ⇔ w ∈ P ϕ 1 ∪ P ϕ 2 w ∈ P ϕ 1 ∧ϕ 2 ⇔ w ∈ P ϕ 1 ∩ P ϕ 2 w ∈ P ¬ϕ ⇔ w / ∈ P ϕ w ∈ P ϕ 1 U ϕ 2 ⇔ ∃i ≥ 0 s.t. w ≥i ∈ P ϕ 2 and ∀0 ≤ j < i, w ≥j ∈ P ϕ 1
where w ≥k = u k u k+1 . . . for every index k.

The semantics of a formula ϕ over infinite runs of A is derived from that of property P ϕ . One can easily be convinced that we recover the standard semantics of LTL. If ϕ is an LTL formula and ̺ ∈ Runs(A, s), we write ̺ |= ϕ whenever ̺ |= P ϕ . We also write ϕ A,s for P ϕ A,s . 2.3.5. Specifications given as deterministic timed automata. A specification ω-regular timed automaton is a tuple B = (L, i 0 , X, AP, E, F) such that: • L is a finite set of locations, and i 0 : 2 AP → L is an input function;

• X is a finite set of clocks;

• AP is a finite set of atomic propositions;

• E ⊆ L × G(X) × 2 AP × 2 X × L is a finite set of edges;
• F is an internal ω-regular prefix-independent condition; • it is deterministic: for all edges (l

g 1 ,u,Y 1 ----→ l 1 ) and (l g 2 ,u,Y 2 ----→ l 2 ) in E, g 1 ∧ g 2 is not satisfiable;
• it is complete: for every every l ∈ L, for every u ∈ 2 AP , for every v ∈ R X + , for every τ ∈ R + , there exists (l

g,u,Y ---→ l ′ ) ∈ E such that v + τ |= g.
Runs in B will be defined in a very similar way as runs in standard timed automata. Only labels of transitions will be slightly different. The runs of B are therefore of the form:

(l 0 , v 0 ) τ 1 ,u 1 ---→ (l 1 , v 1 ) τ 2 ,u 2 ---→ . . .
where conditions on valuations are those expected, and labels u i 's are those given by the edges that are taken. Such a run is accepted by B whenever the sequence (l i ) i≥0 satisfies the ω-regular condition F.

Such a specification automaton B naturally gives rise to a timed property P B defined as follows. Let

w = u 0 τ 1 u 1 τ 2 . . . ∈ 2 AP • Ä R + • 2 AP ä ω .
There is a unique run κ w = (l 0 , 0 X )

τ 1 ,u 1 ---→ (l 1 , v 1 ) τ 2 ,u 2
---→ . . . in automaton B where l 0 = i 0 (u 0 ). The existence of κ w follows from the completeness of B and its uniqueness from the determinism. Then, w ∈ P B iff κ w is an accepting run in B.

The semantics of a specification timed automaton B over infinite runs of A is derived from that of property P B . If B is a specification timed automaton and ̺ ∈ Runs(A, s), we write ̺ |= B whenever ̺ |= P B . We also write B A,s for P B A,s .

Remark 2.4. If the accepting condition F is a Büchi (or Muller) condition, then B will be called a specification Büchi (or Muller) timed automaton. If X = ∅, we will speak of a specification ω-regular (untimed) automaton. It is well known [START_REF] Vardi | Reasoning about infinite computations[END_REF] and [GThW02, Chapter 3] that for any LTL formula ϕ, there is a (deterministic) specification Muller untimed automaton B ϕ that characterises ϕ, that is: for every run ̺, ̺ |= ϕ iff ̺ |= B ϕ . In that case, obviously, ϕ A,s = B ϕ A,s for every A and s.

Stochastic timed automata: the semantics

In this section we define a probabilistic semantics for timed automata. Probabilities will rule time elapsing as well as choices between enabled events. This will define a purely stochastic process: intuitively, from a state, we will first randomly choose a delay among all possible delays, then we will randomly choose an edge among all those which are enabled.

The sequel assumes some basics of measure theory and probabilities, that can be found in classical text books.

3.1. Probability measure on runs of a timed automaton. Let A = (L, X, E, I, L) be a timed automaton. We will assign probability distributions from every state of A both over delays and over enabled moves. Let s be a state of A. The probability distribution from s over delays is a probability measure µ s over R + (equipped with the standard Borel σ-algebra) which satisfies the following requirements, denoted (⋆) in the sequel: (H1): µ s (I(s)) = µ s (R + ) = 1,5 (H2): Writing λ for the standard Lebesgue measure on R + , if λ(I(s)) > 0, then µ s is equivalent6 to λ on I(s); Otherwise, µ s is equivalent to the uniform distribution over points of I(s). This last condition denotes some kind of fairness w.r.t. enabled transitions when only punctual delays are possible, in that we cannot disallow one transition by putting a probability 0 to delays enabling that transition.

We also assume a probability distribution p s over edges, such that for every edge e, p s (e) > 0 iff e is enabled in s (i.e., s e -→ s ′ for some s ′ ). Moreover, to simplify, we assume that p s is given by weights on transitions, as it is classically done for resolving non-determinism: we associate with each edge e a weight w(e) > 0, and for every state s, for every edge e, p s (e) = 0 if e is not enabled in s, and p s (e) = w(e)/( e ′ enabled in s w(e ′ )) otherwise. As a consequence, if s and s ′ are region equivalent, then for every edge e, p s (e) = p s ′ (e). Definition 3.1 (Stochastic timed automaton). A stochastic timed automaton is a tuple A, µ, w consisting of a timed automaton A equipped with probability measures µ = (µ s ) s∈L×R X + satisfying (⋆), and positive weights w = (w e ) e∈E .

Note that when measures are clear or implicit in the context, we will simply write A for A, µ, w . We now show how we define a probability measure P A on infinite runs of A, µ, w .

We fix a stochastic timed automaton A, µ, w , which satisfies (⋆). We define a measure, that we also note P A , over finite symbolic paths from state s as follows:

P A (π(s, e 1 . . . e n )) = t∈I(s,e 1 )
p s+t (e 1 ) P A (π(s t , e 2 . . . e n )) dµ s (t) where s t -→ (s + t) e 1 -→ s t , and we initialise with P A (π(s)) = 1. The formula for P A relies on the fact that the probability of taking transition e 1 at time t coincides with the probability of waiting t time units and then choosing e 1 among the enabled transitions, i.e., p s+t (e 1 )dµ s (t). Note that, time passage and actions are independent events. The value P A (π(s, e 1 . . . e n )) is the result of n successive one-dimensional integrals, but it can also be viewed as the result of an n-dimensional integral. Hence, we can easily extend the above definition to finite constrained paths π C (s, e 1 . . . e n ) when C is Borel-measurable. This extension to constrained paths is needed to measure rather complex properties, like Zeno behaviours or those expressed as specification timed automata. The measure P A can then be defined on cylinders, letting P A (Cyl(π)) = P A (π) if π is a finite (constrained) symbolic path. Finally we extend P A in a standard and unique way to the σ-algebra generated by these cylinders (using Caratheodory's theorem), that we note Ω s A . We first check that P A defined as such is a probability measure. Proposition 3.2. For every state s of A, P A is a probability measure over (Runs(A, s), Ω s A ).

The proof of this proposition justifies a posteriori the above construction for the probability measure P A . It goes as follows: first prove that P A is a probability measure on the set of constrained symbolic paths of length n (for all n), then extend this result to the ring generated by all constrained symbolic paths and finally use Caratheodory's extension theorem to establish that P A is a probability measure on the set of all runs. The complete proof is rather technical, and therefore postponed to Appendix A, page 41.

Example 3.3. Consider the running stochastic timed automaton A running on Figure 3. Assume for all states s t = (ℓ 0 , t) both uniform distributions over delays and discrete moves: µ s 0 = λ is the uniform distribution over [0, 1] and µ st = λ 1-t is the uniform distribution over [t, 1]; the weight of each edge is 1. Then P A running (Cyl(π(s 0 , e 1 e 1 ))) = 1 4 and P A running (π(s 0 , e 1 ω )) = 0. Indeed:

P A running (π(s 0 , e 1 e 1 )) = t∈I(s 0 ,e 1 )
p s 0 +t (e 1 ) P A running (π((ℓ 0 , t), e 1 )) dµ s 0 (t)

= 1 0 1 2 P A running (π((ℓ 0 , t), e 1 )) dλ(t) = 1 2 1 0 Ç t∈I(st,e 1 )
p st+u (e 1 ) P A running (π((ℓ 1 , u))) dµ st (u)

å dλ(t) = 1 2 1 0 Ç 1 t 1 2 1 1 -t dλ(u) å dλ(t) = 1 4 .
In a similar way one can show that P A running (π(s 0 , e 1 n )) = 1 2 n , for n ∈ N; and thus conclude that P A running (π(s 0 , e 1 ω )) = 0. 3.2. Measuring Zeno runs. In timed automata, and more generally in continuous-time models, some behaviours are Zeno. Recall that a run ̺ = s 0

ℓ 0 x≤1 ℓ 1 x≤4 {p 1 } ℓ 2 x≤2 {p 2 } ℓ 3 {p 1 } e 2 , x≤1
τ 1 ,e 1 ---→ s 1 τ 2 ,e 2 ---→ . . . of a timed automaton is Zeno if ∞ i=1 τ i < ∞ (i.e.
, infinitely many actions happen in a finite amount of time). Zeno behaviours are problematic since they most of the time have no physical interpretation. As argued in [START_REF] Desharnais | Continuous stochastic logic characterizes bisimulation of continuous-time Markov processes[END_REF], some fairness constraints are often put on executions, enforcing non-Zeno behaviours, but in probabilistic systems, probabilities are supposed to replace fairness assumptions, and it is actually the case in continuous-time Markov chains in which Zeno runs are negligible (that is, have probability 0) [START_REF] Baier | Modelchecking algorithms for continuous-time Markov chains[END_REF].

We observe that, for any stochastic timed automaton A, the set of Zeno behaviours from a state s is measurable. It can indeed be expressed as M ∈N n∈N (e 1 ,...,en)∈E n π τ 1 +...+τn≤M (s, e 1 . . . e n ) .

It therefore makes sense to compute the probability of Zeno behaviours, and to check whether Zeno behaviours are negligible or not. Being negligible would be a desirable property, as argued before. However, in general this is hopeless since some timed automata are inherently Zeno. For instance, all runs are Zeno in the automaton consisting of a single location with a non-resetting loop guarded by x ≤ 1. In the following, we will discuss Zenoness for several classes of stochastic timed automata.

In the rest of the paper, if A is a stochastic timed automaton and ̺ is a run of A, we write ̺ |= Zeno whenever ̺ is Zeno. If s is a state of A, we then also write P A (s |= Zeno) for the probability of the set of Zeno runs in A from s. We associate the following decision problem, that we call almost-sure non-Zenoness problem: given A a stochastic timed automaton, and s a state of A, does P A (s |= Zeno) = 0? 3.3. From timed automata to timed region automata. In this part we establish a strong relation between a stochastic timed automaton and its stochastic timed region automaton. We let A, µ A , w A be a stochastic timed automaton. The structure of the corresponding stochastic timed region automaton is obviously R(A). We need now to choose properly probability measures µ R(A) and weights w R(A) for R(A) so that measures of runs are preserved via the mapping ι mentioned in Section 2.2. We assume that the probability measures in R(A) satisfy the following conditions: for every state s in A,

µ A s = µ R(A)
ι(s) , and for every edge e ∈ E, w A (e) = w R(A) (f ) whenever f corresponds to e. Under those conditions we show the following transfer properties between A and R(A).

Lemma 3.4. Let A, µ A , w A be a stochastic timed automaton, and let R(A), µ R(A) , w R(A) be the corresponding stochastic timed region automaton as defined above. Then, for every set S of runs in A we have:

S ∈ Ω s A iff ι(S) ∈ Ω ι(s) R(A)
, and in this case P A (S) = P R(A) (ι(S)). To establish Lemma 3.4 it is sufficient to prove that the measures coincide on finite constrained paths, since it implies that they agree on cylinders and by uniqueness of the extension on any measurable set of infinite runs. The complete proof is given in Appendix A, page 43.

Thanks to Lemma 3.4, we will be able to lift results proven on R(A) to A.

3.4. Almost-sure satisfaction. Let A, µ, w be a stochastic timed automaton over AP and s be a state of A.

We refine the notion of timed properties that were defined in Section 2.3.

Let P ⊆ 2 AP • Ä R + • 2 AP
ä ω be a timed property over AP. We say that P is (A, s)-measurable whenever

P A,s ∈ Ω s A .
We say P is A-measurable (resp. measurable) whenever it is (A, s)-measurable for every state s (resp. it is A-measurable for every A).

The following lemma establishes the measurability of several classes of properties, and is proven in Appendix A, page 44. Lemma 3.5. ω-regular properties and properties given as LTL formulas are measurable. Timed properties given as specification Büchi or Muller timed automata are measurable.

In the sequel, if P is a measurable property over AP, we write P A (s |= P ) for

P A {̺ ∈ Runs(A, s) | ̺ |= P }.
Definition 3.6. Let s be a state of A. Assume P is an (A, s)-measurable property over AP. We say that A almost-surely satisfies P , from s, and we then write A, s |≈ P P , whenever P A (s |= P ) = 1. The almost-sure model-checking problem asks, given A, s and P , whether A, s |≈ P P .

The following corollary is an immediate consequence of Lemma 3.4.

Corollary 3.7. Let A be a stochastic timed automaton, s a state of A, and ϕ a measurable property over AP. Then,

A, s |≈ P ϕ ⇔ R(A), ι(s) |≈ P ϕ .
Example 3.8. Consider A running again from Figure 3, and reproduced below, with initial state s 0 = (ℓ 0 , 0) and assuming uniform distributions over delays and uniform distribution over discrete moves in all states. Then, A running , s

0 |≈ P F (p 1 ∧ G (p 1 ⇒ F p 2 ))
. Indeed, in state (ℓ 0 , ν) with 0 ≤ ν ≤ 1, the probability of firing e 2 (after some delay) is always 1/2 (guards of e 1 and e 2 are the same, there is thus a uniform distribution over the two edges), the location ℓ 1 is eventually reached with probability 1. In ℓ 1 , the transition e 3 will unlikely happen, because its guard x = 1 is too much "small" compared to the guard x ≥ 3 of the transition e 4 . The same phenomenon arises in location ℓ 2 between the transitions e 5 and e 6 . In conclusion, the runs of the timed automaton A running (from s 0 ) almost surely follow sequences of transitions of the form e 1 * e 2 (e 4 e 5 ) ω . Hence, with probability 1, the formula

F (p 1 ∧ G (p 1 ⇒ F p 2 )
) is satisfied. Note that the latter formula is not satisfied in A running from s 0 (under the classical LTL semantics), since some runs violate it: 'staying in ℓ 0 forever ', 'reaching ℓ 3 ', etc... All these counter-examples are unlikely and vanish thanks to our probabilistic semantics. Our aim is to decide the almost-sure model-checking problem. It is clear that given a measurable property P , the value P A (s |= P ) depends on the measures µ and w. However, we show later that whether A, s |≈ P P is independent of the precise values of µ and w.

ℓ 0 x≤1 ℓ 1 x≤4 {p 1 } ℓ 2 x≤2 {p 2 } ℓ 3 {p 1 } e 2 , x≤1
To prove this, we design a finite abstraction, independent of µ and w, which is correct for deciding the almost-sure model-checking problem in a number of classes of stochastic timed automata.

A topological semantics

In [START_REF] Varacca | Temporal logics and model checking for fairly correct systems[END_REF] almost-sure model-checking of concurrent reactive systems is characterised by a topological notion: largeness is qualitative and captures the notion of "many runs". Inspired by that work, we propose a topological semantics for timed automata, based on the notion of large sets, which will help us characterise almost-sure sets. In our context also, the topological semantics is purely qualitative but nevertheless gives information on "how big" a set of paths satisfying a given property is.

In this section, relying on a notion of thickness for symbolic paths, we first define a natural topology over infinite runs of a given timed automaton. This topology induces a large semantics: an ω-regular property is satisfied if "most of the runs" satisfy it. As pointed out already in [START_REF] Varacca | Temporal logics and model checking for fairly correct systems[END_REF], largeness, and its complement meagerness, are better appropriate than density to express a notion such as "most of the runs". Indeed, "small" sets can be dense, and the complement of a dense set can also be dense (e.g. Q in R), whereas it is not the case for large sets. Let us start this section by recalling the notion of large sets and their characterisation using Banach-Mazur games.

4.1. Largeness and the Banach-Mazur game. We refer to [START_REF] Munkres | Topology[END_REF] for basic notions of topology (topological space, interior, closure, etc). However we recall here the more specific notion of largeness and also provide its elegant characterisation in terms of Banach-Mazur games [START_REF] Oxtoby | The Banach-Mazur game and Banach category theorem[END_REF].

4.1.1. Some topological notions. Let (A, T ) be a topological space. If B ⊆ A, we denote by B (resp. B) the interior (resp. closure) of B. Let us recall that a set T ′ ⊆ T is called a basis for the topology T if every open set (i.e., elements of T ) can be obtained as the union of elements of T ′ . In this case, the elements of T ′ are called basic opens. A set B ⊆ A is nowhere dense if the interior of the closure of B is empty, i.e., B = ∅. A set is meagre if it is a countable union of nowhere dense sets. Finally, a set is large if its complement is meagre.

Example 4.1. Let R be the set of real numbers equipped with its natural topology (that is, basic open sets are the open intervals). The set of integers Z is nowhere dense in R. The set of rational numbers Q is dense (in R) however Q is meagre since is a countable union of singletons (which are clearly nowhere dense sets); this implies that R \ Q is large. 4.1.2. Banach-Mazur game. Although the notion of largeness is quite abstract, it admits a very nice characterisation in terms of a two-player game, known as Banach-Mazur game. Definition 4.2 (Banach-Mazur game). Let (A, T ) be a topological space and B be a family of subsets of A satisfying the two following properties:

• for all B ∈ B, B = ∅, and • for all O a non-empty open set of A, there exists B ∈ B such that B ⊆ O. Fix C a subset of A. Two players alternate their moves: Player 1 starts and chooses an element B 1 of B; Player 2 then responds by choosing an element B 2 of B such that B 1 ⊇ B 2 ; Then Player 1 chooses B 3 in B such that B 2 ⊇ B 3 , and so on. This way, they define a non increasing sequence of sets B i :

A ⊇ B 1 ⊇ B 2 ⊇ B 3 • • •
where the B 2i+1 's (resp. B 2i 's) are chosen by Player 1 (resp. Player 2), for i ∈ N. Player 1 wins the game if the intersection of all B i 's intersects C, i.e.,

∞ i=1 B i ∩ C = ∅ .
Otherwise, Player 2 wins the game.

Notice that typical examples of family B are provided by topology bases. Banach-Mazur games are not always determined, even for simple topological spaces (see [Oxt57, Remark 1]). Still a natural question is to know when the players have winning strategies. The following result gives a partial answer: Theorem 4.3 (Banach-Mazur [START_REF] Oxtoby | The Banach-Mazur game and Banach category theorem[END_REF]). Player 2 has a winning strategy in the Banach-Mazur game with target set C if and only if C is meagre.

To illustrate Theorem 4.3 we give the following simple example.

Example 4.4. Let (R, T ) be the set of real numbers equipped with the natural topology, B be the family of open intervals with rational bounds, and C be the open set (0, 1). Intuitively, (0, 1) is not meagre, and to prove it using Theorem 4.3, it is sufficient to show that Player 2 does not have a winning strategy in the Banach-Mazur game on B with target set C.

Assume Player 1's first move is to pick the set C for B 1 . From then on, the game takes place within C, and the only way for Player 2 to win is to build a sequence of B i 's converging to the empty set. Let us now explain how Player 1 can prevent this from happening. Let

B 2i = (a i , b i ) be the ith set chosen by Player 2. Player 1's response to (a i , b i ) is the interval B 2i+1 = (a i + ǫ i , b i -ǫ i ), where ǫ i = b i -a i 3 . Notice that B 2i+1 is a regular move for Player 1 since B 2i ⊇ B 2i+1 and B 2i+1 ∈ B. Notice also that the closed set F i = [a i + ǫ i 2 , b i -ǫ i 2 ] satisfies the following inclusions: B 2i ⊇ F i ⊇ B 2i+1 .
Given any strategy of Player 2, using the above strategy Player 1 ensures:

∞ i=1 B i ∩ C = ∞ i=1 F i .
This intersection is guaranteed to be non-empty by Heine-Borel theorem, since the sequence is included in [0, 1] which is a compact set. As a consequence, Player 2 does not have a winning strategy, and thus C is non meagre. A topological space in which all non-empty open sets are not meagre is called a Baire space. 7 As we have just noticed, not all topological spaces are Baire spaces. Indeed, under their natural topologies, Q is not a Baire space whereas R is (a proof follows the same ideas than in Example 4.4). This remark suggests that largeness and meagerness are even more relevant in Baire spaces. 4.2. Thick and thin symbolic paths. We fix a timed automaton A = (L, X, E, I, L) for the rest of the section. In order to attach a topology to sets of infinite runs in A, we first define thick symbolic paths. In R n , open sets are among those sets of maximal dimension. Symbolic paths do not exactly lie in R n , but we will see that each symbolic constrained path of length n can be embedded in some ambient space R m , with m ≤ n. Thick symbolic paths will then naturally arise as symbolic paths of maximal dimension in their ambient space. Before going to the definition, let us explain through an example the intuition behind this notion.

Example 4.6. Consider the single-clock timed automaton depicted in Figure 4, s 0 = (ℓ 0 , 0) and π be the (unconstrained) symbolic path π(s 0 , e 1 e 2 ). One can naturally associate a polyhedron of (R + ) 2 with π:

Pol(π) = {(τ 1 , τ 2 ) ∈ (R + ) 2 | ̺ = s 0 τ 1 ,e 1 ---→ s 1 τ 2 ,e 2 ---→ s 2 } = {(τ 1 , τ 2 ) ∈ (R + ) 2 | (0 ≤ τ 1 ≤ 2) ∧ (0 ≤ τ 1 + τ 2 ≤ 5)} Pol(π) has dimension 2 in R 2 .
Since it is of maximal dimension, we say that the symbolic path π is thick. Consider now the symbolic path π ′ = π(s 0 , e 1 e 3 ). The polyhedron Pol(π ′ ) associated with π ′ has dimension 1, and is somehow embedded in a two-dimensional space (due to the existence of the edge e 2 ). In that case, we say that it is thin.

The above example is simplistic and could give the wrong impression that symbolic paths with singular transitions (i.e.. transitions that do not increase the dimension of the polyhedron) are necessarily thin; or equivalently that in order to be thick, a symbolic path of length n should have an associated polyhedron of dimension n. This is not always the case, and singular transitions can play an important role. Consider a slight modification of the automaton of Figure 4 where edge e 1 is guarded by x = 2. In this modified automaton, π(s 0 , e 1 e 2 ) is still thick, π(s 0 , e 1 e 3 ) is thick too and the dimension of the ambient space of any symbolic path of length 2 is 1.

To formally define thick and thin paths, we introduce the notion of associated polyhedron, and some notations. Given π C = π C (s, e 1 . . . e n ) a constrained path of a timed automaton A, its associated polyhedron is defined as follows:

Pol(π C ) = {(τ i ) 1≤i≤n ∈ (R + ) n | s τ 1 ,e 1 ---→ s 1 • • • τn,en ---→ s n ∈ π C (s, e 1 . . . e n )} .
Moreover, for each 0 < i ≤ n, we write C i for the constraint induced by the projection of Pol(π C ) over the variables corresponding to the i first coordinates (with the convention that C 0 is true).

Definition 4.7. The constrained path π C = π C (s, e 1 . . . e n ) is thin whenever there exists some index 1

≤ i ≤ n such that dim Pol Ä π C i (s, e 1 . . . e i-1 e i ) ä < dim e Pol Ä π C i-1 (s, e 1 . . . e i-1 e) ä . Otherwise π C is thick.
Clearly enough all extensions of thin symbolic paths are thin as well. Let us examine an example illustrating some subtlety of this notion.

Example 4.8. Consider the timed automaton depicted in Figure 5 where e i denotes the transition ending in ℓ i , for i = 1, 2, 3. Consider the (unconstrained) symbolic paths π(s 0 , e 1 e 2 ) and π(s 0 , e 1 e 3 ), where s 0 = (ℓ 0 , 0), and let us argue that π(s 0 , e 1 e 2 ) is thin, whereas π(s 0 , e 1 e 3 ) is thick. Intuitively, this difference comes from the fact that "reaching ℓ 2 " is only possible when transition e 1 has been taken exactly when the value of the clock x is 0, although "reaching ℓ 3 " is always possible after transition e 1 has been taken. Formally: Pol(π(s 0 , e 1 e 2 )) = {(0, 0)} whereas Pol(π(s 0 , e

ℓ 0 x≤1 ℓ 1 x≤1 ℓ 2 ℓ 3 e 1 , x≤1 e 2 , x=0 e 3 , x=1
1 e 3 )) = {(τ 1 , τ 2 ) ∈ [0, 1] 2 | τ 1 + τ 2 = 1}. Hence, dim Pol Ä π(s 0 , e 1 e 2 ) ä < dim Pol Ä π(s 0 , e 1 e 3 ) ä = dim e Pol Ä π(s 0 , e 1 e) ä
proving the desired result.

The latter example shows that thickness cannot be tested locally: edges e 2 and e 3 are both guarded by equality constraints, but do not behave the same with respect to thickness. This phenomenon cannot happen in timed region automata, in which, as we shall establish later (see Proposition 5.4, page 21), thickness coincides with local thickness.

The notion of thickness naturally extends to infinite symbolic paths.

Definition 4.9. An infinite symbolic path π C (s, e 1 e 2 . . .) is thick if for all n ≥ 1, π C (s, e 1 . . . e n ) is thick. Otherwise, it is thin.

We illustrate these notions on our running example.

Example 4.10. On A running of Figure 3, also reproduced below, with s 0 = (ℓ 0 , 0), let us explain why π(s 0 , e 1 ω ) is thick and π(s 0 , e 2 e 3 e ω 1 ) is thin. First observe that all finite prefixes π(s 0 , e n 1 ) of π(s 0 , e 1 ω ) are thick. Indeed,

ℓ 0 x≤1 ℓ 1 x≤4 {p 1 } ℓ 2 x≤2 {p 2 } ℓ 3 {p 1 } e 2 , x≤1
Pol(π(s 0 , e 1 n )) = {(τ 1 , . . . , τ n ) ∈ (R + ) n | (0 ≤ τ 1 ≤ 1) ∧ • • • ∧ (0 ≤ τ 1 + • • • + τ n ≤ 1)} .
Thus, clearly enough dim(Pol(π(s 0 , e 1 n ))) = n, which is maximal for an n-dimension polyhedron. This proves that π(s 0 , e 1 n ) is thick, for all n ∈ N, and thus π(s 0 , e 1 ω ) is thick too.

Consider now the infinite path π(s 0 , e 2 e 3 e ω 1 ) and show that it is thin by exhibiting a thin finite prefix. Observe that:

Pol(π(s 0 , e 2 e 3 )) = {(τ 1 , τ 2 ) | (0 ≤ τ 1 ≤ 1) ∧ (0 ≤ τ 1 + τ 2 = 1)} , Pol(π(s 0 , e 2 e 4 )) = {(τ 1 , τ 2 ) | (0 ≤ τ 1 ≤ 1) ∧ (3 ≤ τ 1 + τ 2 )} ,
thus dim(Pol(π(s 0 , e 2 e 3 ))) = 1 < dim(Pol(π(s 0 , e 2 e 4 ))) = 2 which implies that π(s 0 , e 2 e 3 ) is thin. Hence we conclude that π(s 0 , e 2 e 3 e ω 1 ) is thin. Second, regarding our initial objective of expressing a notion of "most of the runs" using largeness, we need, for consistency, the space to be Baire (see Remark 4.5); This is stated below and proven in Appendix B, page 46. Proposition 4.12. For every state s of A, the topological space (Runs(A, s), T s A ) is a Baire space. Now that the validity of our topology is clear, we illustrate it on our running example.

Example 4.13. On the running automaton A running of Figure 3 with initial state s 0 = (ℓ 0 , 0), the set C def = i∈N π(s 0 , e 1 i e 2 (e 4 e 5 ) ω ) is large. To prove it (or equivalently to prove that the complement of C is meagre) we use a Banach-Mazur game, and show that Player 2 has a strategy to avoid the complement of C, that is to reach C. The game is played with the basic open sets of Runs(A running , s 0 ). A winning strategy for Player 2 goes as follows:

• Assume Player 1 has chosen a cylinder Cyl(π(s 0 , e 1 n 1 )), for some n 1 ∈ N 0 (if Player 1 leaves ℓ 0 at her first move, we skip the first move of Player 2) • Player 2 chooses Cyl(π(s 0 , e 1 n 1 e 2 )), • Notice that Player 1 is not allowed to extend the symbolic path π(s 0 , e 1 n 1 e 2 ) with sequences of transitions including e 3 or e 6 , since both symbolic paths π(s 0 , e 1 n 1 e 2 e 3 ) and π(s 0 , e 1 n 1 e 2 e 4 e 6 ) are thin. Therefore Player 1 can only play moves of the form Cyl(π(s 0 , e 1 n 1 e 2 (e 4 e 5 ) n 2 )) or Cyl(π(s 0 , e 1 n 1 e 2 (e 4 e 5 ) n 2 e 4 )). • Player 2 then responds Cyl(π(s 0 , e 1 n 1 e 2 (e 4 e 5 ) n 3 )), with n 3 > n 2 .

One can easily be convinced that repeating infinitely often the last two moves, the play forms a run of C, proving that Player 2 wins the game and thus that C is large. Notice that both players could also play with constrained paths. This would not be interesting for Player 1, since it may cause the intersection to be empty (in which case Player 2 wins as well).

We now give a simple characterisation of the basic open sets considered in Definition 4.11, whose proof is given in Appendix B, page 48. Definition 4.15. Let s be a state of A, and P be a timed property over AP. We say that A largely satisfies P from s, and write A, s |≈ T P , if the set {̺ ∈ Runs(A, s) | ̺ |= P } is topologically large (in (Runs(A, s), T s A )). Let us illustrate this notion of large satisfaction on our running example.

Example 4.16. On the running example A running depicted below, with s 0 = (ℓ 0 , 0),

A running , s 0 |≈ T F (p 1 ∧ G (p 1 ⇒ F p 2 )) . ℓ 0 x≤1 ℓ 1 x≤4 {p 1 } ℓ 2 x≤2 {p 2 } ℓ 3 {p 1 } e 2 , x≤1

4.5.

From timed automata to timed region automata. As in the context of probabilities, we can relate the topologies in A and in R(A). Although the topological spaces given by A and R(A) are not homeomorphic, the topologies in A and in R(A) are somehow equivalent, as stated by the next lemma. This will allow us to lift result from R(A) to A.

Lemma 4.17. Let ι : Runs(A, s) → Runs(R(A), ι(s)) be the projection of runs in A onto the region automaton R(A). Then ι is continuous, and for every non-empty open set

O ∈ T s A , • ῑ(O) = ∅.
The proof of this lemma is given in Appendix B, page 48.

Remark 4.18. Note that ι : Runs(A, s) → Runs(R(A), ι(s)) is not an homeomorphism since ι -1 : Runs(R(A), s) → Runs(A, ι -1 (s)) is not continuous. Indeed, let us consider the automaton A of Figure 2, page 8, with s 0 = (ℓ 0 , 0). The set of runs O = Cyl(π(s 0 , e 1 )) is open in T s 0 A since π(s 0 , e 1 ) is a thick symbolic path. However, ι(Cyl(π(s 0 , e 1 ))

) = Cyl(π(s 0 , f 1 ))∪Cyl(π(s 0 , f 2 )) is not open in T ι(s 0 ) R(A) as π(s 0 , f 1 ) is thin and hence Cyl(π(s 0 , f 1 )) is not a basic open. Thus ι(O)
is not open and ι -1 is not continuous. Lemma 4.17 allows one to simulate a Banach-Mazur game from A to R(A) and viceversa. Therefore, the large satisfaction relations in A and R(A) coincide, see Appendix B, page 50. Proposition 4.19. Let s be a state of A, and P be a timed property over AP. Then, A, s |≈ T P ⇔ R(A), ι(s) |≈ T P .

Construction of the thick graph

In this section, we construct the so-called thick graph. The idea is to remove locally thin edges from the region automaton, and it will be used to characterise (globally) thin paths.

We fix a timed automaton A = (L, X, E, I, L), and we start by defining a local notion of thinness.

Definition 5.1. Let e be an edge of R(A), and q its source. We say e is thin whenever dim(I(s, e)) < dim(I(s)) for some (or equivalently, for every) s ∈ q. Otherwise the edge is said thick.

An equivalent definition is that an edge e with source q is thin whenever for every s ∈ q, the length-1 constrained path π(s, e) is thin. That is why this notion of thinness is local. Next we will write dim(I(q, e)) (resp. dim(I(q))) instead of dim(I(s, e)) (resp. dim(I(s))) for every s ∈ q since this is independent on s ∈ q.

Definition 5.2. The thick graph of A, denoted G t (A), is obtained from R(A) by deleting all the thin edges.

In particular, G t (A) has only thick edges. We first state a lemma, which explains how the dimension of symbolic paths grows in the (timed) region automaton. Its proof can be found in Appendix C, page 50 Lemma 5.3. Let π(s, e 1 . . . e n ) be a symbolic path of R(A). Assuming Pol(π(s, e 1 . . . e n )) = ∅ and letting q be the target region of π(s, e 1 . . . e n-1 ), dim(Pol(π(s, e 1 . . . e n ))) = dim(Pol(π(s, e 1 . . . e n-1 ))) + dim(I(q, e n )).

That is, we are able to compute the global dimension of a symbolic path, given the dimension of each of its edges. Notice that this is only true in the region automaton. As an example, in the timed automaton of Example 4.8, Pol(π(s, e 1 e 2 )) = {(0, 0)}, whereas Pol(π(s, e 1 )) = [0, 1].

The following proposition states the correctness of the thick graph, in the sense that a symbolic path is (globally) thin if and only if it traverses a (locally) thin edge. Its proof is given in Appendix C, page 51.

Proposition 5.4. Let π = π(s, e 1 . . . e n ) be a symbolic path in R(A). Then, π is thin in R(A) iff there exists 1 ≤ i ≤ n such that e i is thin.

The thick graph will be used in the next section for characterising large and almost-sure satisfaction. It will later be used for algorithmic issues.

Example 5.5. We illustrate the construction of the thick graph on the running example. Figure 6 represents the classical region graph where thick (resp. thin) edges are depicted bold (resp. dashed). From that region graph, by removing thin edges and keeping only the states reachable from the initial one, we obtain the thick graph, represented on Figure 7. Remark 5.6. In the following, we will denote by MC(A) the finite Markov chain obtained by taking G t (A) as the support of the Markov chain, and assuming uniform distributions over edges. In the next sections, we write MC(A), s |≈ P whenever the finite Markov chain MC(A) almost-surely satisfies property P from state s.

ℓ 0 ,0 ℓ 0 ,(0,1) ℓ 0 ,1 ℓ 1 ,0 ℓ 1 ,(0,1) ℓ 1 ,1 ℓ 2 ,0 ℓ 3 ,0 ℓ 3 ,(0,1) ℓ 3 ,
6. When do the large and the almost-sure satisfaction coincide?

We know that large satisfaction and almost-sure satisfaction coincide for finite automata for several classes of properties [START_REF] Varacca | Temporal logics and model checking for fairly correct systems[END_REF]. We want here to discuss situations where almost-sure and large satisfactions also match in our context. This will help giving algorithmic solutions to the almost-sure model-checking problem using the thick graph. We fix for this section a stochastic timed automaton A, µ, w .

6.1. Safety properties. We first compare the two semantics in the restricted case of safety properties. Let us first state this simple result that, in a region automaton, a finite symbolic path has probability 0 iff it is thin. This is the first easy link we can make between the probabilities and the topology. Note that this correspondence does not depend on the choice of the probability distributions.

Proposition 6.1. Consider a finite symbolic path π = π(s, e 1 . . . e n ) in R(A). Then, P R(A) (Cyl(π)) > 0 iff π is thick. Equivalently, P R(A) (Cyl(π)) = 0 iff π is thin.

This proposition relies on condition (⋆) on the probability distributions µ (cf page 11): if an edge is thick, it is either because it has dimension 1, or because it has dimension 0, but all other outgoing edges also have dimension 0. In the first case, the measure µ must be equivalent to the Lebesgue measure, and in the second case, it will give a positive mass to the edge. The full details of the proof are given in Appendix D.1, page 52.

Using this result, we show that the large and the almost-sure satisfaction always coincide when we restrict to safety properties. Theorem 6.2. Let s be a state of A, and P be a(n untimed) safety property over AP. Then the four following properties are equivalent: This result relies on the fact that safety properties are violated by finite prefixes. Proposition 6.1 then tells us that such finite prefixes yield positive probability whenever they are thick. We can then play a Banach-Mazur game in the topological space of the automaton, where only thick paths can be used by the players as moves. This allows to show that property ¬P is meagre iff P is not violated by thick prefixes, that is when ¬P has probability 0. The details of the proof are given in Appendix D.1, on page 52.

As said, the proof of Theorem 6.2 heavily relies on the fact that witnesses of violation (resp. validation) for safety (resp. reachability) properties are finite prefixes. Not surprisingly, Theorem 6.2 does not hold for general LTL or ω-regular properties, for which the violation cannot always be witnessed by finite prefixes. As an example, consider the timed automaton of Figure 8, and the property F p. The probability of F p is indeed 1 in this automaton, although the infinite symbolic path π((ℓ 0 , 0), e ω 0 ) violates F p and is thick.

ℓ 0 ℓ 1 {p} e 0 , x≤1 e 1 , x≤1
Figure 8: A counterexample for Theorem 6.2 beyond safety.

This kind of behaviours motivates the restriction to fair paths, which is rather natural since probabilities and strong fairness are closely related [Pnu83, PZ93, BK98]. 6.2. Restriction to fairness: the case of prefix-independent properties. Motivated by the counterexample of Figure 8, we define a natural notion of fairness for infinite symbolic paths in timed automata. Definition 6.3. An infinite region path π = q 0 e 1 -→ q 1 e 2 -→ q 2 . . . of R(A) is fair iff for every thick edge e, if e is enabled in infinitely many q i (i ∈ N), then e i = e for infinitely many i ∈ N.

Fairness extends to runs and symbolic paths in an obvious way as detailed below. Region paths and symbolic paths in R(A) are closely related: to any non-empty symbolic path π(s, e 1 e 2 . . .), we associate a unique region path q 0 e 1 -→ q 1 e 2 -→ q 2 . . . with s ∈ q 0 and q i is the target region of edge e i . We then say that a symbolic path π(s, e 1 e 2 . . .) in R(A) is fair whenever its corresponding region path is fair. Finally we say that an infinite run ̺ in R(A) is fair whenever π ̺ (its underlying symbolic path) is fair. Obviously, the set of fair infinite runs from s is measurable (that is, in Ω s R(A) ), as fairness is an ω-regular property over infinite paths. We now turn the definition from R(A) to A: an infinite run ̺ in A is fair whenever ι(̺) is fair.

We write fair for this property, that is if an infinite run ̺ (in A or in R(A)) is fair, then we write ̺ |= fair. We then write P A (s |= fair) (resp. P R(A) (ι(s) |= fair)) for the probability of fair runs in A from s (resp. in R(A) from ι(s)). We say that A (resp. R(A)) is almost-surely fair from s (resp. ι(s)) whenever P A (s |= fair) = 1 (resp. P R(A) (ι(s) |= fair) = 1).

Let us state the following straightforward lemma, which gives a useful characterisation of thick and fair symbolic paths in the region automaton. Lemma 6.4. Let s be a state of A, and P be a prefix-independent property over AP. Then, the two following properties are equivalent:

(i) all BSCCs 9 reachable from [s] in G t (A) satisfy P ; 10 (ii) every infinite thick and fair symbolic path π from ι(s) in R(A) satisfies P ;

(iii) MC(A), ι(s) |≈ P . We write §(A, s, P ) for this property.

6.2.1. Fairness and topology. Even though fairness is introduced because of the probabilities, we first realise that adding fairness to paths allows to characterise the large satisfaction.

More precisely, we prove the following result, which is rather similar to Theorem 6.2, when restricted to topology.

Theorem 6.5. Let s be a state of A, and P be a prefix-independent property over AP.

Then: A, s |≈ T P ⇔ §(A, s, P ) .

Proof. First assume that A, s |≈ T P . This equivalently means that R(A), ι(s) In this game, Player 2 has a strategy to ensure that i B i ∩ ¬P R(A),ι(s) = ∅, where the B i 's are the moves in the game. Let us denote Σ 2 this winning strategy. Fix any BSCC C of G t (A) reachable from [s], and let {ℓ 1 , . . . , ℓ p } be an enumeration of the locations in C. In order to prove that C satisfies P , we will build a symbolic path π, played according to Σ 2 (and thus satisfying P ), witnessing that C satisfies P . Let Player 1 play as follows (against Σ 2 ): at her first move, Player 1 chooses B 1 leading to ℓ 1 ; then, no matter which 9 BSCC stands for 'bottom strongly connected component', see e.g. [START_REF] Thomas | Introduction to algorithms[END_REF]. 10 We say that a prefix-independent property P is satisfied by a BSCC C whenever every run visiting infinitely often all states of C satisfies P . As P is prefix-independent, this reduces to the existence of a run satisfying P , which visits infinitely often all states of C.

|≈ T P (Lemma 4.19), that is, ¬P R(A),ι (
B 2 Player 2 chooses, Player 1 chooses B 3 (longer than B 2 ) leading to ℓ 2 ; etc. Furthermore applying a technique similar to the proof of Proposition 4.12 (compactification), Player 1 can ensure that i B i = ∅. We then get that ∅ = i B i ⊆ P R(A),ι(s) , since Σ 2 is winning for Player 2. Let π be the infinite symbolic path underlying i B i . As P is a property over AP, π |= P . Furthermore, π visits all locations of C (since Player 1 has ensured visiting all the locations of C infinitely often), which means that the BSCC C satisfies P . We conclude that all BSCCs satisfy property P .

Conversely, assume that every BSCC of G t (A) satisfies P . It is then easy to provide a winning strategy for Player 2 in the same Banach-Mazur game as described above. Once a BSCC C has been reached (after Player 1's first move or Player 2's first move), Player 2 will ensure to visit all the locations of C (as Player 1 did in the above proof). The resulting infinite path will satisfy P (by hypothesis), which implies the winning condition for Player 2.

What about fairness and probabilities?

The natural question is: can we fully extend Theorem 6.2 and therefore prove that almost-sure satisfaction is equivalent to ( §)? We concentrate on the following equivalence:

A, s |≈ P P ⇔ ® every infinite thick and fair symbolic path π from ι(s) in R(A) satisfies P ( ‡)

We show now that this equivalence is unfortunately not true in general. The counterexample to that equivalence is much more surprising than that of Figure 8. The reasons why it fails is rather subtle and is due to complex time converging behaviours. As pointed out in [START_REF] Cassez | A comparison of control problems for timed and hybrid systems[END_REF], timed automata admit various time converging behaviours, and, in our context, some of these behaviours can lead to "big" sets of unfair executions. Inspired by an example presented in [START_REF] Cassez | A comparison of control problems for timed and hybrid systems[END_REF], we design a two-clock timed automaton A unfair (see Figure 9) for which the equivalence ( ‡) does not hold. In this automaton, every (infinite) fair and thick symbolic path satisfies G F p 1 ∧ G F p 2 , and in particular F p 2 . Thus, letting ϕ = F p 2 , the right-hand side of equivalence ( ‡) is true. However, when A unfair is equipped with uniform distributions, starting in s 0 = (ℓ 0 , (0, 0)), one can show that the probability of the symbolic path π(s 0 , (e 3 e 4 e 5 ) ω ) is positive and therefore A unfair , s 0 |≈ P F p 2 . We notice that this implies P A unfair (s 0 |= fair) < 1. All this is proven formally in Appendix D.2, page 53. 6.2.3. When fairness is almost-sure. We will show that a sufficient condition to have ( ‡) is to have P A (s 0 |= fair) = 1. We can now state the following crucial theorem: Theorem 6.6. Let s be a state of A, and P be a prefix-independent (untimed) property over AP. Assuming P A (s |= fair) = 1, the following holds:

ℓ 0 ℓ 1 ℓ 2 y<1 {p 2 } ℓ 3 ℓ 4 {p 1 } y<1 e 1 , y<1 e
A, s |≈ P P ⇔ §(A, s, P ) .

Proof. First define the property thick as follows: letting ̺ be a run in R(A), ̺ |= thick iff π ̺ is thick. Applying Theorem 6.2, we get that P R(A) (s |= thick) = 1.

We now prove that P R(A) (s |= P ) > 0 iff there exists an infinite symbolic path π from s, which is thick and fair, and such that π |= P . This will imply the expected result. We prove the two implications separately.

• Proof of the left-to-right implication. Let us assume that P R(A) (s |= P ) > 0. We have seen that P R(A) (s |= thick) = 1. Therefore, thanks to the fact that

P R(A) (s |= fair) = 1, P R(A) (s |= P ) = P R(A) (s |= P ∧ fair ∧ thick). Hence, P R(A) (s |= P ∧ fair ∧ thick) > 0.
In particular, there exists a fair thick infinite path from s which satisfies P . • Proof of the right-to-left implication. Let π = π(s 0 , e 1 e 2 . . .) be a fair thick symbolic path in R(A) satisfying P . We consider the thick graph G t (A) of A. Since π is thick, π is also a path in G t (A). Let us consider the strongly connected components of G t (A). As π is a fair path, it eventually reaches a BSCC in G t (A) and from then on takes each edge of the BSCC infinitely often. Otherwise, this would mean that π ignores a thick edge forever, which would contradict the fairness assumption. Let B π be the BSCC that π eventually reaches and π pref the shortest prefix of π leading from s to B π (note that it is thick). Consider the following set of paths in R(A):

S def = {π ′ ∈ Cyl(π pref ) | π ′ is
thick and fair} .

Since P R(A) (s |= thick) = 1 and P R(A) (s |= fair) = 1, we deduce that P R(A) (S) = P R(A) (Cyl(π pref )). Moreover since π pref is thick, we obtain P R(A) (S) > 0. It now suffices to observe that all paths in S satisfy P . Indeed, the satisfiability of prefix-independent (untimed) properties over AP only depends on the set of states that are visited infinitely often, and all paths in S visit infinitely often exactly the states in B π , and π |= P .

Conclusion.

We can conclude this subsection by stating the main result concerning prefix-independent properties. It is a direct consequence of Theorems 6.5 and 6.6.

Corollary 6.7. Let s be a state of A, and P be a prefix-independent (untimed) property over AP. Assuming P A (s |= fair) = 1, the following equivalences hold:

A, s |≈ P P ⇔ A, s |≈ T P ⇔ §(A, s, P ) .

Note that characterisation ( §) will help with algorithmic issues. Complexity issues will be discussed in Section 8. 6.3. Extension to richer properties. In this section we extend the previous study to properties which are richer than prefix-independent properties, in particular to LTL properties and properties expressed as specification timed automata.

Let A, µ, w be a stochastic timed automaton with A = (L, X, E, I, L), and let B = (L, i 0 , X, AP, E, F) be a specification Büchi or Muller timed automaton. We build the product stochastic timed automaton A ⋉ B, µ, w as follows. The timed automaton A ⋉ B = (L, X ∪ X, E, I) (with no labelling function) is such that:

• L = L × L; • E is composed of the following edges: if e def = (ℓ g,Y --→ ℓ ′ ) ∈ E then for all e def = (l g,λ(ℓ),Y -----→ l ′ ) ∈ E, there is an edge ((ℓ, l) g∧g,Y ∪Y ------→ (ℓ ′ , l ′ )
) in E, which we write e e ; • I((ℓ, l)) = I(ℓ) for every (ℓ, l) ∈ L. The measures µ and the weights w are such that: • µ (ℓ,l) = µ ℓ for every (ℓ, l) ∈ L, and • w e = w e for every edge e ∈ E which comes from edge e. Given a state s = (ℓ, v) of A, we define the initial state in A ⋉ B as init A⋉B (s) def = ((ℓ, i 0 (L(s))), v0 X ); that is, we start in B from the location specified by the label of state s (this is i 0 (L(s))), with all clocks of B set to 0.

Note that any run ̺ in A from state s has a unique image in A ⋉ B from init A⋉B (s), denoted ̺ B (since B is complete and deterministic). Note that the converse also holds: for any run ̺ ′ in A ⋉ B from some init A⋉B (s), there is a unique preimage ̺ in A from s, such that ̺ ′ = ̺ B . We define the ω-regular property P A⋉B in A ⋉ B as the lifting of F in A ⋉ B (an infinite run in A ⋉ B satisfies P A⋉B whenever its projection on B satisfies the accepting condition F). As F is an internal prefix-independent condition in B, P A⋉B is an internal prefix-independent condition in A ⋉ B. Remark 6.8. It should be clear enough that A⋉B is non-blocking assuming A is. Moreover, for all states s = (ℓ, v) of A, for all states s = (l, v) of B, and for every edge e ∈ E,

I(s, e) = e=(l g,λ(ℓ),Y -----→l ′ ) I(((ℓ, l), (vv)), e e )
This allows to properly define the probability measure P A⋉B .

We can now state the main theorem for specification timed automata, which uses this product construction. Its proof is given in Appendix D.3, page 55. Theorem 6.9. Let s be a state of A, and B be a specification Büchi or Muller timed automaton. Assuming P A⋉B (init A⋉B (s) |= fair) = 1, the following holds:

A, s |≈ P B ⇔ A, s |≈ T B ⇔ §(A ⋉ B, init A⋉B (s), P A⋉B ) .
The above also applies to specification untimed automata. In particular, it also applies to specification automata corresponding to LTL formulas. It is now easy to be convinced that if B is a specification untimed automaton, then P A (s |= fair) = P A⋉B (init A⋉B (s) |= fair) since B does not restrict guards of edges, and in particular

P A (s |= fair) = 1 ⇔ P A⋉B (init A⋉B (s) |= fair) = 1 .
This allows to get the following important corollary, which characterises the almost-sure model-checking for LTL. Corollary 6.10. Let s be a state of A, and ϕ be an LTL formula over AP. Assuming P A (s |= fair) = 1, the following holds:

A, s |≈ P ϕ ⇔ A, s |≈ T ϕ ⇔ §(A ⋉ B ϕ , init A⋉Bϕ (s), P A⋉Bϕ ) .

Application to several classes of timed automata

In the previous section, we showed that, provided fairness is almost-sure, one could characterise almost-sure satisfaction and large satisfaction using thick paths. We will describe here two classes of stochastic timed automata for which this holds.

7.1. Single-clock timed automata. In this section, we focus on single-clock timed automata, and we show that, under some minor additional technical hypotheses, single-clock timed automata are almost-surely fair. In particular, Corollary 6.10 will apply, yielding the decidability of the almost-sure model-checking problem for ω-regular properties on this class of stochastic timed automata.

Let A = (L, X, E, I, L) be a single-clock stochastic timed automaton. We assume the following conditions on A, denoted ( †):

(H3): For all ℓ ∈ L, for all [a, b] ⊆ R + , the function v → µ (ℓ,v) ([a, b]) is continuous; (H4): If s ′ =
s + t for some t ≥ 0, and 0 / ∈ I(s + t ′ , e) for every 0 ≤ t ′ ≤ t, then µ s (I(s, e)) ≤ µ s ′ (I(s ′ , e)); (H5): There is 0 < λ 0 < 1 s.t. for every state s with I(s) unbounded, µ s ([0, 1/2]) ≤ λ 0 .

Remark 7.1. The three last requirements are technical and needed to properly define a probability measure over infinite runs, but they are natural and easily satisfiable. For instance, a timed automaton equipped with uniform (resp. exponential 11 ) distributions on bounded (resp. unbounded) intervals satisfy these conditions. If we assume exponential distributions on unbounded intervals, the very last requirement corresponds to the bounded transition rate condition in [START_REF] Desharnais | Continuous stochastic logic characterizes bisimulation of continuous-time Markov processes[END_REF], required to have reasonable and realistic behaviours.

Theorem 7.2. Assuming A satisfies ( †), if s is a state of A, P A (s |= fair) = 1.

The proof of this theorem is very technical. We will describe the main ingredients of the proof in the core of the paper, and postpone all details to Appendix E.

Let {c i | 0 ≤ i ≤ k} be the set of constants appearing in guards of A, assuming w.l.o.g. c 0 = 0. We know [START_REF] Laroussinie | Model checking timed automata with one or two clocks[END_REF] that the following intervals are regions for A:

{c i } for 0 ≤ i ≤ k; (c i , c i+1 ) for 0 ≤ i < k; (c k , +∞)
We assume R(A) is built with these regions. It is polynomial-size (contrary to standard region automaton which is exponential-size).

The proof of the above theorem then relies on Lemma 7.3 below. A subregion of a region q is a pair (q, J) such that J ⊆ q is an interval. If s ∈ J, we may write s ∈ (q, J) as well. If (q, J) and (q ′ , J ′ ) are subregions, we write (q, J) e -→ (q ′ , J ′ ) to express that (q, v)

τ,e --→ (q ′ , v ′ ) for some v ∈ J, v ′ ∈ J ′ and τ ∈ R + . In the sequel to ease the reading, we will use LTL-like notations, like P A (s, G F (q, J) e -→ (q ′ , J ′ ) | G F (q, J)) to denote the conditional probability of the set of runs s 0

τ 1 ,e 1 ---→ s 1 τ 2 ,e 2 ---→ s 2 • • • such that s 0 = s and {s i e i+1
--→ s i+1 | s i ∈ J, e i+1 = e, and s i+1 ∈ J ′ } is infinite, assuming that the set {s i | s i ∈ J} is infinite. We will use other similar notations, that we expect are sufficiently explicit to be understandable.

Lemma 7.3.

(1) For every subregion (q, J) of q such that (i) J is non-empty and open in q (for the induced topology), and (ii) J ⊆ q is compact, (2) for every thick edge e enabled in q, (3) for every subregion (q ′ , J ′ ) of q ′ such that for every s ∈ (q, J), e(s) ∩ J ′ is non-empty and open in q ′ (for the induced topology), where e(s)

= {s ′ | ∃τ ∈ R + s.t. s τ,e --→ s ′ }, (4) for every state s of R(A) such that P R(A) (s, G F (q, J)) > 0, 12 P R(A) (s, G F (q, J) e -→ (q ′ , J ′ ) | G F (q, J)) = 1 .
The idea of this lemma is to provide a lower-bound on the probability of firing the transition (q, J) e -→ (q ′ , J ′ ) each time we visit (q, J). By thickness of e, we know that the probability at each visit is positive, but as J is compact, we infer a positive uniform lower-bound λ. This is the main ingredient to prove the result.

Remark 7.4. This lemma holds for all timed automata, not only one-clock timed automata.

We have shown the proof for a single edge, but this lemma can be extended straightforwardly to finite sequences of edges as follows:

Lemma 7.5. (1) For all regions (q i ) 0≤i≤p , (2) for all edges (e i ) 1≤i≤p such that e i is thick and enabled in q i-1 , (3) for all subregions ((q i , J i )) 0≤i≤p such that for every 0 ≤ i < p:

(a) J i is non-empty and open in q i (for the induced topology), (b) J i ⊆ q i is compact, and (c) for every s ∈ J i , e i (s) ∩ J i+1 is non-empty and open, where e i (s) = {s ′ | ∃τ ∈ R + s.t. s

τ,e i --→ s ′ }, (4) for every state s of A such that P R(A) (s, G F (q 0 , J 0 )) > 0 it holds that:

P R(A) (s, G F σ | G F (q 0 , J 0 )) = 1
where σ = (q 0 , J 0 ) e 1 -→ (q 1 , J 1 ) . . .

ep

-→ (q p , J p ). Now, we can turn back to Theorem 7.2.

Sketch of proof of Theorem 7.2. Let s be a state in A. We want to prove that P A (s |= fair) = 1. We will equivalently prove P R(A) (ι(s) |= fair) = 1. To that purpose, we decompose the set of infinite runs in R(A) from ι(s) into: (F 1 ) the set of runs with infinitely many resets, (F 2 ) the set of runs with finitely many resets, and which are ultimately in the unbounded region (c k , +∞), (F 3 ) the set of runs with finitely many resets, and which ultimately stay forever in a bounded region, either {c i } with 0 ≤ i ≤ k, or (c i , c i+1 ) with 0 ≤ i < k. We write (F

(c i ,c i+1 ) 3 ) (resp. (F c i
3 )) for condition F 3 restricted to (c i , c i+1 ) (resp. {c i }).

BERTRAND, BOUYER, BRIHAYE, MENET, BAIER, GR ÖSSER, AND JURDZI ŃSKI

We write P R(A) (s, F j ) for the probability of the runs starting in s and satisfying condition F j . The three sets of runs above are measurable and partition the set of all runs. Hence j=1,2,3 P R(A) (s, F j ) = 1, and applying Bayes formula:

P R(A) (s |= fair) = j=1,2,3 P R(A) (s |= fair | F j ) • P R(A) (s, F j ) . (•)
We now distinguish between the three cases to prove that P R(A) (s |= fair | F j ) = 1 (in case P R(A) (s, F j ) = 0 we remove the corresponding term from (•)).

Case F 1 .: In that case, for all states (q, 0) which are visited infinitely often we apply Lemma 7.5 to any sequence of thick edges, and get the expected result for F 1 . Case F 2 .: Once the unbounded region is reached, precise values of clocks are irrelevant, and the timed automaton roughly behaves like a finite Markov chain, which yields the expected result for F 2 . Case F 3 .: We consider runs which end up in a bounded region r. This case is only possible (with positive probability) if no thick edge is enabled infinitely often with a guard above r (otherwise it would be taken infinitely often -due to the hypothesis (H4)). Therefore in this case as well the automaton ultimately behaves like a finite Markov chain, which allows to conclude with the expected property.

Note that the one-clock hypothesis is crucial for cases F 1 and F 3 .

Checking almost-sure non-Zenoness in one-clock timed automata. Note that we cannot obtain the result on Zeno behaviours from Corollary 6.10 since Zenoness is a timed property. We can neither use the product construction of Section 6.3 and Theorem 6.9 since this will increase the number of clocks to 2. Therefore we need a specific proof, that we present now. We first show the following crucial lemma.

Lemma 7.6. Assuming A satisfies ( †), if s is a state of A, then:

P A (s |= Zeno) = B Zeno BSCC of G t (A) P R(A) (ι(s) |= F B)
where a BSCC of G t (A) is said Zeno whenever it is bounded and the clock is never reset.

To prove the lemma, we need to realise that runs ending up in the unbounded region or runs with infinitely many resets have probability 0 to be Zeno. Indeed, in the first case, there will be non constraint on the clock for taking transition, and in particular, with probability 1 a delay of 1 will elapse infinitely often; in the second case, infinitely often a guard of the form 0 < x < 1 will be enabled, and therefore with probability 1, a delay of at least 1/2 will be done, yielding with probability 1 a non-zeno run. It remains those runs ending up in a bounded region, which will correspond to the right-hand side of the equality in the statement (due to fairness, the runs end up with probability 1 in a BSCC). The details are given in the Appendix on page 59.

Theorem 7.7. Assuming A satisfies ( †), if s is a state of A, then the three following properties are equivalent: (a) A, s |≈ P ¬Zeno;

(b) A, s |≈ T ¬Zeno; (c) no Zeno BSCC is reachable in G t (A) from ι(s).
This theorem is a consequence of Lemma 7.6, and uses once more Banach-Mazur games for what concerns the large satisfaction. The details are also given in the Appendix on page 62.

Corollary 7.8. The almost-sure non-Zenoness problem is NLOGSPACE for single-clock stochastic timed automata which satisfy condition ( †).

We write R(A), µ, w for the stochastic timed region automaton based on A (we abusively also write µ and w since we will not use that notation for A), and we write Q for the set of locations of R(A), and T for its set of edges. Thanks to Corollary 3.7, in order to prove Proposition 7.11, it is sufficient to prove that R(A) is almost-surely fair. In the following we denote by M the maximal constant appearing in A (or R(A)), and we write P instead of P R(A) .

To prove almost-sure fairness in R(A), we have to show that for every thick edge e, the probability to visit e infinitely often, knowing we visit source(e) infinitely often, is equal to 1. The key point of this proof lies in the fact that, since the automaton R(A) is reactive, there exists a subset of regions, called memoryless, that will be visited infinitely often with probability 1. A region r is said memoryless whenever the following holds for every clock x ∈ X: either v(x) = 0 for every v ∈ r, or v(x) > M for every v ∈ r. The interest of memoryless regions is that once you reach such a region the future (and its probability) is independent of both the finite prefix and the clock valuations. In particular, visiting infinitely often memoryless regions prevents converging phenomena as the one observed in Figure 9. For each memoryless region r, we distinguish a canonical valuation v r ∈ r defined by v r (x) = 0 or v r (x) = M + 1 for every x ∈ X (note that this valuation is uniquely defined). If q = (ℓ, r) ∈ Q is such that r is memoryless, we distinguish the canonical configuration

s q = (ℓ, v r ) (or s q = ((ℓ, r), v r ) in R(A)).
The fact that memoryless regions are visited infinitely often almost-surely is formalised in Lemma 7.13. Then it remains to show that knowing we visit infinitely often such a memoryless region, we visit a reachable thick edge e infinitely often with probability 1. To this end, we investigate the set of runs that visit infinitely often memoryless regions and e, and we conclude thanks to a judicious decomposition of this set and Borel-Cantelli lemma, this is formalised in Lemma 7.14. A sketch of proof is given for Lemma 7.13 and the complete proofs of both lemmas are provided in Appendix F, page 63.

In order to formalise these ideas, we need to introduce further notations. Let s be a state of R(A), that we will take as initial. If e is a thick edge in T , and q ∈ Q, we write R e (s) for the set of runs in R(A) that start in s and take e infinitely often, and R q (s) for the set of runs of R(A) that start in s and visit q infinitely often. In particular, we write R source(e) (s) for the set of runs that start in s and visit source(e) infinitely often (hence along which e is enabled infinitely often).

We fix a thick edge e in T , and we let Q be the set of pairs q = (ℓ, r) where r is memoryless and Q ′ the set of elements q = (ℓ, r) ∈ Q such that P(R q (s)) > 0 and P(R q,e 0 (s q )) > 0 where R q,e 0 (s q ) is the set of runs that start from s q and take e before any other visit to q. Lemma 7.13. Assuming the above notations,

P Ñ q∈Q R q (s) é = 1 .
Sketch of proof. We notice that the set of runs that delay infinitely many times more than M time units before taking a transition is a subset of q∈Q R q (s). Indeed, if a run ̺ delays more than M time units before taking the n-th transition then each clock is either reset on the n-th transition (hence its value is 0), or its value exceeds M . Now, as for every ℓ ∈ L, we have assumed µ ℓ is equivalent to the Lebesgue measure on R + , it holds that µ ℓ ([0, M ]) < 1.

We can then prove that the probability of the set of runs that delay only finitely many times more than M time units is zero, since L is finite, which concludes the proof.

Lemma 7.14. Assuming the above notations, for all q ∈ Q ′ P (R e (s) | R q (s)) = 1. Now assuming Lemma 7.13 and Lemma 7.14, we will prove Proposition 7.11.

Proof of Proposition 7.11. We want to prove that the probability of being fair is 1, hence we want to prove that for every thick edge e with P(R source(e) (s)) > 0,

P Ä R e (s) | R source(e) (s) ä = 1 .
Let e be a thick edge with P(R source(e) (s)) > 0. By Lemma 7.13, we have that

P Ñ q∈Q R q (s) é = 1, (7.1)
and by Lemma 7.14, we have that

P (R e (s) | R q (s)) = 1 (7.2)
for any q ∈ Q ′ . Applying Lemma 7.12 (point 3.), we deduce from Equation (7.2) that

P Ñ R e (s) | q∈Q ′ R q (s) é = 1 (7.3)
and applying Lemma 7.12 (point 1.), we deduce from Equation (7.1) that:

P Ñ q∈Q R q (s) | R source(e) (s) é = 1. (7.4)
Moreover, we can easily show that

P Ñ q∈Q R q (s) | R source(e) (s) é = P Ñ q∈Q ′ R q (s) | R source(e) (s) é . (7.5)
Indeed, we just have to prove that

P Ñ q∈Q R q (s) ∩ R source(e) (s) é = P Ñ q∈Q ′ R q (s) ∩ R source(e) (s) é
and it is thus sufficient to prove that

P Ñ q∈Q\Q ′ R q (s) ∩ R source(e) (s) é = 0 .
However, if q ∈ Q\Q ′ , we have P(R q (s)) = 0 or P(R q,e 0 (s q )) = 0. Now, if P(R q (s)) = 0, we have

P Ä R q (s) ∩ R source(e) (s) ä = 0
and if P(R q,e 0 (s q )) = 0, we also have

P Ä R q (s) ∩ R source(e) (s) ä = 0 .
We therefore deduce from Equations (7.4) and (7.5) that

P Ñ q∈Q ′ R q (s) | R source(e) (s) é = 1 . (7.6)
Applying Lemma 7.12 (point 2.), we get the expected result from Equations (7.3) and (7.6):

P Ä R e (s) | R source(e) (s) ä = 1 .
7.2.1. Extension to weak reactive stochastic timed automata. We now extend the almostsure fairness from the subclass of reactive stochastic timed automata to the larger class of weak reactive stochastic timed automata, defined as follows.

Definition 7.15. A stochastic timed automaton A, µ, w with A = (L, X, E, I, L) is said to be weak reactive whenever L is the disjoint union of sets L u and L b such that ℓ ∈ L u if and only if I(ℓ, v) is unbounded for all v such that v |= I(ℓ), and:

• for every pair s = (ℓ, v), s ′ = (ℓ, v ′ ) satisfying for every x ∈ X, v(x) = v ′ (x) or min(v(x), v ′ (x)) > M , µ s = µ s ′ ;
• there exists 0 < λ 0 ≤ 1 such that for every ℓ ∈ L u , for every v |= I(ℓ), we have that

µ (ℓ,v) ([M, +∞[ ) ≥ λ 0 ;
• there exist 0 < λ 1 ≤ 1 and N ≥ 1 such that for any ℓ ∈ L b , for every v |= I(ℓ), we have that P A (e 1 ,...,e N )∈Eu π((ℓ, v), e 1 , . . . , e N ) ≥ λ 1

where E u = {(e 1 , . . . , e N ) | target(e i ) ∈ L u for some 1 ≤ i < N }.

It is obvious that the class of reactive stochastic timed automata is a subclass of weak reactive stochastic timed automata. In fact, the main difference between these classes of automata lies on the existence of some states s such that I(s) is bounded. The proof of almost-sure fairness of reactive stochastic timed automata is based on two lemmas: Lemma 7.13 and Lemma 7.14. The proof of Lemma 7.14 works in the same way for weak reactive stochastic timed automata, using the fact that for every pair s = (ℓ, v), s ′ = (ℓ, v ′ ) satisfying for every x ∈ X, v(x) = v ′ (x) or min(v(x), v ′ (x)) > M , we have µ s = µ s ′ . The proof of Lemma 7.13 can also be adapted in view of properties of weak reactive stochastic timed automata in order to obtain the following lemma: Lemma 7.16. Let A be a weak reactive stochastic timed automaton and s be a state of A. Then

P Ñ q∈Q R q (s) é = 1 .
Thanks to these two lemmas, we deduce the almost-sure fairness for weak reactive automata as in the case of reactive stochastic timed automata: Proposition 7.17. Let A be a weak reactive stochastic timed automaton and s 0 be a state of A. Then P A (s |= fair) = 1. We end up this subsection by exhibiting some examples of weak reactive stochastic timed automata:

ℓ 0 ℓ 1 ℓ 2 y<1 {p 2 } ℓ 3 ℓ 4 {p 1 } e 1 ,
Example 7.18.

(1) Let A be a stochastic timed automaton such that for any ℓ ∈ L u , there exists a probability distribution µ ℓ over R + , equivalent to the Lebesgue measure, such that for every v ∈ R X + , µ (ℓ,v) = µ ℓ . If L b does not contain any cycle then A is weak reactive. (2) Let λ > 0. The modification of A unfair given on Figure 10, where µ (ℓ 4 ,v) is the exponential distribution of parameter λ, is weak reactive. The other modification of A unfair given on Figure 11, where µ (ℓ 2 ,v) is the exponential distribution of parameter λ, is not weak reactive. Discussion on Zenoness. A side-result of the proofs of Lemmas 7.13 and 7.16 is that the set of Zeno runs in a (weak) reactive stochastic timed automaton is negligible, which implies in particular that the almost-sure non-Zenoness problem is trivial.

ℓ 0 ℓ 1 ℓ 2 {p 2 } ℓ 3 ℓ 4 {p 1 } y<1 e 1 ,
Proposition 7.19. Let A be a (weak) reactive stochastic timed automaton, and s be a state of A.

Then P A (s |= Zeno) = 0.
Intuitively, this is because almost-surely, time will increase by a lower-bounded amount. The proof requires details of those of Lemmas 7.13 and 7.16, and is therefore postponed to the Appendix, on page 71.

Decidability and complexity results

We will use the thick graph construction for deciding almost-sure model-checking problem. For safety properties, we will use the characterisation given in Theorem 6.2, whereas we will use condition ( §) for more general properties, under the assumption that fairness is almost-sure.

Lemma 8.1. Let A be a timed automaton over AP, s a state of A, and P be a Büchi or Muller property over AP. Assume that G t (A) has size f (A), then we can decide in nondeterministic log(f (A))-space whether condition §(A, s, P ) holds.

Proof. The algorithm for checking condition §(A, s, P ) is the following: • guess a state q of G t (A);

• check that there is a (thick) path from [s] to q in G t (A);

• check that q belongs to a BSCC of G t (A) which satisfies property P . Note that as P is prefix-independent, we can assume the thick path from [s] to q is simple. All this can be done on-the-fly and in non-deterministic log(f (A))-space. Note that checking P in a BSCC can be done in log(f (A))-space as well.

Lemma 8.2. Let A be a timed automaton over AP, s a state of A, and P be a simple safety property over AP. Assume that G t (A) has size f (A), then we can decide in nondeterministic log(f (A))-space whether there is an infinite path π from ι(s) in G t (A) which does not satisfy P .

Proof.

Here is a possible algorithm with the expected complexity:

• guess a state q of G t (A);

• check that there is a (thick) path from [s] to q in G t (A);

• check that this finite path violates property P . Note that as P is a simple safety property, we can assume that the path between [s] and q is simple.

We now state the following lemma, whose proof follows from the definition of A ⋉ B and from the definition of (weak) reactiveness. This will imply that, under the mentioned conditions, A ⋉ B is almost-surely fair, which will allow to apply Theorem 6.9 to (weak) reactive stochastic timed automata.

Lemma 8.3. Let A be a (weak) reactive stochastic timed automaton, and B be a specification timed automaton. Then A ⋉ B is a (weak) reactive stochastic timed automaton.

We apply the results from Section 6, and obtain the following principal theorem, which states decidability and complexity results for the almost-sure model-checking. Notice that in all those cases, almost-sure model-checking coincides with large model-checking.

Theorem 8.4.

(i) The almost-sure model-checking of stochastic timed automata for simple safety properties is PSPACE-complete.

(ii) The almost-sure model-checking of single-clock stochastic timed automata for Büchi or Muller properties, or for properties given as specification (untimed) automata, is NLOGSPACE-complete.13 (iii) The almost-sure model-checking of single-clock stochastic timed automata for properties given as LTL formulas is PSPACE-complete. (iv) The almost-sure model-checking of (weak) reactive stochastic timed automata for Büchi or Muller properties or properties given as specification timed automata is PSPACE-complete.

All upper bounds are then obtained via Lemmas 8.1 and 8.2, since the size of the region automaton (and therefore the thick graph) is exponential [START_REF] Alur | A theory of timed automata[END_REF], except for single-clock timed automata, where it is only polynomial-size [START_REF] Laroussinie | Model checking timed automata with one or two clocks[END_REF]. Note that if A is a timed automaton and B a specification automaton, then the size of G t (A ⋉ B) is exponential in the two following cases: B is a specification timed automaton, and B is a specification untimed automaton of size at most exponential. The lower bounds are proven in Appendix G. Note that to establish the lower-bound in (i), the classical PSPACE-hardness proof of reachability in timed automata has to be adapted, since it is based on punctual guards that would yield negligible behaviours in the context of stochastic timed automata.

Conclusion

In this article we introduced and studied the model of stochastic timed automata that combines real-time constraints and probabilities. We considered the almost-sure modelchecking problem and designed an abstraction that can be used to prove decidability of the above, provided fairness is almost-sure in the model. We identified two main classes of automata for which this is the case, the class of single-clock timed automata and that of weak reactive timed automata. In the two cases, the proof of almost-sure fairness is non-trivial and requires intricate arguments.

A remaining open problem is the decidability status of the almost-sure model-checking problem for the general class of stochastic timed automata, already for reachability properties.

As future work, we want to extend our study to quantitative model-checking, that is, compute the probability of a given property in an automaton. This has partly been solved for single-clock automata in [START_REF] Bertrand | Quantitative modelchecking of one-clock timed automata under probabilistic semantics[END_REF], but more importantly, we would like to do it for the class of (weak) reactive stochastic timed automata, which allows for more complex timed constraints.

Compositionality is often a key for the description of real systems. Defining a composition of stochastic timed automata seems non-trivial in general, but the model of reactive stochastic timed automata seems to be well-suited for compositional design, since time can never be blocked by a component.

In this technical appendix, statements in boxes refer to statements given in the core of the paper, and whose proofs were postponed to the appendix. All other statements are local to the appendix. = τ 1 ∈I(s,e 1 ) p s+τ 1 (e 1 )

τ 2 ∈I(sτ 1 ,e 2 ) p sτ 1 +τ 2 (e 2 ) • • • τn∈I(sτ 1 •••τ n-1 ,en) p sτ 1 •••τ n-1 +τn (e n ) lim i 1 C i (τ 1 , . . . , τ n ) dµ sτ 1 •••τ n-1 (τ n ) • • • dµ s (τ 1 )
(by dominated convergence and equation (A.1)) = τ 1 ∈I(s,e 1 ) p s+τ 1 (e 1 )

τ 2 ∈I(sτ 1 ,e 2 ) p sτ 1 +τ 2 (e 2 ) • • • τn∈I(sτ 1 •••τ n-1 ,en) p sτ 1 •••τ n-1 +τn (e n ) 1 C (τ 1 , . . . , τ n ) dµ sτ 1 •••τ n-1 (τ n ) • • • dµ s (τ 1 ) = P A (A)
This shows that P A is a measure on F n (s), for all n ∈ N. It is moreover a probability measure since P A (F n (s)) = P A (π(s)) = 1. Lemma A.3. P A is a probability measure on F(s).

Proof. Obviously P A is non-negative on F(s), additive (because F n (s) ⊆ F n+1 (s) for every n ∈ N) and finite over F(s). It remains to prove that it is σ-additive. For this, we use Proposition A.1, and consider a sequence

(B n ) n of sets in F(s) such that B 0 ⊇ B 1 ⊇ B 2 ⊇ • • • and n B n = ∅. W.l.o.g.
we assume that for every n, B n ∈ F n (s). We want to prove that lim n P A (B n ) = 0. Applying a reasoning similar to that of [KSK76, Lemmas 2.1, 2.2, 2.3], it is sufficient, thanks to Lemma A.2, to do the proof when B n is some Cyl(π n ) where π n is a finite (constrained) symbolic path of length n. We write C n for the tightest constraint over variables (τ i ) i≤n corresponding to π n . We define p i the constraint from R i+1 + onto the i first components (thus in R i + ). Note that this projection is continuous (for the product topologies). In π n , if i < n, the i first variables are constrained by C i n = p i (C i+1 n ). Moreover, for every i ≤ n, we have that

C i n+1 ⊆ C i n and C i n ⊆ C i-1 n
Fix some i, the sequence (C i n ) n is nested, hence converges to C i , and C i ⊆ C i-1 . By continuity of the projection over the i first components, we have that C i = p i (C i+1 ). If none of the C i is empty, we can thus construct an element in i C i as follows: we take some τ 1 satisfying the constraint C 1 ; we have that C 1 = p 1 (C 2 ) (and C 2 is a constraint over τ 1 and τ 2 ), hence there exists τ 2 such that (τ 1 , τ 2 ) satisfies C 2 (while τ 1 still satisfies C 1 ); we do the same step-by-step for all τ i and construct a sequence (τ i ) i which satisfies all constraints C i . This sequence corresponds to a run in i Cyl(π i ). As we assumed at the beginning of the paragraph that i Cyl(π i ) = ∅, it thus means that there exists some i ∈ N such that C i = ∅.

We will use the fact that C i = n≥i C i n is empty to prove that lim n P A (π n ) = 0. We write, still with the notation that 1 α is the characteristic function of set α:

P A (Cyl(π n )) = τ 1 ∈I(s,e 1 ) p s+τ 1 (e 1 ) τ 2 ∈I(sτ 1 ,e 2 ) p sτ 1 +τ 2 (e 2 ) • • • τn∈I(sτ 1 •••τ n-1 ,en) p sτ 1 •••τ n-1 +τn (e n ) 1 Cn (τ 1 , . . . , τ n ) dµ sτ 1 •••τ n-1 (τ n ) • • • dµ s (τ 1 ) ≤ τ 1 ∈I(s,e 1 ) τ 2 ∈I(sτ 1 ,e 2 ) • • • τ i ∈I(sτ 1 •••τ i-1 ,e i ) 1 C i n (τ 1 , . . . , τ i ) dµ sτ 1 •••τ i-1 (τ i ) • • • dµ s (τ 1 )
Applying the dominated convergence theorem, we get that:

lim n P A (Cyl(π n )) = ••• ••• • • • ••• lim n 1 C i n (τ 1 , . . . , τ i ) dµ sτ 1 •••τ i-1 (τ i ) • • • dµ s (τ 1 ) = 0
This concludes the proof that P A is σ-additive on F(s), and thus the proof that P A is a probability measure on F(s).

We conclude the proof using the following classical measure extension theorem: Theorem A.4 (Carathéodory's extension theorem). Let S be a set, and ν a σ-finite measure defined on a ring R ⊆ 2 S . Then, ν can be extended in a unique manner to the σ-algebra generated by R.

We apply Theorem A.4 to the set S = Runs(A, s), R = F(s), and ν = P A which is a σ-finite measure on F(s). Hence, there is a unique extension of P A on Ω s A , the σ-algebra generated by the cylinders, which is a probability measure.

Lemma 3.4. Let

A, µ A , w A be a stochastic timed automaton, and let R(A), µ R(A) , w R(A) be the corresponding stochastic timed region automaton as defined above. Then, for every set S of runs in A we have:

S ∈ Ω s A iff ι(S) ∈ Ω ι(s) R(A)
, and in this case P A (S) = P R(A) (ι(S)).

Proof. It is sufficient to prove that the measures coincide on finite constrained paths, since it implies that they agree on cylinders and by uniqueness of the extension on any measurable set of infinite runs.

In this proof we will denote transitions of A by e i and transition in R(A) by f i . We prove that P A and P R(A) coincide on finite paths by induction on the length n of constrained symbolic paths. When n = 0, this is obvious as, for every (ℓ, ν), there is a single state ((ℓ, r), ν) in R(A) such that ν ∈ r, and in that case, ι(π((ℓ, ν))) = {π(((ℓ, r), ν))}. We assume the induction hypothesis holds for all constrained paths of length strictly smaller than n.

We will use the following notations (this will be technical, but rather simple): given s a state, we recall that s + t is the state reached from s after a delay t, [s] is the region to which s belongs. If q is a state of the region automaton, we write n q for the number of edges enabled without delay in q in R(A) (or equivalently in A). If transition e 1 can be taken from q without delay, e 1 (q) denotes the single image region reached after firing e 1 from q, and we write q |= f 1 if f 1 is the unique transition with guard checking that we are in q and corresponding to e 1 in R(A).

Let π = π C (s, e 1 , . . . , e n ) be a constrained symbolic path in A. Constraint C is on n variables τ 1 • • • τ n . We will denote C t the constraint obtained from C by replacing τ 1 by t.

P A (π) = t∈I(s,
P R(A) (π ′ Ct ) dµ A s (t) = q t∈I(s,e 1 ) s+t∈q p A s+t (e 1 )
π ′ ∈ι(π(st,e 2 ...en))

P R(A) (π ′ Ct ) dµ A s (t) = q t∈I(s,e 1 ) s+t∈q p A s+t (e 1 )
(f 2 ,...fn)∈ι(e 1 (q),e 2 ,...,en)

P R(A) (π Ct (ι(s t ), f 2 . . . f n )) dµ A s (t) = q t∈I(ι(s),f 1 ) s+t∈q q|=f 1 [s] f 1 -→e 1 (q) p R(A) ι(s)+t (f 1 )
(f 2 ,...,fn)∈ι(e 1 (q),e 2 ,...,en)

P R(A) (π Ct (ι(s) t , f 2 , . . . , f n )) dµ R(A) ι(s) (t)
by hypothesis on the measures and weights

= q|=f 1 [s] f 1 -→e 1 (q)
(f 2 ,...,fn)∈ι(e 1 (q),e 2 ,...,en)

t∈I(ι(s),f 1 ) p R(A) ι(s)+t (f 1 ) P R(A) (π Ct (ι(s) t , f 2 , . . . , f n )) dµ R(A) ι(s) (t) = q|=f 1 [s] f 1 -→e 1 (q)
(f 2 ,...,fn)∈ι(e 1 (q),e 2 ,...,en)

P R(A) (π C (ι(s), f 1 , . . . , f n )) = P R(A) (ι(π))
where (f 2 , . . . , f n ) ∈ ι(e 1 (q), e 2 , . . . , e n ) iff (f 2 , . . . , f n ) is a finite sequence of transitions corresponding to (e 2 , . . . , e n ) and which starts in (e 1 (q)) (this is a state of R(A)).

Lemma 3.5. ω-regular properties and properties given as LTL formulas are measurable. Timed properties given as specification Büchi or Muller timed automata are measurable.

Proof. It is sufficient to do the proof in the case of specifications given as deterministic timed automata. Indeed, it covers also the case of ω-regular and LTL-properties, since they can be turned into a deterministic untimed Muller automaton. Let A, µ, w be a stochastic timed automaton, and B a specification automaton (that is, a deterministic complete timed automaton). We prove that the set of runs in A that are accepted by B is measurable (for the probability measure defined by A, µ, w ). To do so, we consider the product timed automaton A ⋉ B (see definition on page 27). Let R(A ⋉ B) be its (untimed) region automaton, and F the accepting condition naturally derived from the one of B. The set of paths in R(A ⋉ B) satisfying F is a Boolean combination of

Corollary B.4. Assume π C ′ is a non-empty open set of (Runs(A, s), T s A ) and π C ⊆ π C ′ and Pol(π C ) is open in Pol(π), then π C is thick (that is, π C is a non-
empty basic open set of (Runs(A, s), T s A )). Proof. By Corollary B.3 applied to both π C and π, and π C ′ and π, we get for every 1 ≤ i ≤ n:

dim(Pol(π C i )) = dim(Pol(π C ′ i )) = dim(Pol(π i )) . As π C ′ is
a basic open set it also holds that for every 1 ≤ i ≤ n:

dim(Pol(π C ′ i )) = dim( e Pol(π C ′ i-1 (s, e 1 . . . e i-1 e)))
.

By containment of π C i-1 (s, e 1 . . . e i-1 e) into π C ′ i-1 (s, e 1 . . . e i-1 e), we get that dim( e Pol(π C ′ i-1 (s, e 1 . . . e i-1 e))) ≥ dim( e Pol(π C i-1 (s, e 1 . . . e i-1 e)))
.

This shows that π C is thick:

dim(Pol(π C i )) ≥ dim( e Pol(π C i-1 (s, e 1 . . . e i-1 e)))
.

We can now come to the proof of Lemma B.1. The fact that π C ′′ is thick is a consequence of Corollary B.4. We conclude that π C ′′ is an open set for our topology.

Proposition 4.12. For every state s of A, the topological space (Runs(A, s), T s A ) is a Baire space. Proof. To prove that (Runs(A, s), T s A ) is a Baire space, we prove that every non-empty basic open set in T s A is not meagre. Let Cyl(π C (s, e 1 . . . e n )) be a basic open set. Using Banach-Mazur games (see page 15 or [START_REF] Oxtoby | The Banach-Mazur game and Banach category theorem[END_REF]), we prove that Cyl(π C (s, e 1 . . . e n )) is not meagre by proving that Player 2 does not have a winning strategy for the Banach-Mazur game played with basic open sets and where the goal set is C = Cyl(π C (s, e 1 . . . e n )).

Player is an open set. Player 1's move will be to take B 3 = Cyl(π C 3 (s, e 1 . . . e n 1 )). By iterating this process, we define a strategy for Player 1 which satisfies:

B 1 ⊇ B 2 ⊇ Cyl(π D 1 ) ⊇ B 3 ⊇ B 4 ⊇ Cyl(π D 2 ) ⊇ . . . ⊇ B 2i-1 ⊇ B 2i ⊇ Cyl(π D i ) ⊇ • • •
where for each i, K i = Pol(π D i ) is a closed and bounded subset of Pol(π(e 1 , . . . , e n i )) ⊆ R n i + (where the n i 's form a non-decreasing sequence of N). We then have that:

∞ i=1 B i = ∞ i=1 Cyl(π D i ) .
We would like to guarantee that the above intersection is non-empty. This is not completely straightforward since the polyhedra K i = Pol(π D i ) belong to different powers of R + . We distinguish between two cases: • either the sequence (n i ) i≥1 diverges to +∞. In that case, we will embed ∞ i=1 K i into a compact set of R N + . We first define

K j = Proj {n j-1 +1,...,n j } K j and K = j≥1 K j ,
where Proj I (K J ) for

I ⊆ {1 • • • n j } is the natural projection from R n j
+ to the coordinates specified by I. Note that K j is a compact set, since it is the projection of a compact set. Each K i can naturally be embedded in K by considering the sets K ′ i defined by

K ′ i = K i × j>i K j .
The decomposition is illustrated on Figure 12. The K ′ i 's form a nested chain of closed sets of K. By Tychonoff's theorem, K is compact. Hence we can ensure that ∞ i=1 K ′ i is non-empty (Heine-Borel theorem). Take a sequence (τ j ) j≥1 in ∞ i=1 K ′ i . Each subsequence (τ j ) 1≤j≤n i straightforwardly belongs to K i . Hence, the run s

τ 1 ,e 1 ---→ s 1 τ 2 ,e 2 ---→ s 2 . . . is in ∞ i=1 B i , which completes the proof in this case. R n 1 + R n 2 + R n 2 -n 1 + K 1 K 2 K 2
Figure 12: The decomposition of the K i 's.

• either the sequence (n i ) i≥1 is upper bounded. In that case, we embed ∞ i=1 K i into a compact set of R N + where N = lim i→+∞ n i . We let the details to the reader, as they are very similar to (and easier than) the previous case. ). We need to prove that ι -1 (Cyl(π C )) is an open set of T s A . One can easily be convinced that ι -1 (Cyl(π C )) = Cyl(ι -1 (π C )). Thus proving the continuity of ι consists in proving that ι -1 (π C ) is a thick finite symbolic path whose polyhedron is open in its ambient space.

First notice that there are unique edges e 1 , . . . , e n such that ι -1 (π C ) ⊆ π(s, e 1 . . . e n ), we can then set π ′ def = ι -1 (π C ). Then obviously, Pol(π C ) = Pol(π ′ ). Let γ be the tightest constraint which defines Pol(π(ι(s), f 1 . . . f n )). We have for every i ≤ n:

® ι -1 (π C i (ι(s), f 1 . . . f i )) = π C i ∧γ i (s, e 1 . . . e i ) f ι -1 (π C i (ι(s), f 1 . . . f i-1 f )) = e π C i-1 ∧γ i-1 (s, e 1 .
. . e i-1 e) where C i and γ i are the projection of C and γ on the i first coordinates (in particular, γ i is the tightest constraint defining π(ι(s), f 1 . . . f i ) since this is in R(A)). As π C is thick, the two dimensions on the left are equal, and therefore so are the two dimensions on the right. We deduce that π ′ is thick. Now, as π(ι(s), f 1 . . . f n ) is thick (since π C is thick), we can prove by induction on its length that there is some open constraint δ such that Pol(π(ι(s), f 1 . . . f n )) = Pol(π δ (s, e 1 . . . e n )) = Pol(π(s, e 1 . . . e n )) ∩ δ Indeed:

• if δ i is an open constraint such that Pol(π δ i (s, e 1 . . . e i )) = Pol(π(ι(s), f 1 . . . f i )), we have that dim(Pol(π δ i (s, e 1 . . . e i e i+1 ))) = dim(Pol(π(ι(s), f 1 . . . f i f i+1 ))) (by thickness of π(ι(s), f 1 . . . f n ));

• furthermore this value is either equal to dim(Pol(π(ι(s), f 1 . . . f i ))) or to dim(Pol(π(ι(s), f 1 . . . f i ))) + 1; • in the first case, we set δ i+1 = δ i , whereas in the second case δ i+1 is obtained by adding to δ i the open constraint derived from the last transition f i+1 (which is then open); • we can easily check that this concludes the induction.

As

π C is thick, Pol(π C ) is open in Pol(π(ι(s), f 1 . . . f n )): there exists an open set O of R n such that Pol(π C ) = Pol(π(ι(s), f 1 . . . f n )) ∩ O.
We infer that Pol(π

′ ) = Pol(π C ) = Pol(π(s, e 1 . . . e n )) ∩ δ ∩ O,
π C ′ i (ι(s), f 1 . . . f i ) ä < dim f Pol Ä π C ′ i-1 (ι(s), f 1 . . . f i-1 , f )
′ i )) = dim(Pol(π C i )). Furthermore, f Pol Ä π C ′ i-1 (ι(s), f 1 . . . f i-1 f ) ä ⊆ e Pol Ä π C i-1 (s, e 1 . . . e i-1 e) ä
(this is a property of the region automaton). Finally, we get that dim Pol Proof. We prove both implications using characterisation of meagre sets by Banach-Mazur games and Lemma 4.17. To play this game, we choose as basis all open sets.

Assume Player 2 has a winning strategy in A to avoid P A,s . We will show that Player 2 also has a winning strategy in R(A) to avoid P R(A),ι(s) . Before starting the simulation, we recall that P R(A),ι(s) = ι( P A,s ).

The first move of Player 1 in R(A) is some open set B 1 (in T ι(s) R(A) ). That move can be transported in A: thanks to Lemma 4.17, B ′ 1 def = ι -1 (B 1 ) is a legal move of the game in A. Then, Player 2 plays according to her strategy in A with move B ′ 2 . This move cannot directly be transported to R(A) (since ι(B ′ 2 ) may not be an open set), but thanks to Lemma 4.17, there is a non-empty open set B 2 such that B 2 ⊆ ι(B ′ 2 ). We continue the simulation that way. Finally we get that

i B i ⊆ i ι(B ′ i ) = ι( i B ′ i ).
As Player 2 plays with a winning strategy in A, we get that i B ′ i ∩ P A,s = ∅, which implies that i B i ∩ P R(A),ι(s) = ∅.

On the contrary, assume that Player 2 has a winning strategy in R(A) to avoid P R(A),ι(s) . We will show that Player 2 also has a winning strategy in A to avoid P A,s . Assume that Player 1 plays π γ (s, e 1 . . . e n ), then applying Lemma 4.17, Player 2 can play as if it was π γ (ι(s), f 1 . . . f n ) in R(A) for some f 1 , . . . , f n . The game then plays as in R(A), and all moves are legal thanks to Lemma 4.17. We conclude that this strategy avoids P A,s as well, which concludes the proof.

Appendix C. Details for Section 5 Lemma 5.3. Let π(s, e 1 . . . e n ) be a symbolic path of R(A).

Assuming Pol(π(s, e 1 . . . e n )) = ∅ and letting q be the target region of π(s, e 1 . . . e n-1 ), dim(Pol(π(s, e 1 . . . e n ))) = dim(Pol(π(s, e 1 . . . e n-1 ))) + dim(I(q, e n )).

Proof. Let q be the target region of π(s, e 1 . . . e n-1 ). There are two possible cases:

• dim(I(q, e n )) = 0: for every s ′ ∈ q, there is a unique delay τ n (s ′ ) such that s ′ τn(s ′ ),en -----→. Also, for all delays τ 1 , . . . , τ n-1 such that s

τ 1 ,e 1 ---→ . . . τ n-1 ,e n-1 ------→ there is a unique s ′ ∈ q such that s τ 1 ,e 1 ---→ . . . τ n-1 ,e n-1
------→ s ′ . We can therefore define the function g with g(τ 1 , . . . , τ n-1 ) = τ n (s ′ ). We then write:

Pol(π(s, e 1 . . . e n )) = {(τ 1 , . . . , τ n ) | τ n = τ n (s ′ ) where s τ 1 ,e 1 ---→ . . . τ n-1 ,e n-1 ------→ s ′ } = {(τ 1 , . . . , τ n ) | (τ 1 , . . . , τ n-1 ) ∈ Pol(π(s, e 1 . . . e n-1 ))
and τ n = g(τ 1 , . . . , τ n-1 )} = {(τ 1 , . . . , τ n-1 , g(τ 1 , . . . , τ n-1 )) | (τ 1 , . . . , τ n-1 ) ∈ Pol(π(s, e 1 . . . e n-1 ))} Let us assume first that for all i ∈ I, π i is thin. To prove that , ¬P R(A),ι(s) is meagre we use a Banach-Mazur game and Theorem 4.3, playing with the set B of basic open sets of T ι(s) R(A) . The objective of the game is set to be ¬P R(A),ι(s) . By hypothesis, ¬P R(A),ι(s) = i∈I Cyl(π i ) and all π i are thin. As every basic open set is of the form Cyl(π) with π thick, it holds that for every B ∈ B such that B = Runs(R(A), ι(s)), we have B ∩ ¬P R(A),ι(s) = ∅. Thus, if the first move of Player 1 is Runs(R(A), ι(s)), Player 2 picks some cylinder of a finite thick path. If the first move of Player 1 is a cylinder Cyl(π), then Player 2 just chooses the same set. Then, Player 2 wins the game by mimicking at each round the choices of Player 1, i.e., whatever set B 2j-1 Player 1 chooses in the j-th round, Player 2 answers with the same choice B 2j = B 2j-1 . For such a play we clearly have

∞ i=1 B i ∩ ¬P R(A),ι(s) = ∅.
Thus Player 2 has a winning strategy and Theorem 4.3 implies that ¬P R(A),ι(s) is meagre.

Let us now prove the other implication. For a contradiction we assume that π i is thick for some i ∈ I. In particular ¬P R(A),ι(s) would contain the open set Cyl(π i ), which is not meagre because our topological space is Baire (see Proposition 4.12). Since the notion of being meagre is closed under subset, the set ¬P R(A),ι(s) would not be meagre, which is a contradiction. Proof. In this proof, we write P for P A unfair , and we first show that given 0 < t 0 < 1, P Ä π(s t 0 , (e 3 e 4 e 5 ) ω ) ä > 0 where s t 0 = (ℓ 0 , (0, t 0 )). Obviously, we have that We now would like to express P(π(s t 0 , (e 3 e 4 e 5 ) N )) as a multiple integral. In order to take the leftmost loop, we need to choose a first delay ensuring that the valuation of the clock y satisfies the guard 1 < y < 2. The location ℓ 4 is then reached with the clock valuation (2t 0 , 0). From there a second positive time delay has to be chosen in order to reach location ℓ 0 . We thus have that:

D.2. Details for the counter-example

P Ä π(s t 0 , (e 3 e 4 e 5 ) N ) ä = 1 2 -t 0 2-t 0 τ =1-t 0 1 1 -t 0 1 t 1 =t 0 P Ä π(s 1 , (e 3 e 4 e 5 ) N -1 ) ä dt 1 dτ = 1 2 -t 0 • 1 1 -t 0 1 t 1 =t 0 P Ä π(s 1 , (e 3 e 4 e 5 ) N -1 ) ä dt 1
where s 1 = (ℓ 0 , (0, t 1 )). By iterating this process, we obtain that:

P Ä π(s t 0 , (e 3 e 4 e 5 ) N ) ä = 1 2 -t 0 . 1 1 -t 0 1 t 1 =t 0 1 2 -t 1 • 1 1 -t 1 1 t 2 =t 1 . . . 1 2 -t N -1 • 1 1 -t N -1 1 t N =t N-1 dt N . . . dt 1 .
We write Proof of Theorem 6.9. We can now prove Theorem 6.9. The property P A⋉B is prefixindependent. We can therefore apply Corollary 6.7 to A ⋉ B. We can now combine with the previous technical lemmas, and we get the expected equivalence.

γ N i = 1 1 -t i-1 1 t i =t i-1 1 2 -t i • 1 1 -t i 1 t i+1 =t i . . . 1 2 -t N -1 • 1 1 -t N -1 1 t N =t N-1 dt N . . . dt i Lemma D.6. (1) If O is a non-empty open set of Runs(A ⋉ B, init A⋉B (s)), then ι -1 B (O)
(F 3 ) the set of runs with finitely many resets, and which ultimately stay forever in a bounded region, either {c i } with 0 ≤ i ≤ k, or (c i , c i+1 ) with 0 ≤ i < k. We write (F

(c i ,c i+1 ) 3 ) (resp. (F c i
3 )) for condition F 3 restricted to (c i , c i+1 ) (resp. {c i }). We write P R(A) (s, F j ) for the probability of the runs starting in s and satisfying condition F j . The three sets of runs above are measurable and partition the set of all runs. Hence j=1,2,3 P R(A) (s, F j ) = 1, and applying Bayes formula:

P R(A) (s |= fair) = j=1,2,3 P R(A) (s |= fair | F j ) • P R(A) (s, F j ) . (•)
We now distinguish between the three cases to prove that P R(A) (s |= fair | F j ) = 1 (in case P R(A) (s, F j ) = 0 we remove the corresponding term from (•)).

Case F 1 : We consider the set of runs with infinitely many resets. Let ̺ = s 0

τ 1 ,e 1 ---→ s 1 τ 2 ,e 2
---→ . . . be such a run. There exists q such that for infinitely many i with i ∈ N, s i = (q, 0) (since A is single-clock). Now, fix a state (q, 0) and assume that P R(A) (s, G F (q, 0)) > 0 (otherwise the set of runs visiting infinitely often (q, 0) will be negligible). For every sequence σ of edges and compact sets (as in the statement of Lemma 7.5), we get that

P R(A) (s, G F σ | G F (q, 0)) = 1 .
Hence, for sequences of edges (e i ) 1≤i≤p such that such a σ exists, we get that

P R(A) (s, G F (q, 0) e 1 -→ q 1 . . . ep -→ q p | G F (q, 0)) = 1 . (⋆)
Now notice that such a σ always exists whenever these edges are thick, hence (⋆) holds for every sequence of consecutive thick edges. Now, fix a thick edge e, and assume that the set of paths passing through (q, 0) infinitely often and enabling e infinitely often, has a positive probability. We will then prove that

P R(A) (s, (G F e enabled) ⇒ (G F e -→) | G F (q, 0)) = 1 , which will imply that P R(A) (s |= fair | F 1 ) = 1.
• Assume that e is reachable from (q, 0) following thick edges, say (e i ) 1≤i≤p with e p = e.

Then, applying (⋆), we get that P R(A) (s, G F (q, 0)

e 1 -→ q 1 . . . ep -→ q p | G F (q, 0)) = 1, hence that P R(A) (s, G F e -→| G F (q, 0)) = 1.
• Assume on the contrary that e is not reachable from (q, 0) following thick edges. If e is not reachable from (q, 0), then P R(A) (s, G F e enabled | G F (q, 0)) = 0. Let W be the set of finite sequences of edges (e i ) 1≤i≤p leading from (q, 0) to a state where e is enabled. Then:

P R(A) (G F e enabled | G F (q, 0)) = P R(A) (G F w∈W w | G F (q, 0)) ≤ P R(A) (F w∈W w | G F (q, 0)) = 0
because one of the edges in w is thin.

In both cases, we get the expected property. Case F 2 : We consider the set of runs with finitely many resets and which end up in the unbounded region (c k , +∞). Let ̺ = s

τ 1 ,e 1 ---→ s 1 τ 2 ,e 2
---→ . . . be such a run, and assume that from s n on, all states are in the unbounded region. From that state on, all edges which are enabled are thick and have guard x > c k . Let e be such an edge, and q be the region-state source of e: the probability P R(A) (Cyl(π(s, e))) for every s ∈ q is independent of the choice of s (as there is no restriction on delays, it is equal to w e /( e ′ enabled at q w e ′ )). Hence, ultimately, after having reached the unbounded region (and never leave it anymore), it will behave like a finite Markov chain.

Assume now that a resetting edge e is enabled infinitely often along ̺. Then, by a similar argument to the one in the proof of Lemma 7.3 with the E k , as the probability distribution of taking an edge is lower-bounded (because we are now in a finite Markov chain), then any edge will be almost surely taken infinitely often. Hence, P R(A) (s, G F resetting edge enabled | F 2 ) = 0 , and thus P R(A) (s, ¬(G F resetting edge enabled) | F 2 ) = 1 . Once more, due to the distribution over edges (which is a finite Markov chain), when there is no more resetting edges, we get

P R(A) (s |= fair | F 2 ) = 1 .
Case F 3 : We consider the set of runs with finitely many resets and which end up in a bounded region. We assume the region

r def = (c i , c i+1 ). Let ̺ = s e 1 -→ s 1 e 2
-→ . . . be a witness run, and we assume that from s n on, we are in region r. If s j 1 and s j 2 with n ≤ j 1 < j 2 correspond to the same location, then the clock value of s j 1 is less than (or equal to) that of s j 2 . Hence, if a thick edge e and whose guard is included in [c i+1 , +∞) is enabled in s j 1 (and thus also in s j 2 ), the probability of taking e from s j 2 is greater than (or equal to) the probability of taking e from s j 1 (due to (H4) in ( †) (page 28) on µ's and to the fact that the discrete probability over edges is constant by regions). Hence, there is a positive lower bound for the probability of taking e, and if e is enabled infinitely often, it will be taken infinitely often. Such an enabled edge is thus only possible with probability 0 under the assumption made in this case. Hence, with probability 1, only edges with guard x ∈ r are enabled. For these edges, as previously, the system behaves like a finite Markov chain. We thus get that

P R(A) (s |= fair | F (c i ,c i+1 ) 3 ) = 1 .
If we now assume the region r = {c i }, the reasoning is very similar to the previous one. Given a location ℓ along the suffix of the path where x = c i always holds, the edges enabled in (ℓ, x = c) are equipped with a distribution defining a finite Markov chain. Hence any edge enabled infinitely often will be taken infinitely often almost surely, which implies that

P R(A) (s |= fair | F c i
3 ) = 1 . Gathering all cases, we get the desired property, i.e., P R(A) (s |= fair) = 1. E.1. Details for Zenoness in single-clock timed automata. Lemma 7.6. Assuming A satisfies ( †), if s is a state of A, then:

P A (s |= Zeno) = B Zeno BSCC of G t (A) P R(A) (ι(s) |= F B)
where a BSCC of G t (A) is said Zeno whenever it is bounded and the clock is never reset. 62 BERTRAND, BOUYER, BRIHAYE, MENET, BAIER, GR ÖSSER, AND JURDZI ŃSKI be in F 3 (either it would end up in an unbounded region, or have infinitely many resets). Conversely, any run ending up in a Zeno BSCC is in F 3 . Hence, the mentioned equality holds.

This concludes the proof of the lemma.

Theorem 7.7. Assuming A satisfies ( †), if s is a state of A, then the three following properties are equivalent:

(a) A, s |≈ P ¬Zeno; (b) A, s |≈ T ¬Zeno; (c) no Zeno BSCC is reachable in G t (A) from ι(s).
Proof. The equivalence of (a) and (c) is a consequence of Lemma 7.6 and of Theorem 6.2:

P A (s |= Zeno) = B Zeno BSCC of G t (A) P R(A) (ι(s) |= F B). Therefore, A, s |≈ P ¬Zeno iff P A (s |= Zeno) = 0, which is then equivalent to "for every Zeno BSCC B of G t (A), P R(A) (ι(s) |= F B) = 0", which is itself equivalent to "for every Zeno BSCC B of G t (A), P R(A) (ι(s) |= G ¬B) = 1"; it
remains to realise that G ¬B is a simple safety property, and to apply Theorem 6.2.

We now show the equivalence with (b). We remove syntactically all resets from edges of R(A) labelled by x = 0 since they are useless. We also borrow the notations used in the proof of Theorem 7.2. Assume first that P A (s |= Zeno) = 0. Then no BSCC of G t (A) is Zeno. We once more play a Banach-Mazur game using the basic open sets. Player 1 plays some move B 1 , and player 2 then plays a move B 2 leading to a BSCC B of G t (A). By hypothesis, B is not a Zeno BSCC, hence either it is not bounded, or it contains resetting edges.

• We first consider the case where B contains no resetting edges. In that case, it means that the clock value when in B is always above the maximal constant. Hence, the game can keep going on, and each time Player 2 chooses a move, she first chooses a move which constrains the cylinder saying that the delay has to be larger than 1. This is always possible, due to the form of the constraints, which all include (c k , +∞). In that case, it is not difficult to check that the resulting runs are all non-Zeno. • We now consider the case where B has resetting edges. Note that the clock can then become larger than 0. In that case, Player 2 can always choose a move so that it terminates with a resetting edge, but has visited a positive region, and has enforced that the value of the clock in that precise region was larger than 1/2. In that case also, all runs resulting from that play are non-Zeno. Hence, we get that Player 2 has a strategy to avoid the set of Zeno runs, hence this set is meagre.

Conversely assume that the set of Zeno runs is meagre, but assume also that P A (s |= Zeno) > 0. Once more, let's play the Banach-Mazur game. Player 2 has a strategy to avoid Zeno behaviours. However, as P A (s |= Zeno) > 0, Player 1 can play a first move leading to a Zeno BSCC B of G t (A). Then B has no resetting edges and lies within an interval (c i ; c i+1 ) or {c i }. Then whatever move Player 2 chooses, the resulting runs will all be Zeno, hence contradicting the assumption that the set of Zeno runs is meagre. The claim follows. (s). Hence, we have D >M k (s) ⊂ q∈Q K q k (s) and

P Ñ n∈N k≥n Ñ q∈Q K q k (s) éé = 1 .
As Q is a finite set, we deduce

P Ñ q∈Q Ñ n∈N k≥n K q k (s) éé = 1
and as n∈N k≥n K q k (s) = R q (s), we get

P Ñ q∈Q R q (s) é = 1 .
Now we give the proof of Lemma 7.14. It will require quite long developments that we give in details.

Lemma 7.14. Assuming the above notations, for all q ∈ Q ′ P (R e (s) | R q (s)) = 1.

Proof. Let q ∈ Q ′ . We want prove that P (R e (s) | R q (s)) = 1 or equivalently that P (R e (s) ∩ R q (s) | R q (s)) = 1. We notice that the event R e (s) ∩ R q (s) coincides with n∈N k≥n R q,e k (s)

where R q,e k (s) is the set of runs starting in s along which an occurrence of edge e is preceded by precisely k visits to q, i.e. R q,e k (s) = {̺ ∈ Runs(A, s) | ̺ = s τ 1 ,e 1 ---→ s 1 . . .

τm,em

----→ s m . . . and there exists j s.t. e j = e and #{1 ≤ i < j | loc(s i ) = q} = k}, where loc(s i ) is the location of state s i . We recall the following lemma, which is well-known in probability theory (see for example [START_REF] Billingsley | Probability and measure[END_REF]): Lemma F.1 (Borel-Cantelli). Assume (E, P) is a probabilistic space, and that the measurable events (E k ) k∈N are independent. If With the aim to apply this lemma, we will prove that the events R q,e k (s) are independent in the R q (s)-conditional σ-algebra, and that k∈N P(R q,e k (s) | R q (s)) = +∞, which will imply Lemma 7.14. This is non-trivial and will require several technical lemmas that we present now. The following arguments rely on result that will be given as Corollary F.7 (which is technical, and therefore postponed). Independence of events.

Lemma F.2. The events R q,e k (s) are conditionally independent given R q (s). Proof. Defining R q ≥n (s) as the set of runs starting in s and visiting q at least n times, we compute: P R q,e k (s) | R q (s) = P Ñ R q,e k (s) | R q,e k (s) ∩ R q ≥n (s)

ä é P Ñ n>k R q ≥n (s) é .
The two sequences Ä R q,e k (s) ∩ R q ≥n (s) where I x is an interval of the form [c; c] for some integer 0 ≤ c ≤ M , or (c; c + 1) for some integer 0 ≤ c < M , or (M ; +∞). We have that:

P(π(s ′ , e 1 . . . e n )) = t∈I(s ′ ,e 1 ) p s ′ +t (e 1 ) P(π(s ′ e 1 t , e 2 . . . e n )) dµ ℓ (t)

where s ′ t,e 1 --→ s ′ e 1 t . Now, it is not difficult to check that p s ′ +t (e 1 ) = p s ′′ +t (e 1 ) and I(s ′ , e 1 ) = I(s ′′ , e 1 ) by hypothesis on s ′ and s ′′ . Also, writing s ′′ t,e 1 --→ s ′′ e 1 t , we easily get that if v ′ e 1 t and v ′′ e 1 t are the valuations of s ′ e 1 t and s ′′ e 1 t then for every x ∈ X, we have v ′ e 1 t (x) = v ′′ e 1 t (x) or min(v ′ e 1 t (x), v ′′ e 1 t (x)) > M . We deduce by induction hypothesis: P(π(s ′ e 1 t , e 2 . . . e n )) = P(π(s ′′ e 1 t , e 2 . . . e n )). Hence, we have P(π(s ′ , e 1 . . . e n )) = t∈I(s ′′ ,e 1 ) p s ′′ +t (e 1 ) P(π(s ′′ e 1 t , e 2 . . . e n )) dµ ℓ (t) = P(π(s ′′ , e 1 . . . e n )).

This concludes the proof.

We define E q (s) the set of runs starting in s and visiting q at least once.

Proposition F.5. Let q ∈ Q ′ . The following equalities hold true:

(1) For every n ≥ 1, P Ä R q ≥n (s) ä = P (E q (s)) • P Ä R q ≥1 (s q ) ä n-1 .

(2) For every 1 ≤ k < n, P Ä R q,e k (s) ∩ R q ≥n (s) ä = P (E q (s)) • P Ä R q ≥1 (s q ) ä n-2 • P Ä R q ≥1 (s q ) ∩ R q,e 0 (s q ) ä .

(3) For every 1 ≤ k < k ′ < n, P Ä R q,e k (s) ∩ R q,e k ′ (s) ∩ R q ≥n (s) ä = P (E q (s))

• P Ä R q ≥1 (s q ) ä n-3 • P Ä R q ≥1 (s q ) ∩ R q,e 0 (s q ) ä 2 .

Proof. We will only prove the first equality. The other equalities can be handled, using decompositions, similarly to the first equality. We define the set ε q (s) as: target(e h ) = q, and target(e i ) = q for any i < h} .

Note that a run ̺ is in E q (s) iff there is some (e 1 , . . . , e h ) ∈ ε q (s) with ̺ ∈ Cyl (π(s, e 1 . . . e h )).

The set ε q (s) is a basic set for E q (s ′ ). For every state s ′ , we define the set γ q n (s ′ ) as: Note that a run ̺ is in R q ≥n (s ′ ) iff there is some (e 1 , . . . , e h ) ∈ γ q n (s ′ ) such that ̺ ∈ Cyl (π(s ′ , e 1 . . . e h )). The set γ q n (s ′ ) is a basic set for R q ≥n (s ′ ). Note also that if s ′ and s ′′ are region-equivalent, then the two sets γ q n (s ′ ) and γ q n (s ′′ ) coincide. We will thus write γ q n (q), where q is the region-state of s ′ and s ′′ . We will decompose runs in R q ≥n (s) using the basic sets ε q (s) and γ q n (s q ). Indeed, if ̺ ∈ R q ≥n (s), then we can decompose ̺ into ̺ ′ • ̺ ′′ such that there exist (e 1 , . . . , e h ) ∈ ε q (s) with ̺ ′ ∈ π(s, e 1 . . . e h ), and (f 1 , . . . , f k ) ∈ γ q n-1 (last(̺ ′ )) with ̺ ′′ ∈ Cyl (π(last(̺ ′ ), f 1 , . . . , f k )). By definition of ε q (s), last(̺ ′ ) ∈ q, and by applying Lemma F.4, we get P π(last(̺ ′ ), f 1 . . . f k ) = P (π(s q , f 1 , . . . , f k )) .

If we denote ε q (s) instead of (e 1 ,...,e h )∈ε q (s) and γ q n-1 (q) instead of (f 1 ,...,f k )∈γ q n-1 (q) , we have the following simplification:

P Ä R q ≥n (s) ä = ε q (s) γ q n-1 (q) P ̺ = ̺ ′ • ̺ ′′ | ̺ ′ ∈ π(s, e 1 . . . e h ),
̺ ′′ ∈ Cyl π(last(̺ ′ ), f 1 . . . f k ) = ε q (s) γ q n-1 (q) t 1 t 2 . . . ---→) ∈ q) = ε q (s) γ q n-1 (q) t 1 t 2 . . .

t h h-1 i=0
p s i +t i+1 (e i+1 )

• P (π(s q , f 1 . . . f k )) dµ s h-1 (t h ) . . . dµ s (t 1 ) = Ö γ q n-1 (q) P (π(s q , f 1 . . . f k ))

è • Ñ ε q (s) t 1 t 2 . . . t h h-1 i=0
p s i +t i+1 (e i+1 ) dµ s h-1 (t h ) . . . dµ s 0 (t 1 ) é = P Ä R q ≥n-1 (s q ) ä • P (E q (s)) .

By induction on n, using a similar decomposition, we can prove that:

P Ä R q ≥n (s q ) ä = P Ä R q ≥1 (s q )
ä n which concludes the proof for the first equality.

We can simplify equalities of the previous proposition thanks to following lemma:

Lemma F.6. Let q ∈ Q ′ . We have P(R q ≥1 (s q )) = 1.

Hardness in reactive timed automata. We prove that the almost-sure model-checking problem in reactive timed automata against simple safety and simple reachability properties is PSPACE-hard. To that aim we simulate a linearly-bounded Turing machine M on an input word w 0 . The general reduction is rather standard [START_REF] Aceto | Is your model-checker on time? On the complexity of model-checking for timed modal logics[END_REF] but it is required to work out the details so that there is no equality constraints in the constructed timed automaton, so that R(A) and G t (A) coincide.

Let N be the bound on the tape of M when simulating on input word w 0 . We assume the alphabet is {a, b} and we encode the content of j-th cell C j using a clock x j with the following convention: when we enter a module, cell C j contains an a whenever x j < 1 and it contains a b whenever x j > 2. To simulate a transition q ′ = δ(q, α, β, dir) where α, β ∈ {a, b}, we construct a module as in Fig. 13 for every index i such that 1 ≤ i ≤ N and 1 ≤ dir(i) ≤ N , where dir(i) is either i + 1 (if the head goes to the left), or i -1 (if the head goes to the right). q,i ... ... q ′ ,dir(i) u:=0 2<u<3

x 1 <4,u<3

x 1 :=0

x 1 >4,u<3

x 2 <4,u<3

x 2 :=0

x 2 >4,u<3 g α,i ,Y β,i

x N <4,u<3

x N :=0

x N >4,u<3

Figure 13: Simulation of M-transition q ′ = δ(q, α, β, dir) where α, β ∈ {a, b}. Index i is such that 1 ≤ i ≤ N and 1 ≤ dir(i) ≤ N . Guard g a,i is x i < 4, u < 3 and guard g b,i is x i > 4, u < 3. Set Y a,i is {x i } and set Y b,i is ∅.

We complete the construction with an initialisation module (with input w 0 on the tape), and we complete the automaton so that it is reactive (by adding transitions to sink location). We note A for this timed automaton and write halt for the halting location (which can be made a sink). Let P safety be the safety property that halt is not visited, and P reach be the property of reaching sink. We attach the exponential distribution with parameter, say 1, to every state, and assume weight 1 for every edge. Let s 0 be the initial state of A where all clocks are set to 0.

Lemma G.1. The following equivalences hold: M does not halt on input w 0 ⇔ P A (s 0 |= P safety ) = 1 ⇔ P A (s 0 |= P reach ) = 1

Proof. Assume M halts on input w 0 . Then there is a finite run ̺ in A leading to halt. Due to the special form of A, the probability of the cylinder generated by π ̺ is positive (A has only strict guards). This implies that P A (s 0 |= P reach ) < 1 (since state sink is not reached by that cylinder), and P A (s 0 |= P safety ) < 1.

If M does not halt on input w 0 , then location halt is never visited, and therefore sink is visited with probability 1. This implies that P A (s 0 |= P reach ) = 1, and that P A (s 0 |= P safety ) = 1. This shows hardness results for (i) and (iv).

Hardness in single-clock timed automata. The NLOGSPACE-hardness result of (ii) already holds for finite Markov chains (since checking reachability properties in finite graphs is NLOGSPACE-hard).

Similarly, the result of (iii) concerning PSPACE-hardness already holds for finite Markov chains [START_REF] Vardi | Automatic verification of probabilistic concurrent finite-state programs[END_REF].

This work is licensed under the Creative Commons Attribution-NoDerivs License. To view a copy of this license, visit http://creativecommons.org/licenses/by-nd/2.0/ or send a letter to Creative Commons, 171 Second St, Suite 300, San Francisco, CA 94105, USA, or Eisenacher Strasse 2, 10777 Berlin, Germany

Figure 1 :

 1 Figure 1: Modelling the IPv4 Zeroconf using stochastic timed automata.

Figure 2 :

 2 Figure 2: An automaton and its timed region automaton.

Figure 3 :

 3 Figure 3: The stochastic timed automaton A running .

  Remark 4.5. Surprisingly, in general, there is no relation between meagre and open sets. Indeed non meagre open sets obviously exist, but one can identify topological spaces where open sets are meagre. Let us consider the set of rational numbers Q with its natural topology (whose basic open sets are the open intervals). In this topology all sets, and in particular all open sets, are countable and thus meagre.

Figure 4 :

 4 Figure 4: Thick and thin symbolic paths on an example.

Figure 5 :

 5 Figure 5: A subtle example illustrating thickness and thinness.

  e 3 , x=1 e 4 , x≥3, x:=0 e 5 , x≤2 e 6 , x=0 e 1 , x≤1 e 7 , x≤1

4. 3 .

 3 A topology on infinite runs. The goal of this subsection is to define a topology on the set of infinite runs of a given timed automaton. Keeping our analogy with R n , where the open sets are among the sets of maximal dimension, we use the notion of thickness introduced in the latter subsection in order to define a topology on runs. More precisely, the basic open sets will be cylinders over thick constrained symbolic paths whose associated polyhedra are open in their ambient spaces. Definition 4.11. Let s be a state of A. Let T s A be the topology over the set of runs of A starting in s defined with the following basic open sets: 8 either the set Runs(A, s), or the empty set ∅, or the cylinders Cyl(π C ) where π C = π C (s, e 1 e 2 . . . e n ) is a finite constrained symbolic path of A such that: (i) π C is thick, (ii) C is Borel-measurable, and (iii) Pol(π C ) is open in Pol(π) for the classical topology on R n , where π = π(s, e 1 e 2 . . . e n ). Before illustrating our definition, let us draw the reader's attention on the two following points. First notice that Definition 4.11 only makes sense if the intersection of two basic open sets is still a basic open set; This is proven in the Appendix as Lemma B.1 (page 45).

Lemma 4. 14 .

 14 In the topological space (Runs(A, s), T s A ), a finite symbolic path π defines a basic open set if and only if there exist an open constraint C of R n and thick edges e 1 , . . . , e n such that π = π C (s, e 1 . . . e n ). 4.4. Large satisfaction. We are now in a position where we can define a notion of large satisfaction.

  e 3 , x=1 e 4 , x≥3, x:=0 e 5 , x≤2 e 6 , x=0 e 1 , x≤1 e 7 , x≤1 Indeed, in Example 4.13, we proved that the set C def = {π(s 0 , e 1 i e 2 (e 4 e 5 ) ω ) | i ∈ N} is large. Moreover each run of C satisfies ϕ def = F (p 1 ∧G (p 1 ⇒ F p 2 )), and thus A running , s 0 |≈ T ϕ, since largeness is closed under subsumption. Note that the previous formula is not satisfied with the classical LTL semantics. 'Staying in ℓ 0 forever ', 'reaching ℓ 3 ', etc are examples of behaviours in A running that violate the LTL formula ϕ.

Figure 6 :Figure 7 :

 67 Figure 6: Construction of the thick graph on the running example.

  (a) A, s |≈ P P ; (b) A, s |≈ T P ; (c) every infinite thick symbolic path π from ι(s) in R(A) satisfies P ; (d) every infinite path π from ι(s) in G t (A) satisfies P ; (e) MC(A), ι(s) |≈ P .

  s) is meagre. We now apply the characterisation of meagre sets via Banach-Mazur games (Theorem 4.3), where the players play with basic open sets of (Runs(R(A), ι(s)), T ι(s) R(A) ). Note that for every basic open set π C (s, e 1 . . . e n ) in the above topology, all edges e 1 , . . . , e n are thick, the open set can therefore "be read" in G t (A).

Figure 9 :

 9 Figure 9: A two-clock automaton, A unfair with non negligible set of unfair runs.

Figure 10 :

 10 Figure 10: Automaton A 1 unfair .

Figure 11 :

 11 Figure 11: Automaton A 2 unfair .

of Lemma B. 1 .

 1 Let us denote in this proof C ′′ = C ∩ C ′ , and π the unconstrained symbolic path π(s, e 1 , . . . , e n ). Write πC ′′ for π C ∩ π C ′ = π C ′′ (s, e 1 , . . . , e n ). If π C ′′is empty, we are done since the empty set is an open set. We therefore assume that π C ′′ is non-empty. We first show that Pol(π C ∩ π C ′ ) is open in Pol(π), which is the second condition for π C ∩ π C ′ to be an open set. We have that Pol(π C ′′ ) = Pol(π C ) ∩ Pol(π C ′ ). By assumption both Pol(π C ) and Pol(π C ′ ) are open in Pol(π), hence their intersection too.

Lemma 4. 14 .

 14 In the topological space (Runs(A, s), T s A ), a finite symbolic path π defines a basic open set if and only if there exist an open constraint C of R n and thick edges e 1 , . . . , e n such that π = π C (s, e 1 . . . e n ). Proof. First notice that if C is an open constraint of R n , then C is Borel-measurable, and Pol(π C (s, e 1 . . . e n )) = Pol(π(s, e 1 . . . e n )) ∩ C is open in Pol(π(s, e 1 . . . e n )). Furthermore, applying Corollary B.4, π C (s, e 1 . . . e n ) is thick if π(s, e 1 . . . e n ) is thick as well. Now, assume that π = π C (s, e 1 . . . e n ) is a basic open set. This means in particular that Pol(π) is open in Pol(π(s, e 1 . . . e n )): there exists an open set δ of R n such that Pol(π) = Pol(π(s, e 1 . . . e n )) ∩ δ. As it is open, δ is Borel-measurable, and we get that Pol(π) = Pol(π δ (s, e 1 . . . e n )), and therefore π = π δ (s, e 1 . . . e n ), which is the expected result. Lemma 4.17. Let ι : Runs(A, s) → Runs(R(A), ι(s)) be the projection of runs in A onto the region automaton R(A). Then ι is continuous, and for every non-empty open set O ∈ T s A , • ῑ(O) = ∅. Proof. We first prove that ι is continuous. Let π C = π C (ι(s), f 1 . . . f n ) be a symbolic path in R(A) such that Cyl(π C ) is a basic open set of (Runs(ι(s), R(A)), T ι(s) R(A)

ä

  where C ′ i corresponds to the projection on the i first coordinates of the tightest constraint defining π ′ C . Moreover, asPol(π ′ C ) ⊆ Pol Ä π C ä and dim(Pol(π ′ C )) = dim(Pol(π C )), applying Lemma B.2, we get that for all i's, dim(Pol(π ′ C

π

  C i-1 (s, e 1 . . . e i-1 e) ä which contradicts the hypothesis that π is thick. We deduce that Cyl(π ′ ) is a basic open set of (Runs(R(A), ι(s)), T ι(s) R(A) ), hence the result.Proposition 4.19. Let s be a state of A, and P be a timed property over AP. Then, A, s |≈ T P ⇔ R(A), ι(s) |≈ T P .

  A unfair of Figure 9. Proposition D.1. P A unfair Ä π(s 0 , (e 3 e 4 e 5 ) ω ) ä > 0, where s 0 = (ℓ 0 , (0, 0)).

  t 0 , (e 3 e 4 e 5 ) ω ) t 0 , (e 3 e 4 e 5 ) N ) ä where we write P Ä π(s t 0 , (e 3 e 4 e 5 ) N ) ä for P Ä Cyl(π(s t 0 , (e 3 e 4 e 5 ) N )) ä .

.

  ℓ ∈ S N -1 , we haveP Ä D ≤M n,N (s) | D ≤M n,N -1 (s) ∩ K ℓ N -1 (s) (s) | D ≤M n,N -1 (s) ∩ K ℓ N -1 (s) (s) | D ≤M n,N -1 (s) ∩ K ℓ N -1 (s)As for any ℓ ∈ L, we have assumed µ ℓ ([0, M ]) < 1, we conclude thatP Ä D ≤M n,N (s) ä ≤ (max ℓ∈L µ ℓ ([0, M ])) N +1-n -→ N →∞ 0 64BERTRAND, BOUYER, BRIHAYE, MENET, BAIER, GR ÖSSER, AND JURDZI ŃSKI just a matter of noticing that if ̺ = st 1 ,a 1 ---→ s 1 • • • tn,an ---→ s n • • • is in D >M n (s), then s n is of the form (ℓ n , v n ) with (ℓ n , [v n ] A ) ∈ Q (a clockis either reset on the n-transition (hence its value is 0), or it is above M ) and thus ̺ ∈ K (ℓn,[vn] A ) n

  , . . . , e h ) ∈ E h | source(e 1 ) = [s] A ,

  , . . . , e h ) ∈ E h | source(e 1 ) = [s ′ ] A , target(e h ) = q, and #{1 ≤ i ≤ h | target(e i ) = q} = n © .

  e 1 ) p A s+t (e 1 ) P A (π Ct (s t , e 2 . . . e n )) dµ A

			s (t)
	=	t∈I(s,e 1 )	p A s+t (e 1 ) P R(A) (ι(π Ct (s t , e 2 . . . e n ))) dµ A s (t) by induction hypothesis
	=		p A s+t (e 1 )
		t∈I(s,e 1 )	π ′ ∈ι(π(st,e 2 ...en))

  1 starts by choosing a set B 1 = Cyl(π C (s, e 1 . . . e n )). Then Player 2 picks some basic open set B 2 = Cyl(π C 2 (s, e 1 . . . e n . . . e n 1 )) such that B 1 ⊇ B 2 . Let us now explain how Player 1 can build her move in order to avoid to reach the empty set. Since B 2 is an open set, we have that (i) π C 2 is thick and (ii) Pol(π C 2 (s, e 1 . . . e n 1 )) is open in Pol(π(s, e 1 . . . e n 1 )) ⊆ R n 1 + . The topology on Pol(π(s, e 1 . . . e n 1 )) is induced from a distance, hence there exists a closed, bounded and convex set denoted K 1 such that K1 = ∅ and K 1 ⊆ Pol(π C 2 (s, e 1 . . . e n 1 )). Let D 1 be the constraint associated with K 1 ; clearly cylinder Cyl(π D 1 (s, e 1 . . . e n 1 )) is included in B 2 . Let O be an open set included in K 1 and C 3 be the constraint associated with O. It is Borel-measurable since it is open. Applying Corollary B.4, we know that π C 3 (s, e 1 . . . e n 1 ) is thick. Hence clearly enough, Cyl(π C 3 (s, e 1 . . . e n 1 ))

  and δ ∩ O is open in R n : Pol(π ′ ) is open in Pol(π(s, e 1 . . . e n )).This concludes the proof: Cyl(π ′ ) is a basic open set in (Runs(A, s), T s A ). , that is, there is a thick symbolic path π ′ whose polyhedron is open in its ambient space and such that Cyl(π ′ ) ⊆ ι(Cyl(π C )).Letπ C = π C (s, e 1 . . . e n ) be a constrained symbolic path such that Cyl(π C ) is a basic open set of (Runs(s, A), T s A ). We have that ι(π C ) = f 1 ,...,fn π C (ι(s), f 1 . . . f n )where the (finite) union is taken over all sequences of edges f 1 , . . . , f n corresponding to e 1 , . . . , e n . There exist thus edges f 1 , . . . , f n such that ′ C = π C (ι(s), f 1 . . . f n ). We will prove that π ′ C is an open set. Note that as Pol(π C ) is open in Pol(π(s, e 1 . . . e n )), we can assume w.l.o.g. that C defines an open set of R n . Hence π ′ C is open in π(ι(s), f 1 . . . f n ). Assume that it is thin. Then, there exists some i such that dim Pol

	•
	We now prove that for every non-empty open set O ∈ T s A , to prove that for each basic open set Cyl(π C ) of T s A , ι(Cyl(π C )) contains a basic open set ῑ(O) = ∅. Again it is sufficient ι(s) Cyl(π ′ ) of T R(A) dim(Pol(π C )) = dim Pol Ä π C (ι(s), f 1 . . . f n )
	Ä

ä and we write π

  If O is a non-empty open set of Runs(A, s), then ι B (O) has a non-empty interior.Proof. We show the first property. Let π be a basic open set of Runs(A ⋉ B, init A⋉B (s)). Following the notations of Section 6.3 and applying Lemma 4.14, we can write the basic open set π as π C (init A⋉B (s), e 1 e 1 . . . e n e n ), where C is an open constraint of R n . Note that as B is complete, none of the transitions e i have equality constraints (otherwise π would not be an open set). Also notice that all e i 's are also thick (for the same reason). Let γ be the constraint of R n generated by the transitions e 1 , . . . , e n . Due to the previous remark, the interior of γ is non-empty. Also, as C ∧ γ is non-empty, this implies that C ∧ γ has a non-empty interior. Now, we should just notice that ι -1 B (π) = π C∧γ (s, e 1 . . . e n ), which contains an open set, since C ∧ γ has a non-empty interior, and all the e i 's are thick. Fix now a non-empty open set O in Runs(A, s), and pick π = π C (s, e 1 . . . e n ) a basic open set included in O. The image of π by ι B can be decomposed as the following finite union over all sequences of edges in B of length n: ι B (π) = (e 1 ,...,e n ) Pol(π |≤i )) for every i, where we consider here the projections over the i first components. In particular, we can easily prove now that π C (init A⋉B (s), e 1 e 1 . . . e n e n ) is a basic open set in Runs(A ⋉ B, init A⋉B (s)).

	has a non-empty
	interior.
	(2)

π C (init A⋉B (s), e 1 e 1 . . . e n e n ) Also note that we don't lose any behaviour, in the sense that Pol(π) = Pol Ñ (e 1 ,...,e n ) π C (init A⋉B (s), e 1 e 1 . . . e n e n ) é = (e 1 ,...,e n ) Pol Ä π C (init A⋉B (s), e 1 e 1 . . . e n e n ) ä In particular, there is some (e 1 , . . . , e n ) such that dim(Pol Ä π C i (init A⋉B (s), e 1 e 1 . . . e i e i ) ä ) = dim(

In the core of the article, MC(A) is the so-called thick graph Gt(A), that we interpret as a finite Markov chain, putting the uniform distributions over edges.

Roughly, a run is fair if any edge which is enabled infinitely often is taken infinitely often.

⌊•⌋ (resp. {•}) denotes the integral (resp. fractional) part.

Note that this is possible, as we assume A is non-blocking, hence I(s) = ∅ for every state s of A.

Two measures ν and ν ′ are equivalent whenever for each measurable set A, ν(A) = 0 ⇔ ν ′ (A) = 0.

In modern definitions, a topological space is a Baire space if each countable union of closed sets with an empty interior has an empty interior. However, the two definitions coincide, see[START_REF] Munkres | Topology[END_REF] p.295].

We recall that open sets of T s A are then built from those basic open sets using union.

This is for the next conditional probability to be defined.

Note that simple safety or simple reachability properties can be expressed as small specification untimed automata, which yield an NLOGSPACE upper bound in those cases as well.

We use here the following general topology result: if X is a convex set and O an open set in R n such that X ∩ O = ∅, then dim(X) = dim(X ∩ O).

Recall that edges labelled with x = 0 are not labelled with a reset.

Acknowledgement

Nathalie Bertrand and Patricia Bouyer were partly supported by ANR project ImpRo (number ANR-10-BLAN-0317). Patricia Bouyer was furthermore supported by the ERC Starting grant EQualIS (number 308087). Thomas Brihaye was partly supported by the ARC project (number AUWB-2010-10/15-UMONS-3), a grant "Mission Scientifique" from the F.R.S.-FNRS, the FRFC project (number 2.4545.11), and the EU-FP7 project CASST-ING (number 601148). Quentin Menet was supported by a grant of FRIA. Christel Baier was partly supported by the German Research Council (DFG) through the collaborative research centre 912 Highly-Adaptive Energy-Efficient Computing (HAEC) and the cluster of excellence Centre for Advancing Electronics Dresden (cfAED), the EU-FP7 project MEALS (295261) and by the EU and the State Saxony through the ESF young researcher groups IMData (100098198) and SREX (100111037).

Condition (c) in Theorem 7.7 can be checked in NLOGSPACE (recall that in that case G t (A) is polynomial in the size of A).

7.2. Reactive and weak-reactive timed automata. Although fairness is not almostsure in general for n-clock stochastic timed automata with n ≥ 2 (see Figure 9), it is the case for the subclass of reactive (and weak-reactive) stochastic timed automata. Let us first recall that a (non-stochastic) timed automaton A is reactive if I(s) = R + for all states s of A.

We first focus on the class of reactive stochastic timed automata, and later extend the results to the class of weak-reactive stochastic timed automata. Definition 7.9. A stochastic timed automaton A, µ, w is reactive whenever the timed automaton A = (L, X, E, I, L) is reactive, and for every ℓ ∈ L, there exists a probability distribution µ ℓ over R + , equivalent to the Lebesgue measure, such that for every v ∈ R X + , µ (ℓ,v) = µ ℓ .

Note that for any constant C, for any ℓ ∈ L, µ ℓ ([0, C]) < 1, this is due to the equivalence of µ ℓ with the Lebesgue measure. Note also that if s = (ℓ, v) and s ′ = (ℓ, v ′ ) are such that v ∼ = A v ′ , then p s (e) = p s ′ (e) for every edge e.

Example 7.10. Examples of distributions over delays that respect the above conditions are exponential distributions, but we can think of many other kinds of distributions. Later, all our examples will use exponential distributions. Each such distribution is characterised by a positive parameter λ ℓ , and its density is t → λ ℓ • e -λ ℓ •t . Note that reactive stochastic timed automata generalise continuous-time Markov chains (CTMC for short). A CTMC is nothing else than a single-clock reactive stochastic timed automaton in which (i) on all transitions, the guard is trivial, and the clock is reset, and (ii) each location is assigned an exponential distribution over delays.

Let A, µ, w be a reactive stochastic timed automaton. The goal of this section is to prove the following result, which will allow to apply results of Section 6, and in particular Theorem 6.9. Proposition 7.11. Let s be a state of A. Then P A (s |= fair) = 1.

We first recall some basic probability results.

Lemma 7.12. Let P be a probability measure on some probabilistic space Ω. Let A, B and C be measurable sets such that P(B) > 0 and P(C) > 0, then (1) If P(A) = 1, then P(A | B) = 1. Appendix A. Details for Section 3 Proposition 3.2. For every state s of A, P A is a probability measure over (Runs(A, s), Ω s A ). Proof. We first recall a basic property in measure theory [START_REF] Kemeny | Denumerable Markov Chains[END_REF].

Proposition A.1. Let ν be a non-negative additive set function defined on some set space F such that for every A ∈ F, ν(A) < ∞. The three following properties are equivalent:

(1) ν is σ-additive, (2) for every sequence

For every n ∈ N, we write F n (s) for the ring 14 generated by the set of (basic) cylinders from s of length n, i.e., all Cyl(π C (s, e 1 . . . e n )). The elements of F n (s) are thus finite unions of basic cylinders of length n. We then define

Lemma A.2. For every n, P A is a probability measure on F n (s).

Proof. First, by induction on n, it is not difficult to prove that for every n ∈ N, (e 1 ,...,en)

We fix n ∈ N. P A is obviously additive, non-negative and finite over F n (s). Take a sequence

There are finitely many distinct sequences of edges of length n. Hence, intersecting each of the A i 's with each of the symbolic paths π(s, e 1 . . . e n ) of length n, we can assume w.l.o.g. that each A i is a single constrained finite symbolic path.

Let e 1 . . . e n be the sequence of edges underlying all constrained symbolic paths A i , and write C i for the tightest constraint defining A i (i.e., A i = π C i (s, e 1 . . . e n )). We have that C i ⊆ C i+1 , and (C i ) i converges to C, which corresponds to the constraint associated with A. We can write, if 1 α is the characteristic function of set α, that:

p s+τ 1 (e 1 ) cylinders Cyl(s 0 , e 1 . . . e n ). Indeed, since F is an ω-regular condition and seeing R(A ⋉ B) as a finite Markov chain (with arbitrary probabilities), this is a consequence of the proof of measurability of ω-regular properties [START_REF] Vardi | Automatic verification of probabilistic concurrent finite-state programs[END_REF]. For a fixed finite path s 0 , e 1 . . . e n in R(A⋉B), we write

Roughly speaking, H(s 0 , e 1 . . . e n ) is the set of all runs in A whose natural projection in R(A⋉B) belongs to Cyl(π(s 0 , e 1 . . . e n )). One can be convinced that H(s 0 , e 1 . . . e n ) consists of a finite union of cylinders generated by constrained symbolic paths in A.

Proof. Assume there exists an index i ≤ n such that dim(Pol(π

there must be an index j, such that Pol(π C ) gains some dimension in the j-th direction, whereas Pol(π C ′ ) does not. But this is not possible since

From this basic result, we get the following corollaries. 15 Applying Lemma B.2 to π C and π yields the expected result.

The second equality holds because π(s, e 1 . . . e n ) is a symbolic path in the region automaton R(A). We deduce that dim(Pol(π(s, e 1 . . . e n ))) = dim(Pol(π(s, e 1 . . . e n-1 ))), which is the expected value.

• dim(I(s ′ , e n )) = 1 for every s ′ ∈ q: there is non-punctual open interval (µ n (s ′ ), ν n (s ′ ))

such that s ′ τn,en ---→ iff τ n ∈ (µ n (s ′ ), ν n (s ′ )). We can then rewrite Pol(π(s, e 1 , . . . , e n )) as follows:

and τ n ∈ g(τ 1 , . . . , τ n-1 )} where g(τ 1 , . . . , τ n-1 ) defines an open interval. We then get dim(Pol(π(s, e 1 . . . e n ))) = dim(Pol(π(s, e 1 . . . e n-1 ))) + 1.

Proposition 5.4. Let π = π(s, e 1 . . . e n ) be a symbolic path in R(A). Then, π is thin in R(A) iff there exists 1 ≤ i ≤ n such that e i is thin.

Proof. The proof is done by induction on the length n of π.

The case n = 0 is obvious since π(s) is thick and π(s) surely contains no thin edge. Assume n > 0 and the result holds for any 0 ≤ j ≤ n -1, and let π = π(s, e 1 . . . e n ) be a symbolic path of length n. For every 1 ≤ j ≤ n, write π ≤j for π(s, e 1 . . . e j ).

• Let us first assume that π is thin in R(A). In case there exists j < n such that π ≤j is thin, then we are done by applying the induction hypothesis to π ≤j . We therefore assume that π ≤j is thick for every j < n. Let k = dim(Pol(π ≤n-1 )). Applying Lemma 5.3, dim(Pol(π)) ∈ {k, k + 1}, and if dim(Pol(π)) = k + 1, then π would be thick (k + 1 is the maximal dimension of any possible Pol(π(s, e 1 . . . e n-1 e))). We thus get that dim(Pol(π)) = k, and there exists e such that dim(Pol(π(s, e 1 . . . e n-1 e))) = k + 1 (this witnesses the fact that π is thin). By Lemma 5.3, we therefore infer that dim(I(q, e n )) = 0 whereas dim(I(q, e)) = 1 where q is the target region of π(s, e 1 . . . e n-1 ): edge e n is thin, which concludes the left-to-right implication. • Assume now that π is thick. By definition of thickness, for every j ≤ n, π ≤j is thick.

By induction hypothesis, all edges e 1 , . . . , e n-1 are then thick. Assume towards a contradiction that e n is thin. Let q be the source-region of e n , there exists an edge e such that for every s ′ ∈ q, dim(I(s ′ , e n )) < dim(I(s ′ , e)). Now we know that for every s ′ with s

whereas dim(Pol(π(s, e 1 . . . e n-1 e))) = dim(Pol(π(s, e 1 . . . e n-1 ))) + dim(I(q, e)).

We deduce that π is thin, contradicting the assumption. This concludes the proof of the right-to-left implication.

Proof. We assume that the probability distributions in R(A) are those used in Lemma 3.4, and we write µ for the distributions over delays.

We first prove that P R(A) (Cyl(π)) > 0 implies that π is thick. Towards a contradiction, assume that π is thin. Following Proposition 5.4, there exists 1 ≤ i ≤ n such that e i is thin. Let q be the target set of π(s, e 1 . . . e i-1 ): dim(I(q, e i )) < dim(I(q)). By hypothesis on the measures µ (condition (⋆), cf page 11), for every s ′ ∈ q, µ s ′ (I(s ′ , e i )) = 0. Hence, for every

Assume now that π is thick. For every 1 ≤ i ≤ n, we write q i for the target region of π(s, e 1 . . . e i ). Following Proposition 5.4, for every 1 ≤ i ≤ n, e i is thick, which means that dim(I(q i , e i+1 )) = dim(I(q i )). As in the first implication, by assumption (⋆) on the measure µ, for every s i ∈ q i , µ s i (I(s i , e i+1 )) > 0. We then use the definition of the probability inductively on suffixes of π starting in some s i to obtain a sequence of integral computation over non negligible set of a positive function, hence P R(A) (Cyl(π)) > 0. Theorem 6.2. Let s be a state of A, and P be a(n untimed) safety property over AP. Then the four following properties are equivalent: (a) A, s |≈ P P ; (b) A, s |≈ T P ; (c) every infinite thick symbolic path π from ι(s) in R(A) satisfies P ; (d) every infinite path π from ι(s) in G t (A) satisfies P ; (e) MC(A), ι(s) |≈ P .

Proof. Equivalence between (c) and (d) is by construction of G t (A).

Thanks to Lemmas 3.4 and 4.19, to prove the equivalence between (a) and (b), it is equivalent (and hence sufficient) to prove that R(A), ι(s) |≈ T P iff R(A), ι(s) |≈ P P . Since P is a property over AP, for every infinite symbolic path π = π(s, e 1 . . . e i . . .), either all realisations ̺ ∈ π satisfy P , or none of them satisfies P . Now, using the fact that P is a safety property, we can write ¬P R(A),ι(s) as a denumerable union of cylinders:

where π i is a finite (unconstrained) symbolic path from ι(s), and I is a denumerable set. Thus, R(A), ι(s) |≈ P P is equivalent to P R(A) ( i∈I Cyl(π i )) = 0. Since I is denumerable, we obtain R(A), ι(s) |≈ P P iff for all i ∈ I, P R(A) (Cyl(π i )) = 0. By Proposition 6.1, we have that R(A), ι(s) |≈ P P iff for all i ∈ I, π i is thin (this by-the-way proves equivalence between (a) and (c)). Thus proving the theorem amounts to proving that ¬P R(A),ι(s) is meagre iff for all i ∈ I, π i is thin. and we can prove by a descending induction on i (see Lemma D.2 below) that γ N i ≥ t i-1 . Thus, we deduce that

It remains to show that P Ä π(s 0 , (e 3 e 4 e 5 ) ω ) ä > 0, i.e. that the above result extends to the case t 0 = 0. Roughly speaking, after one loop, we will have t 1 > 0, hence we can use the above inequality from the second loop on by writing:

This concludes the proof.

Proof. The base case is when i = N . In that case,

which proves the desired property.

We assume we have proved the property for i + 1, and want to prove it for i.

Now, when 0 ≤ x ≤ 1, we know that log(1 + x) ≥ x -x 2 2 (see Lemma D.3). Applying this inequality to x = 1t i-1 , we get the following inequality:

This concludes the inductive case.

2 . Since f ′ (x) = 1 1+x and g ′ (x) = 1x, we remark that for any 0 ≤ x ≤ 1, we have f ′ (x) ≥ g ′ (x). Indeed, for any x ≥ 0, 1 1+x ≥ 1x if and only if 1 ≥ 1x 2 . Since f (0) = 0 = g(0), the result follows. D.3. Extension to specification timed automata. In this part, we aim at proving Theorem 6.9 below. Theorem 6.9. Let s be a state of A, and B be a specification Büchi or Muller timed automaton. Assuming P A⋉B (init A⋉B (s) |= fair) = 1, the following holds:

The proof of this theorem will require several lemmas that we present below. Before that, we define ι B the application (bijection) which assigns to every run ̺ in A its unique image ̺ B in A ⋉ B.

Lemma D.4. Let s be a state of A, and B be a specification Büchi or Muller timed automaton. Assume measures and weights in A ⋉ B are properly set. Then:

Proof. This lemma is a consequence of the two following properties:

(1) for every measurable set E of Runs(A, s),

The second item is a direct consequence of the definition of P A⋉B . The proof for the first item is similar to that for region automata, that is, to the proof of Lemma 3.4. We therefore skip it.

A similar result holds for the topological semantics: Lemma D.5. Let A be a timed automaton, let s be a state of A, and let B be a specification Büchi or Muller timed automaton. Then, for every set S ⊆ Runs(A, s):

Proof. The proof of this lemma is similar to that of Proposition 4.19, even though projection ι B might not be continuous. The next lemma (Lemma D.6) is sufficient to make the simulation between the two Banach-Mazur games (as in the proof of Proposition 4.19), and to prove the expected result.

Appendix E. Details for single-clock timed automata Lemma 7.3.

(1) For every subregion (q, J) of q such that (i) J is non-empty and open in q (for the induced topology), and (ii) J ⊆ q is compact, (2) for every thick edge e enabled in q, (3) for every subregion (q ′ , J ′ ) of q ′ such that for every s ∈ (q, J), e(s) ∩ J ′ is non-empty and open in q ′ (for the induced topology), where e(s)

a This is for the next conditional probability to be defined.

Proof. We write P A (s e -→ (q ′ , J ′ )) for the probability of the set of runs starting from s with a move s τ,e --→ s ′ with s ′ ∈ (q ′ , J ′ ) and for some τ ∈ R + . 16 Let λ def = inf s∈(q,J) P A (s e -→ (q ′ , J ′ )). Since J ⊆ q is compact and ∀s ∈ q, P A (s e -→ (q ′ , J ′ )) > 0 (because e is thick and e(s) ∩ J ′ is non-empty and open), λ > 0. Indeed we have supposed that for all ℓ ∈ L, for all [a, b] ⊆ R + , the function v → µ (ℓ,v) ([a, b]) is continuous, see hypothesis (H3) in ( †) (page 28), hence s → P A (s e -→ (q ′ , J ′ )) is continuous. Denote E k the set of paths in A that visit (q, J) infinitely often, but from the k-th passage in (q, J) on never fire (q, J) e -→ (q ′ , J ′ ) anymore. Note that the set E k is P Ameasurable, and that P A (E k ) ≤ ∞ k (1λ) = 0. Then note that the set k≥1 E k can be equivalently defined by B ∧ ¬A where B is 'G F (q, J)' and A is 'G F (q, J) e -→ (q ′ , J ′ )'. Hence, we get that P A (s, B ∧ ¬A) ≤ lim k→+∞ P A (E k ) = 0, and thus

Proof. Let s be a state in A. We want to prove that P A (s |= fair) = 1. We will equivalently prove P R(A) (ι(s) |= fair) = 1. To that purpose, we decompose the set of infinite runs in R(A) from ι(s) into: (F 1 ) the set of runs with infinitely many resets, (F 2 ) the set of runs with finitely many resets, and which are ultimately in the unbounded region (c k , +∞), 16 Note that this set is PA-measurable because it can be seen as Cyl(πC J ′ (s, e)) for some constraint C J ′ enforcing the first move to lead to J ′ .

Proof. From Lemma 3.4 (resp. Lemma 4.19), we know that (a) (resp. (b)) is equivalent to R(A), ι(s) |≈ P ¬Zeno (resp. R(A), ι(s) |≈ T ¬Zeno).

We first remove syntactically all resets from edges of R(A) labelled by x = 0 since they are useless. We borrow the notations used in the proof of Theorem 7.2, and following that proof, we decompose the set of infinite runs from s into: (F 1 ) the set of runs with infinitely many resets, (F 2 ) the set of runs with finitely many resets, and which are ultimately in the unbounded region (c k , +∞), (F 3 ) the set of runs with finitely many resets, and which ultimately stay forever in a bounded region, either {c i } with 0 ≤ i ≤ k, or (c i , c i+1 ) with 0 ≤ i < k. We then also have:

when these conditional probabilities are well-defined (otherwise it is correct to remove the term from the sum). The proof of Lemma 7.6 is then decomposed into two parts, first we prove that the two first terms of the above sum are always equal to 0, and then that we can decide whether the last term is equal to 0.

Proof. We distinguish two cases. Case F 1 : We consider the set of runs with infinitely many resets. This set can be decomposed according to the states (q, 0) (where q ∈ Q is a region) that are visited infinitely often. We show that P A (ι(s) |= Zeno | G F (q, 0)) = 0. In order to prove this, we distinguish the four following subcases depending on the set I((q, 0)): either (i) I((q, 0)) ∩ [0, 1) = ∅, or (ii) (0, 1) ⊆ I((q, 0)), or (iii) {0} I((q, 0)), or (iv) {0} = I((q, 0)).

Let us first treat the easy case (i). If I((q, 0)) ∩ [0, 1) = ∅, since the timed automaton is non-blocking, this means that each time the automaton arrives in state (q, 0) at least 1 time unit elapses before the next transition. Hence a run visiting infinitely often such state (q, 0) is necessarily non-Zeno.

Let us now consider case (ii), i.e., we assume that (0, 1) ⊆ I((q, 0)). Since the probability distribution over the delays is then equivalent to the Lebesgue measure (see hypothesis (⋆)), the probability of waiting a time delay τ ≤ 1 2 in (q, 0) is positive and strictly smaller than 1 (we write λ (q,0) for this value: 0 < λ (q,0) < 1). Let E k be the set of runs starting from ι(s), visiting (q, 0) infinitely often, and such that from the k-th passage on, the time elapsed from state (q, 0) (before taking an action) is less than 1 2 . We have P R(A) (E k ) ≤ ∞ k λ (q,0) = 0, and as a consequence

In case (iii), we assume that {0} I((q, 0)). If (0, 1) ⊆ I((q, 0)), we are done by case (ii). We can thus suppose that if 0 = τ ∈ I((q, 0)), we have that τ ≥ 1. If I((q, 0)) reduces to a finite union of points, the probability λ 0 of waiting a delay greater than or equal to 1 is positive and strictly smaller than 1 (because the measure is then equivalent to the uniform measure over those points, see hypothesis (⋆)). When going infinitely often through (q, 0), we will thus wait infinitely often a time greater than or equal to 1. If I((q, 0)) contains an open interval, the probability of waiting a delay greater or equal than 1 from (q, 0) is 1 (by hypothesis (⋆)). From this we can easily derive that:

Let us conclude with case (iv) where I((q, 0)) = {0}. Since no positive delay can elapse from (q, 0), the probability of taking any edge enabled in (q, 0) is positive (the distribution over edges indeed becomes uniform). Hence, any state (q e , 0) reachable from (q, 0) taking edge e, is almost surely infinitely often visited (as soon as (q, 0) is). From (q e , 0), again two situations are possible: either I((q e , 0)) = {0} or not. In the first case, note that it is necessarily the case that such a chain (q, 0)

is finite, otherwise the run would contain only finitely many resets 17 . Thus we surely reach infinitely often a state (q ′ , 0) such that I((q ′ , 0)) = {0} allowing us to rely on the previous cases to obtain the desired results.

Gathering the four cases, we conclude that P A (ι(s) |= Zeno | G F (q, 0)) = 0. Hence

Case F 2 : We consider the set of runs with finitely many resets and which end up in the unbounded region. From any state in the unbounded region, the set of potential delays is necessarily of the form [0, +∞) 18 . From hypothesis (H5) in ( †) on the distributions over delays, the probability of waiting a time delay τ ≤ 1 2 from s, denoted λ s , can be bounded by a constant: 0 < λ s ≤ λ 0 < 1. Let E k denote the set of executions which, at the k-th step, are in the unbounded region without leaving it afterwards, and such that all delays afterwards are less than 1 2 . The probability of being Zeno when in E k satisfies: P(E k ) ≤ i>k λ 0 = 0, from which we derive:

This concludes the proof of the Lemma 7.6.

The case of condition F 3 is not similar to the two previous cases. Indeed, it is worth noticing that every execution satisfying the condition

is bounded and contains no resetting edges. Note that in a Zeno BSCC the value of the clock lies in a unique interval (c, c + 1)

Proof. Runs in R(A) are almost surely fair (thanks to Theorem 7.2), hence P R(A) (ι(s) |= F 3 ) = P R(A) (ι(s) |= F 3 ∧ fair). Now, a fair run in R(A) actually ends up in a BSCC of G t (A). It is now sufficient to remark that fair runs in F 3 end up in a BSCC that is bounded and does not reset the clock. Indeed, if one of these condition does not hold, the run would not Appendix F. Details for Subsection 7.2 (reactive timed automata)

Let s be a state of R(A), that we will take as initial. If e is a thick edge in T , and q ∈ Q, we write R e (s) for the set of runs in R(A) that start in s and take e infinitely often, and R q (s) for the set of runs of R(A) that start in s and visit q infinitely often. In particular, we write R source(e) (s) for the set of runs that start in s and visit source(e) infinitely often (hence along which e is enabled infinitely often).

We fix a thick edge e in T , and we let Q be the set of pairs q = (ℓ, r) where r is memoryless and Q ′ the set of elements q = (ℓ, r) ∈ Q such that P(R q (s)) > 0 and P(R q,e 0 (s q )) > 0 where R q,e 0 (s q ) is the set of runs that start from s q and take e before any other visit to q. Lemma 7.13. Assuming the above notations,

Proof. We let D >M n (s) be the set of runs from s that delay more than M time units before taking the n-th transition (i.e.

If we denote D ≤M n,N (s) := n≤k≤N (D >M k (s)) c (where A c is the complement of any set A) and S N the set of locations l ∈ L such that P Ä Thus, by Corollary F.7,

P (E q (s)) • P (R q,e 0 (s q )) lim m→∞ P (E q (s)) = P (R q,e 0 (s q )) where E q (s) is the set of runs starting in s and visiting q at least once, and s q is the canonical configuration (ℓ, v r ) for q = (ℓ, r).

Similarly we prove, using Corollary F.7, that for k = k ′ : P R q,e k (s) ∩ R q,e k ′ (s) | R q (s) = P (R q,e 0 (s q )) 2 = P R q,e k (s) | R q (s) • P R q,e k ′ (s) | R q (s) . We conclude that the two events R q,e k (s) and R q,e k ′ (s) are conditionally independent given R q (s).

Divergence of the series.

Proof. As in the previous lemma, we can deduce from equalities of Corollary F.7 that P R q,e k (s) | R q (s) = P (R q,e 0 (s q )) . However, as q ∈ Q ′ , we know by definition that we have P(R q,e 0 (s q )) > 0. The result follows.

Decomposition using basic sets. This section aims to prove Corollary F.7 and so to complete the previous proofs.

Lemma F.4. Let r be a memoryless region, v ∈ r, and s ′ = (ℓ, v) a configuration of A. Writing q for region-state (ℓ, r), we have for every sequence (e 1 , . . . , e n ) ∈ E n , P(π(s ′ , e 1 . . . e n )) = P(π(s q , e 1 . . . e n )).

Proof. We will prove a stronger result. We show that for every pair s ′ = (ℓ, v), s ′′ = (ℓ, v ′ ) satisfying for every x ∈ X, v(x) = v ′ (x) or min(v(x), v ′ (x)) > M , we have for every sequence (e 1 , . . . , e n ) ∈ E n , P(π(s ′ , e 1 . . . e n )) = P(π(s ′′ , e 1 . . . e n )) . We prove this result by induction on the length n of the sequence of edges. The result trivially holds for n = 0. Assume that n > 0, and that the lemma holds for sequences of edges of length n -1. The constraint labelling the edge e 1 is equivalent to some

Proof. For a contradiction, we assume that P(R q ≥1 (s q )) = α 0 < 1. By Proposition F.5, we thus have that:

As an immediate corollary we get the following result.

Corollary F.7. Let q ∈ Q ′ . The following equalities hold true:

(1) For every n ≥ 1,

(2) For every 1 ≤ k < n,

This concludes the proof of Lemma 7.14.

We now extend the previous study to weak reactive stochastic timed automata.

Lemma 7.16. Let A be a weak reactive stochastic timed automaton and s be a state of A. Then

Proof. We seek to show that, with probability 1, we delay infinitely many times more than M time units before taking a transition. Let D >M n (s) be the set of runs from state s that delays more than M time units before taking the n-th transition (i.e.

Since A is a weak reactive stochastic timed automaton, there exists 0 < λ 0 ≤ 1 such that for every ℓ ∈ L u , for every v |= I(ℓ), we have

and there exist 0 < λ 1 ≤ 1 and N ≥ 1 such that for any ℓ ∈ L b , any v |= I(ℓ), we have where ≥ λ 0 λ 1 .

We deduce that for every state s, P(D ≤M 1,N (s)) ≤ 1λ 0 λ 1 . Therefore for any state s, for any k ≥ 2, we get p s (k-1)N-1 +t (k-1)N (e (k-1)N )P(D ≤M 1,N (s (k-1)N )) dµ s (k-1)N-1 (t (k-1)N ) . . . dµ (ℓ,v) (t 1 ) ≤ (1λ 0 λ 1 )P(D ≤M 1,(k-1)N (s)) ≤ (1λ 0 λ 1 ) k .

In the same way, we deduce that for any j, k ≥ 1, P(D ≤M j,j+kN (s)) ≤ (1λ 0 λ 1 ) k . We conclude that for any k ≥ 1, P(D ≤M k,n (s)) converges to 0 when n tends to infinity and we finish the proof with the same arguments as in the proof of Lemma 7.13. Proposition 7.19. Let A be a (weak) reactive stochastic timed automaton, and s be a state of A. Then P A (s |= Zeno) = 0.

Proof. This is a consequence of the proofs of Lemma 7.13 (for reactive automata) and of Lemma 7.16 (for weak reactive automata).

We should just notice that, writing Zeno(s) for the set of Zeno runs from s,

And in the two proofs that are mentioned, it is proven that P(D ≤M k,n (s)) tends to 0 when n tends to ∞, which implies that P(Zeno(s)) = 0. a Note that simple safety or simple reachability properties can be expressed as small specification untimed automata, which yield an NLOGSPACE upper bound in those cases as well.

The upper bounds have already been explained in the core of the paper (they are obvious consequences of the previous developments). We will now explain several lower bounds.