Abstract :

This paper aims to present the influence of several constructive options on the vibro-acoustic behavior of a wooden lightweight structure. The experiemental protocol, which was optimised and described in an preceeding paper [START_REF] Blon | Experimental Investigations on the Structural-Acoustic Behaviour of a Lightweight Wooden Building : Case of a Plasterboard Wall Addition[END_REF], allows us to quantify the influence of these constructive options in terms of acoustic level and isolation, eigenfrequencies and vibration mode shapes of the different parts of the structure. The results of this work are coherent and confirmed that the experimental test protocol is functional and repeatable.

Introduction

The complexity and the huge diversity of wooden construction assemblies makes difficult the prediction of lightweight buildings vibro-acoustic properties. As a matter of fact, the acoustical behaviour of these structures can only be measured after building completion. The V project has been launched in 2011 to answer this problematic. It is coordinated by the innovative technology transfer center of the CRITT B (. . .pinal, France), in partnership with the LAUM (Acoustic Laboratory of the Maine University, le Mans, France) and several major industrial actors of the wooden construction sector in France. The project also benefit from a French governmental agency (ADEME) grant.

A preceeding paper [START_REF] Blon | Experimental Investigations on the Structural-Acoustic Behaviour of a Lightweight Wooden Building : Case of a Plasterboard Wall Addition[END_REF] has presented the optimisation of the experimental procedure :

-linearity of the response according to the level of excitation, -definition of the frequency band for which the measurment are efficient, -speed of the frequency shift in the shirp excitation, -optimisation of the accelerometers positions to conserve a high information level, -opening-closing of the cavities, -position of the operator on the excited floor, -noise level, -the use of an aluminium frame (in contact with the floor) or a joist (with no floor contact) to suspend the shaker, -repetability of the measurements in time. The tested mockup is presented on figures 1 et 2. As described by [START_REF] Jarnerö | In situ testing of timber floor vibration properties[END_REF] and [START_REF] Jarnerö | Effect of flexible supports on vibration performance of timber floors[END_REF], the excitation is realised by a suspended shaker figure 3, and a microphone and accelerometers are used in the cavities.

In a second section this paper gives an exhaustive review of the influence on isolation and vibration level of the floor joists orientation, the adding of plasterboard, the density of screws to claim the plasterboards, the disconnecting of the plasterboard to the walls, the loading of the structure by static load and the removing of cladding.

Materials and influence of constructive options 2.1 Floor type

Three types of floors are tested : two SOCOPA's joist floors (with long or short joists) (Fig. 1,5) and a wood-concrete floor from SATOB (Fig. 4,5).

The frequency response function measured on the microphone has a lower level with the wood-concrete floor compared to the joist-floor due to its higher mass and stiffness (Fig. 6 up). Accelerometers placed on the roof show the same behavior (Fig. 6 down). Three resonances at 18, 25 and 30 Hz are nevertheless detected and their associated accelerometer experimental mode shapes are also plotted (Fig. 7). Similar analysis for the joist-floors have been performed and the first resonance frequencies are near 25, 30 and 45 Hz for the floor with long joists and near 25, 40 and 52 Hz for the floor with short joists. Moreover, a higher maximum of the FRF near the first acoustic mode at 50 Hz appears for the short-joist floor which reveal a strong coupling with the cavity, the coupling with the second cavity mode near 70 Hz appears whathever the joists orientation, and the amplitude of vibration of the wall which separates the two rooms is greater for the short-joists room than for the long joist one certainly due to a direct coupling between the joists and the considered wall.

Plasterboard walls

The influence of four plasterboard layer configurations are tested :

-one layer of plasterboard, -doubling of the screw density to connect the plasterboard to the battens, -one layer of plasterboard disconnected from the wood structure, -two layers of plasterboard disconnected from the wood structure, The dimensions of the acoustic volumes are reduced when plasterboard layers are clamped to the walls, and the theoretical resonance frequencies consequently shift from 66 to 75 Hz. The figure 8 shows that the vibration intensity is less important with plasterboard and the microphone FRF confirms the increase of the frequency resonance. The doubling of the screw density to clamp the plasterboard layers to the battens or the use of two plasterboard layers has experimentaly no significant effect on the room acoustics nor the vibration amplitude (Tab. 1). On the other hand when the plasterboard layers are disconnected from the structure, a small increase of the isolation between the two cavities is measured (Tab. 1). 1 -Acoustic isolation between the two rooms (dB) for the reference case, and deviation from this reference for each configuration.

Static loading of the structure

The mock up has only one level. In order to simulate a day-to-day loading on the structure, four containers of 300 liters filled with water are installed on the floor. The equivalent loading is 65 kg/m 2 . An increase of 1 dB of the acoustic isolation is measured in the cavities.

The cladding

Measurements without cladding are also performed before the dismantling of the mock up. No significant changes on isolation nor vibration level are observed.

Review of acoustic isolation in the frequency range [20 Hz-200 Hz]

The table 1 compares each configuration to a reference configuration : bare walls without cleats with the small holes bewteen the mock up and the floor filled with glazer putty. When plasterboard layers are added, the rather small increase of the isolation is due to the multiplication by 5 of the reverberation time which has a contrary effect to those of the added mass.

Conclusion

The results of this work are coherent and confirmed that the experimental test protocol is functional and repeatable. The experimental data will be compared to a numerical model of the mock up currently in development in ordrer to validate it.

  a , A. TRIBALEAU b , B. BROUARD b , O. DAZEL b , J.-M. GENEVAUX b a. CRITT Bois + david.blon@cribois.net b. Laboratoire d'Acoustique de l'Université du Maine, UMR CNRS 6613

F 1 -F 2 -

 12 Experimental mock up of VIBRACOUBOIS project : floors are not drawn. Full scale experimental mock up of VIBRACOUBOIS project.

F 3 -

 3 Elastic suspension of the shaker to a wooden beam.F 4 -SATOB's wood-concrete floor installed on the mock up. F 5 -Cut of SOCOPA floor (on the left side) and cut of SATOB floor (on the right side).

F

  functions : microphone (orange), accelerometers (purple) in each cavities. Dashed lines corresponds to the analytical resonance frequencies of the uncoupled cavities.

F

  fonctions of the SATOB floor, and mode shapes at 3 resonance frequencies. The green cross represents the position of the shaker on the floor.

F

  microphone FRFs measured with and without one simple plasterboard layer clamped on cleats.

T


Patricia Bouyer Lsv

Thomas Brihaye

Mickael Randour

Cédric Rivière

Pierre Vandenhove

Decisiveness of Stochastic Systems and its Application to Hybrid Models *

In [3], Abdulla et al. introduced the concept of decisiveness, an interesting tool for lifting good properties of finite Markov chains to denumerable ones. Later [10], this concept was extended to more general stochastic transition systems (STSs), allowing the design of various verification algorithms for large classes of (infinite) STSs. We further improve the understanding and utility of decisiveness in two ways.

.

Introduction

Hybrid and stochastic models. Various kinds of mathematical models have been proposed to represent real-life systems. In this article, we focus on models combining hybrid and stochastic aspects. We outline the main features of these models to motivate our approach.

The idea of hybrid systems originates from the urge to study systems subject to both discrete and continuous phenomena, such as digital computer systems interacting with analog data. These systems are transition systems with two kinds of transitions: continuous transitions, where some continuous variables evolve over time (e.g., according to a differential equation), and discrete transitions, where the system changes modes and variables can be reset. Much of the research about hybrid systems focuses on non-deterministic hybrid systems, i.e., systems modeling uncertainty by considering all possible behaviors (e.g., different possibilities for discrete transitions at a given time, arbitrary long time between discrete transitions). A typical question concerns the safety of such systems-if a system can reach an undesirable state, it is said to be unsafe; if not, it is safe-such a specification is called qualitative. However, this is limiting for two reasons. First, it does not take into account that some behaviors are more likely to occur than others. Second, risks cannot necessarily be avoided, and it is unrealistic to prevent undesirable outcomes altogether. Therefore, we want to make probabilities an integral part of our models, in order to be able to quantify the probability that they behave according to the specification. We thus consider the class of stochastic hybrid systems (SHSs, for short), hybrid systems in which a stochastic semantics replaces non-determinism. Goals. Our interest lies in the formal analysis of continuous-time SHSs, and more specifically in reachability questions, i.e., concerning the likelihood that some set of states is reached. The questions we seek to answer are both of the qualitative kind (is some region of the state space almost surely reached, i.e., reached with probability 1?) and of the quantitative kind (what is the probability that some states are eventually reached?). Such questions are crucial, as verifying that a system works safely often reduces to verifying that some undesirable state of the system is never reached (or with a low probability), or that some desirable state is to be reached with high probability [START_REF] Baier | Principles of model checking[END_REF]. We want to give algorithms that decide, for an SHS H and reachability property P, whether P is satisfied in H . Such an endeavor faces multiple challenges; a first obvious one being that even for rather restricted classes of non-deterministic hybrid systems, reachability problems are undecidable [START_REF] Henzinger | What's Decidable about Hybrid Automata?[END_REF][START_REF] Henzinger | Robust Undecidability of Timed and Hybrid Systems[END_REF]. We want to define and consider a class of SHSs for which some reachability problems are decidable.

Methods and contributions. Our methodology consists of two main steps. In a first step, we follow the approach of Bertrand et al. [START_REF] Bertrand | When are stochastic transition systems tameable?[END_REF]: we study general stochastic transition systems (STSs) through the decisiveness concept (Section 2). The class of STSs is a very versatile class of systems encompassing many well-known families of stochastic systems, such as Markov chains, generalized semi-Markov processes, stochastic timed automata, stochastic Petri nets, and stochastic hybrid systems. Decisiveness was introduced in [START_REF] Parosh | Decisive Markov Chains[END_REF] to study Markov chains, and extended to STSs in [START_REF] Bertrand | When are stochastic transition systems tameable?[END_REF]. An STS is said to be decisive with respect to a set of states B if executions of the system almost surely reach B or a state from which B is unreachable. Decisive STSs benefit from useful properties that make possible the design of verification algorithms related to reachability properties. Our first contribution is to provide a criterion to check the decisiveness of STSs (Proposition 2.8), which generalizes the decisiveness criteria from [START_REF] Parosh | Decisive Markov Chains[END_REF][START_REF] Bertrand | When are stochastic transition systems tameable?[END_REF]. This generalization was mentioned as an open problem in [START_REF] Bertrand | When are stochastic transition systems tameable?[END_REF].

In a second step, we focus on stochastic hybrid systems, which we introduce in Section 3.1. Reachability problems in hybrid systems are notoriously undecidable [START_REF] Henzinger | What's Decidable about Hybrid Automata?[END_REF][START_REF] Henzinger | Robust Undecidability of Timed and Hybrid Systems[END_REF]. Our contributions regarding SHSs are split into two parts.

First, we aim to use the decisiveness idea to get closer to the decidability frontier. Albeit desirable, the decisiveness of a class of SHSs is not sufficient to handle algorithmic questions about each SHS, as we need an effective way to apprehend their uncountable state space. In this regard, an often-used technique is to consider a finite abstraction of the system, that is, a finite partition of the state space that preserves the properties to be verified (a well-known example is the region graph for timed automata [START_REF] Alur | A Theory of Timed Automata[END_REF]). To find such an abstraction of SHSs, we borrow ideas from [START_REF] Brihaye | On O-Minimal Hybrid Systems[END_REF][START_REF] Lafferriere | O-Minimal Hybrid Systems[END_REF]: we consider SHSs with strong resets (Section 3.2), a syntactic condition that decouples their continuous behavior from their discrete behavior. We show that SHSs with adequately placed strong resets (at least one per cycle of their discrete graph) (i) have a finite abstraction (Proposition 3.11), and (ii) are decisive (Proposition 3.9), which can be proved using our new criterion.

Second, in Section 3.3, we show, with strong resets, how to effectively compute a finite abstraction and use it to perform a reachability analysis of the original system. We proceed by assuming that the components of our systems are definable in an o-minimal structure. The main difficulty here is that "a satisfactory theory of measure and integration seems to be lacking in the o-minimal context" [START_REF] Berarducci | An additive measure in o-minimal expansions of fields[END_REF]; in an o-minimal structure, the primitive function of a definable function is in general not definable, which complicates definability questions regarding probabilities. We therefore restrict the possible probability distributions, using properties of o-minimal structures to keep our class as large as possible. When the theory of the structure is decidable (as is the case for the ordered field of real numbers [START_REF] Tarski | A decision method for elementary algebra and geometry[END_REF]), the reachability problems are then decidable. This provides a stochastic extension to the theory of ominimal hybrid systems [START_REF] Lafferriere | O-Minimal Hybrid Systems[END_REF]. We study qualitative and quantitative problems. Due to space constraints, all the missing proofs and some technical details and additional results are omitted from this version and can be found in the full article [START_REF] Bouyer | Decisiveness of Stochastic Systems and its Application to Hybrid Models[END_REF].

Related work.

Our results combine previous work on stochastic systems and hybrid systems. About stochastic systems, we build on the work of [START_REF] Parosh | Decisive Markov Chains[END_REF][START_REF] Bertrand | When are stochastic transition systems tameable?[END_REF]. Our work also takes inspiration from research about stochastic timed automata, a subclass of stochastic hybrid systems which already combines stochastic and timed aspects; model checking of stochastic timed automata has been studied in [START_REF] Baier | Almost-Sure Model Checking of Infinite Paths in One-Clock Timed Automata[END_REF][START_REF] Bertrand | Quantitative Model-Checking of One-Clock Timed Automata under Probabilistic Semantics[END_REF][START_REF] Bertrand | Stochastic Timed Automata[END_REF] and considered in the context of the decisiveness property in [START_REF] Carlier | Verification of Stochastic Timed Automata[END_REF]. Fundamental results about the decidability of the reachability problem for hybrid systems can be found in [START_REF] Alur | A Theory of Timed Automata[END_REF][START_REF] Henzinger | What's Decidable about Hybrid Automata?[END_REF][START_REF] Henzinger | Robust Undecidability of Timed and Hybrid Systems[END_REF]. The class of o-minimal hybrid systems, of which we introduce a stochastic extension, has been studied in [START_REF] Brihaye | On O-Minimal Hybrid Systems[END_REF][START_REF] Gentilini | Reachability Problems on Extended O-Minimal Hybrid Automata[END_REF][START_REF] Lafferriere | O-Minimal Hybrid Systems[END_REF].

The literature about SHSs often follows a more practical or numerical approach. A first introduction to the model was provided in [START_REF] Hu | Towards a Theory of Stochastic Hybrid Systems[END_REF]. An extensive review of the underlying theory and of many applications of SHSs is provided in books [START_REF] Cassandras | Stochastic Hybrid Systems[END_REF][START_REF] Luminita | Stochastic reachability analysis of hybrid systems[END_REF], and a review of different possible semantics for this model is provided in [START_REF] Lygeros | Stochastic Hybrid Systems: A Powerful Framework for Complex, Large Scale Applications[END_REF]. Applications of SHSs are numerous: a few examples are air traffic management [START_REF] Prandini | Application of Reachability Analysis for Stochastic Hybrid Systems to Aircraft Conflict Prediction[END_REF][START_REF] Prandini | A probabilistic approach to aircraft conflict detection[END_REF], communication networks [START_REF] João | Stochastic Hybrid Systems: Application to Communication Networks[END_REF], biochemical processes [START_REF] Li | Review of stochastic hybrid systems with applications in biological systems modeling and analysis[END_REF][START_REF] Singh | Stochastic hybrid systems for studying biochemical processes[END_REF]. The software tool UPPAAL [START_REF] David | Statistical Model Checking for Stochastic Hybrid Systems[END_REF] implements a model of SHS similar to the one studied in this article and uses numerical methods to compute reachability probabilities, through numerical solving of differential equations and Monte Carlo simulation. Reachability problems have also been considered in an alternative semantics with discrete time; a numerical approach is for instance provided in [START_REF] Abate | Approximate Model Checking of Stochastic Hybrid Systems[END_REF][START_REF] Abate | Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems[END_REF].

Notations. We write R + = {x ∈ R | x ≥ 0} for the set of non-negative real numbers. Let (Ω, Σ) be a measurable space. We write Dist(Ω, Σ) (or Dist(Ω) if there is no ambiguity) for the set of probability distributions over (Ω, Σ). The complement of a set A ∈ Σ is denoted by A c = Ω \ A. For A ∈ Σ, we say that two probability distributions µ, ν ∈ Dist(Ω) are (qualitatively) equivalent on A if for each B ∈ Σ, if B ⊆ A, µ(B) > 0 if and only if ν(B) > 0.

Decisiveness of Stochastic Transition Systems

In this section, we define stochastic transition systems (STSs, for short) as in [START_REF] Bertrand | When are stochastic transition systems tameable?[END_REF]. We then describe the concept of decisiveness, first defined in the specific case of Markov chains [START_REF] Parosh | Decisive Markov Chains[END_REF], and then extended to STSs [START_REF] Bertrand | When are stochastic transition systems tameable?[END_REF]. Decisive stochastic systems benefit from "nice" properties making their qualitative and quantitative analysis more accessible. The first contribution of our work is a new decisiveness criterion (Proposition 2.8), which generalizes existing criteria from the literature [START_REF] Parosh | Decisive Markov Chains[END_REF][START_REF] Bertrand | When are stochastic transition systems tameable?[END_REF]. It is an intuitive criterion, which was conjectured in [START_REF] Bertrand | When are stochastic transition systems tameable?[END_REF] but could not be proved. We finish with a brief section on the notion of abstraction between STSs, which will be useful to apply our results to stochastic hybrid systems. [START_REF] Bertrand | When are stochastic transition systems tameable?[END_REF] Definition 2.1 (Stochastic transition system). A stochastic transition system (STS) is a tuple T = (S, Σ, κ) consisting of a measurable space of states (S, Σ), and a function κ : S × Σ → [0, 1] (sometimes called Markov kernel) such that for every s ∈ S, κ(s, •) is a probability measure and for every A ∈ Σ, κ(•, A) is a measurable function.

Stochastic Transition Systems and Decisiveness

The second condition on κ implies in particular that for a measurable set B ∈ Σ, the set {s ∈ S | κ(s, B) > 0} is measurable.

We interpret STSs as systems generating runs, with a probability measure over these runs. We fix an STS T = (S, Σ, κ). From a state s ∈ S, a probabilistic transition is performed according to distribution κ(s, •), and the system resumes from one of the successor states; this process generates random sequences of states. A run of T is an infinite sequence s 0 s 1 s 2 . . . of states. To formally provide a probabilistic semantics to STSs, we define a probability measure over the set of runs of T . From an initial distribution µ ∈ Dist(S), we can define in a classical way a unique probability measure Prob T µ on the σ -algebra generated by all the cylinders, using Carathéodory's extension theorem.

Expressing properties of runs. We use standard LTL notations [START_REF] Pnueli | The Temporal Logic of Programs[END_REF] to express properties of runs of T . If B, B ∈ Σ, we write in particular F B (resp. F ≤n B, B U B, B U ≤n B, G B, G F B) for the set of runs that visit B at some point (resp. visit B in less than n steps, stay in B until a first visit to B, stay in B until a first visit to B in less than n steps, always stay in B, visit B infinitely often). We are interested in two kinds of reachability problems. Definition 2.2 (Qualitative and quantitative reachability). Let B ∈ Σ be a measurable set of target states, and µ ∈ Dist(S) be an initial distribution. The qualitative reachability problems consist in deciding whether Prob T µ (F B) = 1, and whether Prob T µ (F B) = 0. The quantitative reachability problem consists in deciding, given ε, p ∈ Q with ε > 0, whether |Prob T µ (F B) -p| < ε.

Transforming probability distributions. Another useful way to reflect on STSs is as transformers of probability distributions on (S, Σ). Definition 2.3 (STS as a transformer). For µ ∈ Dist(S), its transformation through T is the probability distribution Ω T (µ) ∈ Dist(S) defined for A ∈ Σ by

Ω T (µ)(A) = s∈S κ(s, A) dµ(s).
The value Ω T (µ)(A) is the probability to reach A in one step, from the initial distribution µ.

Attractors. We will be particularly interested in the existence of attractors for STSs. Definition 2.4 (Attractor). A set A ∈ Σ is an attractor for T if for every µ ∈ Dist(S), Prob T µ (F A) = 1. While S is always an attractor for T , we will later search for attractors with more interesting properties. The definition of attractor actually implies a seemingly stronger statement: an attractor is almost surely visited infinitely often from any initial distribution [10, Lemma 19].

Decisiveness. Before introducing decisiveness, we give the definition of an avoid-set: for B ∈ Σ, its avoid-set is written as B = {s ∈ S | Prob T δ s (F B) = 0} (where δ s is the Dirac distribution at s). The avoid-set B corresponds to the set of states from which runs almost surely stay out of B ad infinitum. One can show that the set B belongs to the σ -algebra Σ [10, Lemma 14]. We can now define the concept of decisiveness as in [START_REF] Bertrand | When are stochastic transition systems tameable?[END_REF]. Definition 2.5 (Decisiveness). Let B ∈ Σ be a measurable set. We say that T is decisive w.r.t. B if for every µ ∈ Dist(S), Prob T µ (F B ∨ F B) = 1. Intuitively, the decisiveness property states that, almost surely, either B will eventually be visited, or states from which B can no longer be reached will eventually be visited.

Example 2.6 (Random walk). We consider the STS T (random walk) from Figure 1. We want to find out whether T is decisive w.r.t. B = {0}. We assume that the initial distribution is given by δ 1 (the Dirac distribution at 1). By the theory on random walks, if 1 2 < p < 1, the walk will almost surely diverge to ∞. This entails that Prob T δ 1 (F B) < 1. Moreover, since p < 1, there is a path with positive probability from every state to 0, so B = / 0. Therefore,

Prob T δ 1 (F B ∨ F B) = Prob T δ 1 (F B) < 1, which means that T is not decisive w.r.t. B. If p ≤ 1
2 , state 0 is almost surely reached from any state, that is, for any initial distribution µ ∈ Dist(S), we have that A major interest of the decisiveness concept lies in the design of simple procedures for the qualitative and quantitative analysis of stochastic systems. Indeed, as presented in [START_REF] Parosh | Decisive Markov Chains[END_REF][START_REF] Bertrand | When are stochastic transition systems tameable?[END_REF], it allows, under effectiveness hypotheses, to verify qualitative properties or to compute arbitrary close approximations of the probabilities of various properties, like reachability, repeated reachability, and even ω-regular properties. The reader is referred to [START_REF] Bertrand | When are stochastic transition systems tameable?[END_REF]Sections 6 & 7] for more details, but we briefly recall the approximation scheme for reachability properties in order to illustrate the usefulness of the decisiveness property. This scheme will be applied to a specific class of STSs in Section 3.3.

Prob T µ (F B) = 1. Hence, in this case, STS T is decisive w.r.t. B. . . . 0 1 2 1 p p 1 -p 1 -p 1 -p
Let B ∈ Σ be a measurable set and µ ∈ Dist(S) be an initial distribution. To compute an approximation of Prob T µ (F B), we define two sequences

(p Yes n ) n∈N and (p No n ) n∈N such that for n ∈ N, p Yes n = Prob T µ (F ≤n B) and p No n = Prob T µ (B c U ≤n B).
These sequences are non-decreasing and converge respectively to Prob T µ (F B) and Prob T µ (B c U B). Observe moreover that for all n ∈ N, we have that

p Yes n ≤ Prob T µ (F B) ≤ 1 -p No n .
The main idea behind decisiveness of STSs lies in the following property [START_REF] Parosh | Decisive Markov Chains[END_REF][START_REF] Bertrand | When are stochastic transition systems tameable?[END_REF]

A New Criterion for Decisiveness

Our goal is to provide new sufficient conditions for the decisiveness of STSs. To this end, we expose the following crucial technical lemma. Lemma 2.7. Let B ∈ Σ, and A ∈ Σ. Suppose that there is p > 0 such that for all ν ∈ Dist(A), we have Prob T ν (F B) ≥ p. Then for any µ ∈ Dist(S), Prob T µ (G B c ∧ G F A) = 0. This result seems rather intuitive: if we visit A infinitely often, and after every passage through A we have a probability bounded from below to reach B, then the probability to stay in B c forever is 0. An equivalent statement for Markov chains has been used without proof in [START_REF] Parosh | Decisive Markov Chains[END_REF]Lemmas 3.4 & 3.7]. A weaker version of this statement is given as part of the proof of [START_REF] Bertrand | When are stochastic transition systems tameable?[END_REF]Proposition 36], where it is said that this general case was not known to be true or false. This weaker version assumes that there is a uniform upper bound k such that for all ν ∈ Dist(A), Prob T ν (F ≤k B) ≥ p to obtain a similar conclusion. We have removed the need for this constraint.

A possible proof of this result consists of regarding a stochastic transition system as a stochastic process, and resorting to results from martingale theory. More precisely, using Lévy's zero-one law, we obtain that infinite runs that never reach B are the same (up to a set of probability 0) as the infinite runs s 0 s 1 . . . for which the probability to reach B given s 0 . . . s n converges to 0 as n grows to infinity. Runs that visit A infinitely often cannot both avoid B and have a probability to visit B that converges to 0 (since for every visit to A, the probability to visit B is bounded from below by p > 0). Therefore, such runs will almost surely visit B.

We can now state our main contribution to decisiveness. Proposition 2.8 (Decisiveness criterion). Let B ∈ Σ be a measurable set, and A ∈ Σ be an attractor for T . We denote A = A ∩ ( B) c the set of states of A from which B is reachable with a positive probability. Assume that there exists p > 0 such that for all ν ∈ Dist(A ),

Prob T ν (F B) ≥ p. Then T is decisive w.r.t. B.
With probability 1, every run visits attractor A infinitely often, but the hypotheses imply a dichotomy between runs. Some runs will reach a state of A from which B is almost surely non-reachable (i.e., in B). The other runs will go infinitely often through states of A such that the probability of reaching B is lower bounded by p (i.e., in A ), and will almost surely visit B by Lemma 2.7. This almost-sure dichotomy between runs is required to show decisiveness.

This criterion strictly generalizes those used in the literature. The criterion in [START_REF] Parosh | Decisive Markov Chains[END_REF]Lemma 3.4] assumes the existence of a finite attractor; the criteria in [START_REF] Bertrand | When are stochastic transition systems tameable?[END_REF]Propositions 36 & 37] assume some finiteness property in an abstraction (see next section), which we do not. In [3, Lemma 3.7], a similar kind of property as ours is required from all the states of the STSs, not only from an attractor. We can actually prove the same result using a slightly more general notion of attractor (see [START_REF] Bouyer | Decisiveness of Stochastic Systems and its Application to Hybrid Models[END_REF]Proposition 11]).

Abstractions of Stochastic Transitions Systems

Decisiveness and abstractions are deeply intertwined concepts, so we briefly recall this notion [START_REF] Bertrand | When are stochastic transition systems tameable?[END_REF] and related properties. We let T 1 = (S 1 , Σ 1 , κ 1 ) and T 2 = (S 2 , Σ 2 , κ 2 ) be two STSs, and α :

(S 1 , Σ 1 ) → (S 2 , Σ 2 ) be a measurable function. We say that a set B ∈ Σ 1 is α-closed if B = α -1 (α(B)).
To mean that B is α-closed, we also say that α is compatible with B. Following [START_REF] Bogachev | Measure theory[END_REF][START_REF] Gburek | Composition of Stochastic Transition Systems Based on Spans and Couplings[END_REF], we define a natural way to transfer measures from (S 1 , Σ 1 ) to (S 2 , Σ 2 ) through α: the pushforward of α is the function α # : Dist(S 1 ) → Dist(S 2 ) such that α # (µ)(B) = µ(α -1 (B)) for every µ ∈ Dist(S 1 ) and for every B ∈ Σ 2 . Definition 2.9 (α-abstraction). STS T 2 is an α-abstraction of

T 1 if for all µ ∈ Dist(S 1 ), α # (Ω T 1 (µ)) is qualitatively equivalent to Ω T 2 (α # (µ)).
Informally, the two STSs then have the same "qualitative" single steps. Later, we may speak of abstraction instead of α-abstraction if α is clear in the context.

The objective of the notion of abstraction is that by finding an α-abstraction T 2 which is somehow simpler than T 1 (for example, with a smaller state space), we should be able to use T 2 (with initial distribution α # (µ)) to analyze some properties of T 1 (with initial distribution µ). To do so, we need to know which properties are preserved through an α-abstraction. As a first observation, positive probability of reachability properties is preserved. Stronger conditions are required to study almost-sure reachability properties through α-abstractions. We select a key property of abstractions about that matter which will be useful in the subsequent sections. Definition 2.10 (Sound α-abstraction). We say that T 2 is a sound α-abstraction of

T 1 if for all B ∈ Σ 2 , Prob T 2 α # (µ) (F B) = 1 implies Prob T 1 µ (F α -1 (B)) = 1.
Sound abstractions preserve almost-sure reachability properties from T 2 to T 1 . A major result from [START_REF] Bertrand | When are stochastic transition systems tameable?[END_REF] is that if T 1 is decisive w.r.t. B and T 2 is a sound α-abstraction, then for all µ ∈ Dist(S 1 ),

Prob T 1 µ (F α -1 (B)) = 1 if and only if Prob T 2 α # (µ) (F B) = 1.
Additional results about abstractions are provided in [START_REF] Bouyer | Decisiveness of Stochastic Systems and its Application to Hybrid Models[END_REF]Section 2.4].

Application to Stochastic Hybrid Systems

We choose to restrict our attention to a stochastic extension of the well-studied hybrid systems. A hybrid system is a dynamical system combining discrete and continuous transitions. It can be defined as a non-deterministic automaton with a finite number of continuous variables, whose evolution is described via an infinite transition system. Hybrid systems have been widely studied since their introduction in the 1990s (e.g., [START_REF] Alur | The Algorithmic Analysis of Hybrid Systems[END_REF][START_REF] Henzinger | The Theory of Hybrid Automata[END_REF]). They are effectively used to model various time-dependent reactive systems; systems that need to take into account both continuous factors (e.g., speed, heat, time, distance) and discrete factors (e.g., events, instructions) are ubiquitous.

We define hybrid systems and give them a fully stochastic semantics, yielding the class of stochastic hybrid systems (SHSs). We then show that under classical definability hypotheses, we can obtain decidability results for qualitative and quantitative reachability problems in a class of SHSs (even though such problems are undecidable in full generality), using decisiveness (along with our new decisiveness criterion) as a key tool. This provides a stochastic extension to the study of o-minimal hybrid systems [START_REF] Brihaye | On O-Minimal Hybrid Systems[END_REF][START_REF] Gentilini | Reachability Problems on Extended O-Minimal Hybrid Automata[END_REF][START_REF] Lafferriere | O-Minimal Hybrid Systems[END_REF].

Hybrid Systems with Probabilistic Semantics

We proceed with the definition of a (non-deterministic) hybrid system. Definition 3.1 (Hybrid system). A hybrid system (HS) is a tuple H = (L, X, A , E, γ, I , G , R) where: L is a finite set of locations (discrete states); X = {x 1 , . . . , x n } is a finite set of continuous variables; A is a finite alphabet of events; E ⊆ L × A × L is a finite set of edges; for each ∈ L, γ( ) : R n × R + → R n is a continuous function describing the dynamics in location ; I assigns to each location a subset of R n called invariant; G assigns to each edge a subset of R n called guard; R assigns to each edge e and valuation v ∈ R n a subset R(e)(v) of R n called reset. For ∈ L, e ∈ E, we usually denote γ( ) and R(e) by γ and R e .

We denote the number of variables |X| by n. Given a hybrid system H , we define S H = L × R n as the states of H . We distinguish two kinds of transitions between states:

• there is a switch-transition ( , v) a - → ( , v ) if there exists e = ( , a, ) ∈ E such that v ∈ I ( )∩G (e), v ∈ R e (v) ∩ I ( ); • there is a delay-transition ( , v) τ - → ( , v ) if there exists τ ∈ R + such that for all 0 ≤ τ ≤ τ, γ (v, τ ) ∈ I ( ) and v = γ (v, τ).
Informally, a switch-transition ( , v) a -→ ( , v ) means that an edge e = ( , a, ) can be taken without violating any constraint: the value v of the continuous variables is an element of the invariant I ( ) and of the guard G (e), and there is a possible reset v of the variables which is an element of the invariant I ( ). A delay-transition ( , v) τ -→ ( , v ) means that some time τ elapses without changing the discrete location of the system-the only constraint is that all the values taken by the continuous variables during this time are in the invariant I ( ).

Given s = ( , v) ∈ L × R n a state of the hybrid system, and τ ∈ R + , we denote by s + τ = ( , γ (v, τ)) the new state after some delay τ, without changing the location.

We consider semantics given by mixed transitions, i.e., transitions that consist of a delay-transition (some time elapses) followed by a switch-transition (an edge is taken and the location changes). A mixed transition is denoted by

( , v) τ,a -→ ( , v ) if and only if there exists v ∈ R n such that ( , v) τ - → ( , v ) a - → ( , v ).
We usually assume that there is a bijection between the edges E and the alphabet of events A , and we omit mentioning this alphabet. If e = ( , a, ) ∈ E, we can thus denote e -→ (resp.

τ,e -→) for switch-transitions (resp. mixed transitions) instead of a -→ (resp. τ,a -→).

Example 3.2. We provide in Figure 2 an example of a hybrid system (first studied in [START_REF] Baier | Almost-Sure Model Checking of Infinite Paths in One-Clock Timed Automata[END_REF]). There are two continuous variables (x and y) and five locations, each of them equipped with the same simple dynamics: ẋ = ẏ = 1 (i.e., γ ((x, y), τ) = (x + τ, y + τ) for every location ∈ L). Locations 2 and 4 have the same invariant, which is {(x, y) | y < 1}; the other invariants are simply R 2 . Guards are written next to the edge to which they are related: for instance, G (e 4 ) = {(x, y) | y = 2}. The notation "x := 0" is used to denote a deterministic reset (in this case, the value of x is reset to 0 after taking the edge). For instance, R e 1 (x, y) = {(x, 0)} (the value of x is preserved and y is reset to 0). If nothing else is written next to an edge e, it means that there is no reset on e, i.e., that R e (v) = {v} for all v ∈ R n . An example of mixed transitions of this system can be ( 0 , (0, 0)) We give more vocabulary to refer to hybrid systems. If there is a switch-transition ( , v) e -→ ( , v ), we say that edge e is enabled at state ( , v)-this means that edge e can be taken with no delay from state ( , v). Given a state s = ( , v) and an edge e = ( , a, ) of H , we define I(s, e) = {τ ∈ R + | s τ,e -→ s } as the set of delays after which edge e is enabled from s, and I(s) = e I(s, e) as the set of delays after which any edge is enabled from s. For instance, in the hybrid system from Figure 2, for s = ( 0 , (0, 0.2)), we have I(s, e 0 ) = [0, 0.8), and I(s) = [0, 1.8) \ {0.8}.

We say that a state s ∈ L × R n is non-blocking if I(s) = / 0. In the sequel, we only consider hybrid systems such that all states are non-blocking, thereby justifying why considering solely mixed transitions is doable-such a transition is available from any state.

We now replace the non-deterministic elements of hybrid systems with stochasticity.

Definition 3.3 (Stochastic hybrid system). A stochastic hybrid system (SHS) is defined as a tuple H = (H , µ L , η R , θ ), where:

• H = (L, X, A , E, γ, I , G , R
) is a hybrid system, which is referred to as the underlying hybrid system of H . We require guards, invariants and resets to be Borel sets.

• µ L : L × R n → Dist(R + ) associates to each state a probability distribution on the time delay in R + (equipped with the classical Borel σ -algebra) before leaving a location. Given s ∈ L × R n , the distribution µ L (s) will also be denoted by µ s . We require that for every s ∈ L × R n , µ s (I(s)) = 1, i.e., the probability that an edge is enabled after a delay is 1.

• η R associates to each edge e and valuation v a probability distribution on the set R e (v) ⊆ R n . Given e ∈ E and v ∈ R n , the distribution η R (e)(v) will also be denoted by η e (v).

• θ : L × R n → Dist(E) assigns to each state of H a probability distribution on the edges. We require that θ (s)(e) > 0 if and only if edge e is enabled at s. For s ∈ L × R, we denote θ (s) by θ s . This distribution is only defined for states at which an edge is enabled.

Remark 3.4. The term "stochastic hybrid system" is used for a wide variety of stochastic extensions of hybrid systems throughout the literature. In this work, we consider stochastic delays, stochastic resets, a stochastic edge choice, and stochastic initial distributions. The way this probabilistic semantics is added on top of hybrid systems is very similar to how timed automata are converted to stochastic timed automata in [START_REF] Baier | Almost-Sure Model Checking of Infinite Paths in One-Clock Timed Automata[END_REF][START_REF] Bertrand | Quantitative Model-Checking of One-Clock Timed Automata under Probabilistic Semantics[END_REF][START_REF] Bertrand | Stochastic Timed Automata[END_REF]. Although dynamics appear to be deterministic, the model is powerful enough to emulate stochastic dynamics by assuming that extra variables are solely used to influence the continuous flow of the other variables. These variables can be chosen stochastically in each location through the reset mechanism. This is for example sufficient to consider a stochastic extension of the rectangular automata [START_REF] Henzinger | What's Decidable about Hybrid Automata?[END_REF], whose variables evolve according to slopes inside an interval (such as ẋ ∈ [START_REF] Abate | Approximate Model Checking of Stochastic Hybrid Systems[END_REF][START_REF] Alur | The Algorithmic Analysis of Hybrid Systems[END_REF]). Our model is very close to the one of the software tool UPPAAL [START_REF] David | Statistical Model Checking for Stochastic Hybrid Systems[END_REF]. In Section 3.3, we will identify the need to restrict the definition of some components of SHSs to ensure their definability; this is however not required for the results of Section 3.2.

When referring to an SHS, we make in particular use of the same terminology as for hybrid systems (e.g., runs, enabled edges, allowed delays I(•)) to describe its underlying hybrid system.

In order to apply the theory developed in Section 2, we give the semantics of an SHS H as an STS T H = (S H , Σ H , κ H ). The set S H is the set L × R n of states of H , and Σ H is the σ -algebra product between 2 L and the Borel σ -algebra on R n . To define κ H , we first explain briefly the role of each probability distribution in the definition of SHS. Starting from a state s = ( , v), a delay τ is chosen randomly, according to the distribution µ s . From state s + τ = ( , v ), an edge e = ( , a, ) (enabled in s + τ) is selected, following distribution θ s+τ (such an edge is almost surely available, as µ s (I(s)) = 1 by hypothesis). The next state will be in location , and the values of the continuous variables are stochastically reset according to the distribution η e (v ). We can thus define κ H as follows:

for s = ( , v) ∈ S H , B ∈ Σ H , κ H (s, B) = τ∈R + ∑ e=( ,a, )∈E θ s+τ (e) • v ∈R n 1 B ( , v )d(η e (γ (v, τ)))(v ) dµ s (τ)
where 1 B is the characteristic function of B. It gives the probability to hit set B ⊆ S H from state s in one step (representing a mixed transition). The function κ H (s, •) defines a probability distribution for all s ∈ S H . Definition 3.5 (STS induced by an SHS). For an SHS H , we define T H = (S H , Σ H , κ H ) as the STS induced by H .

Thanks to the stochasticity of our models, we can reason about both qualitative and quantitative reachability problems, as defined in Definition 2.2.

Undecidability. We provide a proof that qualitative and quantitative reachability problems for SHSs with "simple" features are undecidable. The undecidability in itself is not surprising, as some of the undecidability proofs from the literature about non-deterministic hybrid systems [START_REF] Henzinger | What's Decidable about Hybrid Automata?[END_REF][START_REF] Henzinger | Robust Undecidability of Timed and Hybrid Systems[END_REF] can be translated directly to our stochastic setting. Our goal with this new proof is to get as close as possible to the class that we will later (in Section 3.3) show to be decidable, in order to outline as well as possible an undecidability frontier.

We prove undecidability even when constrained to purely continuous distributions on time delays from any state, and very simple guards, resets, and dynamics (that can be defined in simple mathematical structures). This requires a distinct proof from [START_REF] Henzinger | What's Decidable about Hybrid Automata?[END_REF]. The result from [START_REF] Henzinger | Robust Undecidability of Timed and Hybrid Systems[END_REF] is close to the one we want to achieve, and we take inspiration from its proof. The proof consists of reducing the halting problem for two-counter machines to deciding whether a measurable set in an SHS is reached with probability 1. Proposition 3.6 (Undecidability of SHSs). The qualitative reachability problems and the approximate quantitative reachability problem are undecidable for stochastic hybrid systems with purely continuous distributions on time delays, guards that are linear comparisons of variables and constants, and using positive integer slopes for the flow of the continuous variables. The approximate quantitative problem is moreover undecidable for any fixed precision ε < 1 2 . Although the proof is centered on showing the undecidability of qualitative reachability problems, we get as a by-product the undecidability of the approximation. Indeed, as the systems used throughout the proof reach a target set B with a probability that is either 0 or 1, the ability to approximate Prob T H µ (F B) with ε < 1 2 would be sufficient to solve the qualitative problem. As the proof shows that these qualitative problems are undecidable, we obtain that the approximate quantitative problem is undecidable as well. Our result also implies that deciding whether a state lies in B is undecidable.

The Cycle-Reset Hypothesis

The literature about non-deterministic hybrid systems suggests that to obtain subclasses for which the reachability problem becomes decidable, one must set sharp restrictions on the continuous flow of the variables and/or on the discrete transitions (via the reset mechanism). In this decidable spectrum lie for instance the rectangular initialized automata, which are quite permissive toward the continuous evolution of the variables, but need strong hypotheses about the discrete transitions [START_REF] Henzinger | What's Decidable about Hybrid Automata?[END_REF]. Our approach lies at one end of this spectrum: we restrict the discrete behavior by considering strong resets, i.e., resets that forget about the previous values of the variables, decoupling the discrete behavior from the continuous behavior. We show that one strong reset per cycle of the graph is sufficient to obtain valuable results, and we name this property cycle-reset. This point of view has already been studied in [START_REF] Brihaye | On O-Minimal Hybrid Systems[END_REF][START_REF] Gentilini | Reachability Problems on Extended O-Minimal Hybrid Automata[END_REF][START_REF] Lafferriere | O-Minimal Hybrid Systems[END_REF] for non-deterministic hybrid systems, and in [START_REF] Bertrand | Quantitative Model-Checking of One-Clock Timed Automata under Probabilistic Semantics[END_REF] for stochastic timed automata. Note that previous work about finite abstractions of non-deterministic hybrid systems (called time-abstraction bisimulations) does not extend in general to "stochastic" abstractions (as defined in Section 2.3), as there may be transitions that have probability 0 to happen. Definition 3.7 (Strong reset, cycle-reset SHS). Given H a stochastic hybrid system and e an edge of H , we say that e has a strong reset (or is strongly reset) if there exist R * e ⊆ R n and η * e ∈ Dist(R * e ) such that for all v ∈ G (e), R e (v) = R * e and η e (v) = η * e . We say that an SHS H is cycle-reset if for every simple cycle of H , there exists a strongly reset edge.

If an edge e is strongly reset, it stochastically resets all the continuous variables when it is taken, and the stochastic reset does not depend on their values. We show two independent and very convenient results of cycle-reset SHSs: such SHSs are decisive w.r.t. any measurable set (the proof of this statement relies on the decisiveness criterion from Proposition 2.8), and admit a finite abstraction.

Decisiveness of cycle-reset SHSs. We motivate this section with an example of a simple nondecisive SHS, which we will use to show that our decisiveness result is tight. Example 3.8. We add a stochastic layer to the hybrid system of Example 3.2, pictured in Figure 2. The distributions on the time delays in locations 0 , 2 and 4 are uniform distributions on the interval of allowed delays. For instance, at state s = ( 0 , (x, y)), the distribution µ s follows a uniform distribution on [0, 2y). In locations 1 and 3 , the distributions on the delays are Dirac distributions. Reset and edge distributions are simply modeled as Dirac distributions. It is proved in [12, Section 6.2.2] that this SHS is not decisive w.r.t. B = { 2 } × R 2 . The proof is quite technical and we do not recall it here; intuitively, at each passage through location 0 , the value of y increases but stays bounded from above by 1, which decreases the probability to take edge e 0 (and thus reach B); this decrease is too fast to ensure that B is almost surely reached. Proposition 3.9. Every cycle-reset SHS is decisive w.r.t. any measurable set.

Placing (at least) one strong reset per simple cycle is an easy syntactic way to guarantee that almost surely, infinitely many strong resets are performed, which is the actual sufficient property used in the proof. As there are only finitely many edges, we can find a probability lower bound p on the probability to reach B after any strong reset, as required in the criterion of Proposition 2.8. Notice that as shown in Example 3.8, having independent flows for each variable and resetting each variable once in each cycle is not sufficient to obtain decisiveness; variables need to be reset on the same discrete transition in each cycle.

Existence of a finite abstraction. We show that cycle-reset SHSs admit a finite α-abstraction. We first give a simple example showing that without one strong reset per cycle, some simple systems do not admit a finite α-abstraction compatible with the locations. Example 3.10. Consider the SHS of Figure 3. The self-loop edge of 0 is the only edge not being strongly reset. We assume that we want to have an abstraction compatible with s * := { 1 } × R. In order to obtain an abstraction, we must split { 0 } × R n in s 0 := { 0 } × (-∞, 0) and { 0 } × [0, +∞), as all the states of s 0 can reach s * with a positive probability in one step, but none of the states of { 0 } × [0, +∞) can. Then, { 0 } × [0, +∞) must also be split into s 1 := { 0 } × [0, 1) and { 0 } × [1, +∞) because the states of s 1 can all reach s 0 with a positive probability in one step, but none of the states of { 0 } × [1, +∞) can. By iterating this argument, we find that the smallest α-abstraction compatible with { 1 } × R is countably infinite, and the partition that it induces is composed of s * , s 0 and s i = { 0 } × [i -1, i) for i ≥ 1. The underlying hybrid system actually belongs to the class of updatable timed automata [START_REF] Bouyer | Updatable timed automata[END_REF], and the abstraction almost coincides with the region graph of the automaton. The reasoning we have used is very close to the classical bisimulation algorithm for non-deterministic systems, and is explained in more detail in [START_REF] Bouyer | Decisiveness of Stochastic Systems and its Application to Hybrid Models[END_REF]Section 2.4].

x < 0

x := 0 ẋ = 1 x ≥ 0 x := x -1 0 1 ẋ = 1
x ∈ R

x := 0 The proof consists of showing that a stochastic adaptation of the classical bisimulation algorithm terminates under the cycle-reset assumption. Combined with our decisiveness result, we can even show that this abstraction is sound.

Reachability Analysis in Cycle-Reset Stochastic Hybrid Systems

Our goal in this section is to perform a reachability analysis of cycle-reset SHSs. A first hurdle to circumvent is that arbitrary SHSs are in general difficult to apprehend algorithmically: for instance, the continuous evolution of their variables may be defined by solutions of systems of differential equations, which we do not know how to solve in general. To make the problem more accessible, we follow the approach of [START_REF] Brihaye | On O-Minimal Hybrid Systems[END_REF][START_REF] Lafferriere | O-Minimal Hybrid Systems[END_REF] for non-deterministic hybrid systems by assuming that some key components of our systems are definable in a mathematical structure. We identify a large class of SHSs for which the finite abstraction from Section 3.2 is computable, which makes qualitative reachability problems decidable; namely, cycle-reset o-minimal SHSs defined in a decidable theory. We then identify sufficient hypotheses for the approximate quantitative problem to be decidable, in the form of a finite set of probabilities that have to be approximately computable.

Qualitative analysis. We assume that the reader is familiar with basic model-theoretic and logical terms-the reader is referred to [START_REF] Hodges | A Shorter Model Theory[END_REF] for an introduction to the main concepts. In what follows, by definable, we mean definable without parameters. Definition 3.12 (Definable SHS). Given a structure M , an SHS H is said to be defined in M if for every location ∈ L, γ is a function definable in M and I ( ) is a set definable in M , and for every edge e ∈ E, the set G (e) is definable and there exists a first-order formula ψ e (x, y) such that v ∈ R e (v) if and only if ψ e (v, v ) is true.

Note that we require that the flow of the dynamical system in each location is definable in M , and not that it is the solution to a definable system of differential equations.

Our goal is to prove that the class of cycle-reset o-minimal SHSs, i.e., cycle-reset SHSs defined in an o-minimal structure (introduced in [START_REF] Van Den Dries | Remarks on Tarski's problem concerning (R, +, *, exp)[END_REF][START_REF] Pillay | Definable sets in ordered structures[END_REF]), with additional assumptions on the probability distributions, is decidable. We will use that the finite sound abstraction from Proposition 3.11 is then computable, and that decisiveness (Proposition 3.9) gives us a strong link between reachability properties of the abstractions and the original systems. In other words, the definable subsets of M are exactly the ones that are definable with parameters in M, < . Some well-known structures are o-minimal, such as the ordered additive group of rationals Q, <, +, 0 , the ordered additive group of reals R lin = R, <, +, 0, 1 , the ordered field of reals R alg = R, <, +, •, 0, 1 , the ordered field of reals with the exponential function R exp = R, <, +, •, 0, 1, e x [START_REF] Wilkie | Model completeness results for expansions of the ordered field of real numbers by restricted Pfaffian functions and the exponential function[END_REF]. There is no general result about the decidability of the theories of o-minimal structures. A well-known case is the Tarski-Seidenberg theorem [START_REF] Tarski | A decision method for elementary algebra and geometry[END_REF], which asserts that there exists a quantifier-elimination algorithm for sentences in the first-order language of real closed fields. This result implies the decidability of the theory of R alg . However, it is not known whether the theory of R exp is decidable. Its decidability is implied by Schanuel's conjecture, a famous unsolved problem in transcendental number theory [START_REF] Macintyre | On the decidability of the real exponential field[END_REF]. In this work, we define an o-minimal SHS as an SHS defined in an o-minimal structure.

The o-minimality of M implies that definable subsets of M n have a very "nice" structure, described notably by the cell decomposition theorem [START_REF] Knight | Definable sets in ordered structures[END_REF]. In particular, every subset of R n definable in an o-minimal structure belongs to the σ -algebra of Borel sets of R n [30, Proposition 1.1]. Moreover, to help with issues related to the definability of probabilities, we will use the property that in o-minimal structures, definable sets with positive Lebesgue measure coincide with definable sets with non-empty interior [START_REF] Kaiser | First order tameness of measures[END_REF]Remark 2.1]. This is very helpful, as the property of having an empty interior is definable.

Remark 3.14. The definition of o-minimal (non-deterministic) hybrid system in the literature usually assumes that all edges are strongly reset. O-minimal hybrid systems were first introduced in [START_REF] Lafferriere | O-Minimal Hybrid Systems[END_REF], and further studied notably in [START_REF] Brihaye | On O-Minimal Hybrid Systems[END_REF]. The strong reset hypothesis was relaxed in [START_REF] Gentilini | Reachability Problems on Extended O-Minimal Hybrid Automata[END_REF] to "one strong reset per cycle".

Let M = R, <, +, . . . be an o-minimal structure whose theory is decidable, such as R alg . Let H = (H , µ L , η R , θ ) be a cycle-reset o-minimal SHS defined in M . Let µ ∈ Dist(S H ) be an initial distribution. We make the following assumptions, which we denote by ( †):

• for all s = ( , v) ∈ L × R n , if I(s) is finite, µ s is equivalent to the uniform discrete distribution on I(s); if I(s) is infinite, µ s is equivalent to the Lebesgue measure on I(s);

• the initial distribution µ is either equivalent to the discrete measure on some finite definable support D, or equivalent to the Lebesgue measure on a definable support D;

• for e ∈ E, v ∈ R n , we ask that R e (v) is finite or has positive Lebesgue measure; η e (v) is resp. either equivalent to the discrete measure or the Lebesgue measure on R e (v).

The first requirement was already a standard assumption in the case of stochastic timed automata [START_REF] Baier | Almost-Sure Model Checking of Infinite Paths in One-Clock Timed Automata[END_REF][START_REF] Bertrand | Quantitative Model-Checking of One-Clock Timed Automata under Probabilistic Semantics[END_REF][START_REF] Bertrand | Stochastic Timed Automata[END_REF]. Hypothesis ( †) is easily satisfied: for instance, exponential distributions (resp. uniform distributions on [a, b]) are equivalent to the Lebesgue measure on R + (resp. [a, b]). We summarize what these ideas entail in the next proposition. Proposition 3.15. Let H be a cycle-reset o-minimal SHS defined in a structure whose theory is decidable. Let B ∈ Σ H be definable and µ ∈ Dist(S H ). We assume that assumption ( †) holds. Then one can decide whether Prob T H µ (F B) = 1 and whether Prob T H µ (F B) = 0.

In particular, we can decide the qualitative reachability problems for cycle-reset SHSs defined in R alg and satisfying ( †). Assuming Schanuel's conjecture [START_REF] Macintyre | On the decidability of the real exponential field[END_REF], we could extend this result to R exp .

Approximate quantitative analysis. Under strengthened numerical hypotheses, we can solve the approximate quantitative reachability problem in cycle-reset SHSs. Let H be a cycle-reset SHS, B ∈ Σ H and µ ∈ Dist(S H ). Our goal is to apply the approximation scheme described in [START_REF] Bertrand | When are stochastic transition systems tameable?[END_REF] in order to approximate Prob T H µ (F B). To do so, we require that T H is decisive w.r.t. B, which is implied by the cycle-reset hypothesis (Proposition 3.9), and the ability to compute for all m ∈ N, an arbitrarily close approximation of

Conclusion

Summary. We presented in Section 2 how to solve reachability problems in stochastic transition systems via the decisiveness notion, introduced in [START_REF] Parosh | Decisive Markov Chains[END_REF][START_REF] Bertrand | When are stochastic transition systems tameable?[END_REF]. We notably solved in Lemma 2.7 a technical question that was open in [START_REF] Bertrand | When are stochastic transition systems tameable?[END_REF], which helped formulate a general sufficient condition for decisiveness in Proposition 2.8, encompassing known decisiveness criteria from the literature.

In Section 3, we considered stochastic hybrid systems (SHSs). We showed that SHSs with one strong reset per cycle (cycle-reset) are decisive (using our new decisiveness criterion), and admit a finite abstraction. We then identified assumptions, using ideas from logic, leading to the effective computability of this abstraction, and to the decidability of qualitative and quantitative reachability problems. These assumptions pertain to the definability of the different components of the SHSs in a decidable mathematical structure. Combined with the previous decisiveness results, this abstraction can be used to decide qualitative reachability problems. In particular, these results apply to cycle-reset SHSs defined in R alg = R, <, +, •, 0, 1 with well-behaved distributions.

Possible extensions and future work. We identify some possible extensions of our results. A first direction of study is to find other classes of decisive stochastic systems that can be encompassed by our decisiveness criterion (Proposition 2.8). In that respect, a good candidate is the class of stochastic regenerative Petri nets [START_REF] Horváth | Transient analysis of non-Markovian models using stochastic state classes[END_REF][START_REF] Paolieri | Probabilistic Model Checking of Regenerative Concurrent Systems[END_REF]. An application of decisiveness results to stochastic Petri nets was briefly discussed in [START_REF] Bertrand | When are stochastic transition systems tameable?[END_REF]Section 8.3], but under severe constraints; we may be able to relax part of these constraints with the generalized criterion.

In Section 3.3, we circumvent the issue of the definability of measures by using a specific property of the o-minimal structures (namely, that the Lebesgue measure of a definable set is positive if and only if the interior of that set is non-empty). However, more powerful results exist about the compatibility of o-minimal structures and measure theory [START_REF] Kaiser | First order tameness of measures[END_REF]: some o-minimal structures are closed under integration with respect to a given measure (then called tame measure). This consideration may help extend our results to a larger class that is less restrictive w.r.t. probability distributions, or in which actual probabilities may be definable.

Figure 1 :

 1 Figure 1: STS T representing a random walk on N.

0. 4 2 Figure 2 :

 422 Figure 2: Example of a hybrid system with two continuous variables. Each location is equipped with the dynamics ẋ = ẏ = 1.

Figure 3 :

 3 Figure 3: The time delays are given by exponential distributions from any state; resets are Dirac distributions. The smallest abstraction compatible with { 1 } × R is countably infinite.

Definition 3 .

 3 13 (O-minimality). A totally ordered structure M = M, <, . . . is o-minimal if every definable subset of M is a finite union of points and open intervals (possibly unbounded).

p

  Yes m = Prob T µ (F ≤m B) and p No m = Prob T µ (B c U ≤m B).Using the cycle-reset hypothesis, we can express these probabilities as sums and products of a finite number of probabilities of paths with bounded length b ∈ N, where b is the length of the longest path without encountering a strong reset. Details on this computation are available in [14, Section 5.2].

  : if T is decisive w.r.t. B, then lim n→∞ p Yes

n + p No n = 1. Therefore, for any given ε > 0, for some n sufficiently large, p Yes n ≤ Prob T µ (F B) ≤ p Yes n + ε. In situations where p Yes n and p No n can be effectively approximated arbitrarily closely and T is decisive w.r.t. B, we can thus approximate Prob T µ (F B) up to any desired error bound.

Acknowledgments. We would like to thank the anonymous reviewers for their valuable advice, which notably helped simplify the proof of Lemma 2.7.

* Research supported by F.R.S.-FNRS under Grant n • F.4520.18 (ManySynth), and ENS Paris-Saclay visiting professorship (M. Randour, 2019). Pierre Vandenhove is an F.R.S-FNRS Research Fellow. Mickael Randour is an F.R.S-FNRS Research Associate.