Marco Cammarata

Roman Bertoni

Maciej Lorenc

Hervé Cailleau

Sergio Di Matteo

Cindy Mauriac

Samir Matar

Henrik Lemke

Matthieu Chollet

Sylvain Ravy

Claire Laulhé

Jean-François Létard

Eric Collet
email: eric.collet@univ-rennes1.fr

Sequential Activation of Molecular Breathing and Bending during Spin-Crossover Photoswitching Revealed by Femtosecond Optical and X-Ray Absorption Spectroscopy

Keywords: Codes : 42.70.Gi, 75.30.Wx, 78.47.J-, 82.53.Xa

come

role of significant changes of the metal-ligand distance (molecular breathing). It was proposed that the ultrafast ISC results from the dephasing of the photoexcited state into the HS phonon states. A monotonous decay of the photoexcited state to the HS state becomes efficient when this breathing mode is rapidly damped as energy is dissipated into the environment.

By combining femtosecond x-ray absorption near edge structure (XANES) and optical spectroscopy, we provide an experimental evidence of the ultrafast activation and damping of molecular breathing accompanying the ISC, which were lacking up to now. This process is followed by vibrational cooling in the HS potential observed on the bending mode. With respect to conventional models describing SCO photoswitching in terms of potential energy curve along a single breathing coordinate, our work reveals a more complex reality involving a curved trajectory, along breathing and bending, on a multi-dimensional potential energy surface.

Results. The SCO [Fe(phen) 2 (NCS) 2 ] crystal investigated here, undergoes a first-order phase transition from LS (S=0, t 2g 6 e g 0 L 0 ) to HS (S=2, t 2g The ultrafast photoswitching dynamics of [Fe(phen) 2 (NCS) 2 ] is investigated in the LS phase at 140 K by two complementary pump-probe methods 12 . A 50 fs laser pulse (650 nm) photo-switches LS state to HS via a metal-to-ligand charge-transfer process (MLCT). 10 The changes in XANES are recorded with 30 fs x-ray pulses at the XPP station of the LCLS X-FEL, 21 while changes in optical reflectivity (OR) and transmission (OT) are recorded with 50 fs VIS-NIR spectroscopy. Fig. 2(a) shows the time course of the XANES signal measured at two energies most sensitive to the structural change (Fig. 1). The increase of XANES signal at 7.125 keV and the decrease at 7.148 keV mainly result from Fe-N elongation 20 and are the fingerprints of the formation of HS structures. We fit the rising time by convolving a Gaussian temporal Instrument Response Function (IRF) with an exponential rise ( Fe-N ). The 110 (10) fs FWHM IRF, obtained by using a timing tool 21 designed to synchronize the optical and the x-ray laser pulses, allows an accurate determination of  Fe-N = 170 (20) fs. Figs. 2(b-d) & S4 show time traces of OR and OT (with 110 fs IRF) in different spectral zones, revealing two main steps: the onset of OR change or a peak in OT immediately after laser excitation, relaxing towards a plateau during the first 100's fs. The increase of optical absorption on the plateau, which translates into a simultaneous decrease of OR and OT in all probed regions, is another fingerprint of the LS-to-HS photo-switching, also observed during the thermal LS-to-HS conversion 10 (see also Fig. S3). Density of state calculations 22 explain the stronger absorption of the HS state around 760 nm (1.6 eV) by a decrease of the energy gap between t 2g and e g bands from  1.9 eV (LS) to 1.6 eV (HS), due to the molecular ligand field weakening (see also Fig. S5). OT and OR data at 760 nm indicate that the gap narrowing in HS state, resulting from the Fe-N elongation, occurs within  Fe-N 140 (20) fs. It correlates well with the 170 (20) fs time constant obtained by XANES. The transient OT peak corresponds to the absorption of the photoexcited singlet 1 MLCT state (t 2g 5 e g 0 L 1 ), and other possible intermediate (INT) electronic states 9 , and results from transition from a ligand level L to higher energy states (see Fig. S5) 10,12 . 760 nm therefore probes both INT and HS (t 2g -e g ) absorptions. The t 2g -e g absorption is no more accessible at 850 nm and above, and the main effect in the time traces is the absorption of the INT electronic state. This transient OT peak above 850 nm (Fig. 2(c-d) & S4) better characterizes the depopulation of the INT state, which decays within less than 50 fs. Thus far, our results determine an ISC of tens of fs and a 160 fs Fe-N bond elongation in a solid, both of which are similar to those reported for Fe II molecules in solution 23,24,25,26,27,28 .

On top of such changes, clear oscillating components are present in the optical data. Fig. 3a-c show the residuals after exponential fit. Data at 760 nm show a coherent vibration around 113 cm -1 (300 fs oscillation period) in the [0  700 fs] range. The corresponding time-dependent Fourier transforms are presented in Fig. 3(d-f) & S4 and the apparent rising time of the 113 cm -1 mode is limited by the Gaussian temporal window used 12 . It was already discussed above that OT and OR at 760 nm are sensitive to the Fe-N elongation, hereafter referred to as the breathing coordinate D. Therefore, the oscillations riding on 760 nm signals reflect the breathing mode, i.e. the totally symmetric Fe-N stretching, in relation with the symmetry conserving picture of the displacive spin-state switching. This observation is supported by calculations, according to which the only totally symmetric mode (symmetry A in the C 2 point group of the complex) in this frequency range is the breathing mode (125 cm -1 ) in the HS state 29,30 . The breathing mode is represented by green arrows in Fig. 1 and shown in video S1 12 . XANES data do not reveal such small oscillating features after the 0.2 Å elongation, because of the noise limit of the measurements, but we underline that the main Fe-N elongation occurs on a timescale approaching the half period of the breathing mode (Fig. 4(a)).

Optical data at 550, 900 nm (Fig. 2(c)) and 950 nm (Fig. S4) reveal another coherent vibration, in-phase for all these probing wavelengths. These oscillations around 85 cm -1 correspond to the butterfly mode (also of A symmetry) 29,30 , which bends the ligand and the N-Fe-N angles without significantly changing Fe-N distances (see purple arrows in Fig. 1 & video S2). This is a bending coordinate  31 and such a coherent ligand vibration was also observed for another Fe II SCO molecular system in solution. 26 Unlike the breathing mode, we observed that the bending mode with 390 fs period is only activated coherently during a second step, after  500 fs, with a maximum spectral weight around 1300 fs (Fig. 3 &S4). This bending occurs well after the 160 fs initial Fe-N elongation.

Such oscillations cannot be attributed to impulsive Raman process in the ground LS state because the LS breathing frequency is significantly higher (156 cm -1 ) 29,30 . In addition, there is no optical transitions from LS state to other excited states which can be probed in the 760-950 nm region (Fig. S5) and consequently the LS state is optically silent in our data.

Discussion. In SCO materials the Fe-N elongations during LS-to-HS conversion are very similar, but the ligand bending 12,19,31 also plays an important role for the relative stability of LS and HS states. Hauser evidenced in the kinetic studies of HSLS relaxation a breakdown of the single mode model and proposed to describe such systems by qualitatively splitting the reaction coordinate into the breathing and the bending modes 32 . Fig. 4(b) is a cartoon of a likely potential energy surface (PES) of [Fe(phen) 2 (NCS) 2 ] in the breathing and bending (D,) coordinate space. At thermal equilibrium (see ref 13 and Fig. S2) the LS potential is centred at (D LS =1.97 Å,  LS =35°) and the one of the HS state at (D HS 2.16 Å,  HS =65°). The delayed activation of the bending , with respect to breathing D is schematically represented in Fig. 4(b) on (D,) PES from stable LS to stable HS locations.

XANES, OT and OR data at 760 nm give an average elongation D mean (t) with a 160 fs time constant. OR at 900 nm, no more sensitive to D but only to the change of , gives an average torsion  mean (t) with 250 fs time constant.

We thus deduce from these different breathing and bending timescales a curved trajectory in the relevant coordinate space (D,) on PES. If we simply assume that the photoinduced HS state is not significantly different from the HS structure at thermal equilibrium, we can plot a trajectory in Fig. 3(h). It indicates that around 1 ps the motion is mainly along also simultaneously manifested by the strong spectral weight of the bending mode (Fig. 3(e-f)) The coupling of instantly photo-activated phonons to other modes can drive major structural reorganization in solids. 4,33,34 In the present case, the energy transfer between the two totally symmetric breathing (D) to bending () modes can be described by a linear coupling, with the classical equations of motion of coupled harmonic oscillators: µ i are the reduced masses of the oscillators (obtained from Gaussian calculations 12 ), k i are the force constants refined to reproduce 113 and 85 cm -1 frequencies of the oscillations,  i /µ i are the damping rates and k DΣ is the coupling between the two modes. A numerical fit of the oscillating part of the time dependent data 12 with these equations of motion gives the time evolution of the oscillating components D osc (t) and osc (t)Fig. 3(g)). These curves reproduce well the initial activation of the 113 cm -1 breathing oscillation, in agreement with the displacive description of the ISC along D. The fit also evidence a very fast damping of the breathing mode within 166 fs ( D /µ D =6ps -1 ). These results are in agreement with the theoretical model 8 introduced above, which considers an ISC of tens of femtoseconds accompanied by a structural elongation of the order of 100200 fs and a damping time constant shorter than the period of the breathing mode (300 fs here). The observed delayed coherent activation of  characterizes the energy transfer from the breathing to the bending modes schematically represented in Fig. 4b and the smaller damping of the bending mode (  /µ  =1.16 ps -1 ) indicates that the system oscillates (in the HS potential) as it gets vibrationally cooled within 900 fs. The additional transfer to other modes, for instance to lower frequency optical lattice phonons, can also be considered. A lattice mode is observed at 33 cm -1 (Fig. 3d), but its spectral weight is weaker. Thus, the major part of energy of the absorbed photon (1.9 eV) is dissipated, since each coherent molecular phonon only accounts for a small fraction of that energy. For instance, the energy of the breathing mode, E=½ mω 2 D 2 , can be estimated to only 40 meV, with reduced mass m=8.5 amu, angular frequency =2*113cm -1 and elongation D0.2Å.

Conclusion.

In the emerging field of control science, understanding the physical processes allowing functionalization with light on ultrafast time scale is a key issue. Our results confirm the fast intersystem crossing observed in such transition-metal systems [23][24][25][26][27][28] , as the change of electronic state is shorter than 50 fs and followed by a significant metal-ligand elongation within 160 fs. This initial structural change is directly coupled to the change of electronic state because of the less bonging nature of the HS state. Our experimental studies more importantly provides an experimental demonstration that the fast and highly efficient ISC is driven by the dephasing of the photoexcited state into the HS phonon states. The activated breathing mode is damped on a timescale (160 fs) close to its halfperiod, which allows an efficient trapping in the HS state as the decrease of the oscillation amplitude hinders recurrence to the initial state. We also show that the molecular bending is involved too, since the Fe-N elongation once established triggers the increase of the N-Fe-N bending because of ligand rigidity. Its delayed activation reveals a curved trajectory on a multi-dimensional potential energy surface, which underlines the limits of conventional descriptions along a single breathing coordinate on potential energy curves. This description of the photoswitching at the molecular scale, accompanied by important energy redistribution, sets the initial conditions for the slower transformation at material scale 35,36 . Such combination of xray and optical spectroscopies is key to disentangle the role of different degrees of freedom of electronic and/or structural nature in photoinduced phenomena. This work was supported by the Institut Universitaire de France, Rennes Métropole, Région Bretagne (CREATE 4146), ANR (ANR-13-BS04-0002), CNRS (PEPS SASLELX) and Europe (FEDER). Portions of this research were carried out at the Linac Coherent Light Source (LCLS) at SLAC National Accelerator Laboratory. LCLS is an Office of Science User Facility operated for the U.S. Department of Energy Office of Science by Stanford University.

Samples:

Single crystals of [Fe(phen) 2 (NCS) 2 ] compound were obtained by slow diffusion as indicated in reference (13). The powder films of [Fe(phen) 2 (NCS) 2 ] compound have been prepared according to the description of Gütlich and co-workers (14); i.e. i) by reacting 0.77 g (2.77 mmol) of FeSO 4 ・7H 2 O and 0.539 g (5.55 mmol) of KSCN in dry and freshly distilled methanol (6 ml), ii) by filtered off the K 2 SO 4 precipitate, and iii) by adding the solution to 1 g (5.55 mmol) of 1,10-phenanthroline in 3 ml of methanol.

Experimental details of femtosecond pump-probe studies

We have investigated the LS-to-HS photoswitching dynamics by performing pump-probe measurements at 140 K, where [Fe(phen) 2 (NCS) 2 ] is in the pure LS state. The sample was cooled by a nitrogen cryostream. For x-ray and optical studies, the pump wavelength was set to 650 nm where it efficiently induces LS-to-HS transition through MLCT process (see also Fig. S1 & S6).

x-ray absorption probe:

Optical pump and x-ray probe studies were performed at the XPP beamline of the LCLS X-FEL.

A femtosecond laser operating at 120 Hz delivered 50 fs pump pulses at 650 nm focused to 500×500 µm 2 on the sample, with intensities of the order of 2-5 µJ. The x-ray beam was monochromatised using the XPP double Si(111) crystal monochromator. To ensure pulse durations limited time resolution and avoid thermal drifts of the timing, the recently developed "timing tool" has been used (see ref 21 in the letter).

This has the capability of measuring the relative arrival time between x-ray and infrared laser pulses with few tens of femtoseconds resolution and on a shot-to-shot basis. The x-ray fluorescence was collected using a Si diode (Canberra FD450-18-300RM) positioned horizontally at a 90° angle with respect to the x-ray beam propagation direction. The incoming intensity was measured using noninvasive diagnostics (after the x-ray monochromator) developed for pulsed x-ray radiation. We detected the total x-ray fluorescence yield to obtain the XANES spectra in the vicinity of the Fe K-edge (7.120 keV). Optical pump -XAS probe studies on single crystal gave weak signal because of the limited matching of the penetration depths of optical pump and x-ray probe. Therefore, we used the powder films (~few centimeters square) and yet thin (5 µm) samples for increasing the signal/noise ratio. and detailed presentation is given in ref (16). The same method was used here for comparing the change of DOS in the HS phase. Results are given in Fig. S5. The major feature is the low dispersion of the peaks which is descriptive of a molecular system, i.e. in opposition to a metal or an intermetallic system where the DOS are broadened. Somehow, even in the organized periodic solid state, [Fe(phen) 2 (NCS) 2 ] exhibits a molecular behavior. The key information regarding the time-resolved optical studies presented here is that on both sides of the gap the DOS correspond the Fe d states which are respectively t 2g -and e g -like , as indicated by the colored bands. The DOS calculations indicate that -in the LS state the t 2g -e g gap is around 1.9 eV -in the HS state the t 2g -e g gap is around 1.6 eV

The LMCT process induced by femtosecond excitation in the LS state is shown by the red arrow.

Fig. 1 (

 1 Fig. 1 (color online). (a) LS (140 K, blue) and HS (200 K, red) structures of [Fe(phen)2(NCS)2] (phen=1,10-phenanthroline). The central Fe atom is bounded by N to the phenantroline and NCS groups. Green arrows represent the breathing mode and purple ones the bending mode. b) XANES spectra and difference XANES measured between the LS and HS states.

Fig. 2 (

 2 Fig. 2 (color online). Kinetic traces of XANES at 7125 and 7148 eV, fit with a single-exponential function of the rising edge (Fe-N=170 (10) fs) represented by red solid lines (a). Kinetic traces of OR and OT at 760 nm (b), OR at 900 nm & 550 nm and OT at 900 nm (c) and OT 850 nm (d). Fits by a single-exponential function describing the fast change plus a fifth order polynomial are represented by red solid lines.photochromism.7,10,11 Here, L corresponds to the LUMO of the ligand. This molecular bi-stability is associated with important structural reorganizations around the FeN 6 octahedron between both spin states (Fig.1(a), S1 & S2)12 ,131415161718 . The less bonding character of the HS state leads to the expansion of the average Fe-N bond length from <Fe-N> LS = 1.97 Å to <Fe-N> HS =2.16 Å, often observed for Fe II SCO7,19 . That changes the XANES spectrum as shown in Fig.1b, in agreement with the published data on this molecular crystal.20

Fig. 3 (

 3 Fig. 3 (color online). (a-c), oscillating component of OR at 760 nm, OR at 900 nm and OT at 850 nm. (d-f), time dependent FFT of the experimental data, showing the activation of the breathing mode and the delayed activation of the bending mode. Combined fits of OR at 900 nm and OT at 850 nm (red line) by the coupled oscillator model, which show the contribution of the bending () mode (b) and the superposition of bending () and breathing (D) modes (c). The time course of the oscillating component Dosc (300 fs) and osc (390 fs) obtained by the fit in (b) and (c) are displayed in (g) and the average evolutions of Dmean and mean obtained by the fit in Fig. 3 are displayed in (h).

Fig. 4 (

 4 Fig. 4 (color online). (a) schematic representation of the elongation and damping of the breathing mode along the D coordinate . (b) Classical trajectory in the (D,) space. Molecules in the LS (blue) potential reach 1 MLCT state by light excitation. Fast ISC, through possible INT states, drives D elongation during step 1 with the generation and damping of breathing phonon, followed by activation of additional bending phonons such as distortion , during step 2. The sequence is sketched at the bottom.

  The red precipitate was filtered off, washed with methanol and diethyl ether and further purified by the Soxhlet technique during 48 hours corresponding to the form I of [Fe(phen) 2 (NCS) 2 ] showing a first order spin transition around 180 K and LIESST, confirmed by magnetic measurements shown in Fig. S1. The powder film consists in µm size crystals in a polymeric matrix. XANES spectra measured on single crystal or on powder film are very similar.

Fig

  Fig. 1B shows the XANES spectra for the LS (140 K) and HS (200 K) states measured on the powder film.

Figure S1 .Figure S2 .

 S1S2 Figure S1. Magnetic (black) and photomagnetic (colored properties of a polycrystalline sample of [Fe(phen) 2 (NCS) 2 ]. Light excitation was performed at 650 nm.

  The time dependent OR and OT data are fitted with: and where  is the exponential population of the HS state and  is the overall 140 fs instantaneous response function (IRF) of this experiment.

Figure S4 .

 S4 Figure S4. OT at 760 nm (A), oscillating component (B) with 300 fs period (=113 cm -1 ) mode and time-dependent FFT showing the 113 cm -1 mode (C). OT at 950 nm (D), oscillating component (E) with a 85 cm -1 mode and time-dependent FFT (F). FFT of OR at 760 nm and OT at 760, 850 and 950 nm are shown below and indicate the two main modes at 113 cm -1 (breathing) and 85 cm -1 (bending).

Figure S5 .

 S5 Figure S5. Total DOS for [Fe(phen) 2 (NCS) 2 ] in its LS (blue) and HS (red) states with the t 2g and e g like bands (colored). Is the LS state (left) two nearly degenerates e g like bands are 1.9 eV above the t 2g . The light excitation (h red arrow) generates metal-to-ligand charge-transfer from metal (t 2g -like) to ligand (Llike) states (MLCT). The photoexcited L state gives rise to absorption peak around 760-850 nm (arrows left). In the HS state the main absorption around 760 nm is the t 2g -e g transition.

Figure S6 .

 S6 Figure S6. Schematic energy diagram and molecular orbitals obtained from DFT calculation. The LS LUMO molecular orbitals L of the ligand indicates that the laser pump induces a MLCT process from t 2g to L occurs on the phen groups. The HS HOMO with paired electron corresponds to the Fe-N NCS bonds and the probe signal is modulated by the t 2g -e g splitting. Fe atom is in the center, N atoms are blue, C atoms are grey, S atoms are yellow, H atoms are white.

e g 2 L 0 ) states above 180 K and exhibits photomagnetism and

http://wwwasdoc.web.cern.ch/wwwasdoc/minuit/minmain.html

Supplemental Material for

Sequential activation of molecular breathing and bending during spincrossover photoswitching revealed with femtosecond optical and x-ray absorption spectroscopy

Marco Cammarata, 1 Roman Bertoni, 1 Maciej Lorenc, 1 Hervé Cailleau, 1 Sergio Di Matteo, 1 Cindy Mauriac, 2 Samir Matar, 2 Henrik Lemke, 3 Matthieu Chollet, 3 Sylvain Ravy, 4 Claire Laulhé, 4 Jean-François Létard, 2 Eric Collet, 1,* * To whom correspondence should be addressed. E-mail: eric.collet@univ-rennes1.fr 1 Institut de Physique de Rennes, UMR CNRS 6251Université Rennes 1, 35042 Rennes cedex, France.

2 CNRS, Université de Bordeaux, ICMCB, 87 avenue du Dr. A. Schweitzer, Pessac, 33608 France.

Optical probe:

The spin-state switching is associated with important changes of optical properties of the [Fe(phen) 2 (NCS) 2 ] crystals. Absorption and reflectivity spectra are shown in Fig. S3 for the LS (100 K) and HS (210 K) states. The MLCT band of the LS state is centered around 650 nm, the wavelength used as a pump, whereas the d-d band is around 760 nm. The spectra are not very structured and the LS to HS thermal conversion results in a global increase of absorption and decrease of reflectivity below 670 nm and above 720 nm, as illustrated by the temperature dependence of optical transmission at 900 nm. Optical pump-probe studies were performed in Rennes, with a wavelength tunable femtosecond laser operating at 1 kHz and delivering 50 fs pump and probe pulses. Two-colour pump-probe spectroscopy studies were performed on single crystals (10-20µm thick). Time-resolved reflectivity measurements were performed at 550, 760 and 900 nm. Time-resolved transmission measurements were performed at 760, 850, 900 and 950 nm, since the absorption is too high in the visible range. A typical measurement of transient optical density (OD) at 900 nm is presented in Fig. S4.

Single-wavelength measurements probed the resulting dynamics through changes of optical reflectivity (OR) and optical transmission (OT) of the single crystal. In addition to data presented in Fig. 2 we show in Fig. S4 OT data at 760 nm and 950 nm (A&D) and their oscillating component (B&E). The time-dependent FFT (C&F) were obtained by sliding a 700 fs width Gaussian window. The Fe-N breathing mode at 113 cm -1 (with 300 fs period) observed at 760 nm is observed just after excitation, whereas the mode observed at 950 nm, corresponding to the bending mode also observed in Fig. 3 Molecular vibration frequencies calculations were carried out for [Fe(phen) 2 (NCS) 2 ] after geometry optimization, by using hybrid B3LYP functional with LANL2DZ basis set within Gaussian09 code (15).

Frequencies are determined from the second derivatives of the energy with respect to the atomic positions and then operating transformation to mass-weighted coordinates. Exploring the results especially for the vibrations and their animations with screen captures was done with Gaussview annex module to Gaussian. Video S1 shows the breathing mode and video S2 show the ligand bending mode. A complete analysis will be published elsewhere.

Coupled oscillators model:

The motion of two elastically coupled oscillators are described by the classical equations of motions: is the coupling between the two modes D and  i the damping constants due to the coupling to the phonon bath, µ i the reduced masses. The frequencies of the modes are  i = .

Given a set of constants and initial conditions: numerical integration (using the python module scipy.integrate.odeint ( 17


Nathalie Bertrand

Thomas Brihaye

Blaise Genest

Deciding the value 1 problem for reachability in 1-clock decision stochastic timed automata ⋆

We consider reachability objectives on an extension of stochastic timed automata (STA) with nondeterminism. Decision stochastic timed automata (DSTA) are Markov decision processes based on timed automata where delays are chosen randomly and choices between enabled edges are nondeterministic. Given a reachability objective, the value 1 problem asks whether a target can be reached with probability arbitrary close to 1. Simple examples show that the value can be 1 and yet no strategy ensures reaching the target with probability 1. In this paper, we prove that, the value 1 problem is decidable for single clock DSTA by non-trivial reduction to a simple almost-sure reachability problem on a finite Markov decision process. The ε-optimal strategies are involved: the precise probability distributions, even if they do not change the winning nature of a state, impact the timings at which ε-optimal strategies must change their decisions, and more surprisingly these timings cannot be chosen uniformly over the set of regions.

Introduction

Stochastic timed automata (STA) were originally defined in [START_REF] Baier | Probabilistic and Topological Semantics for Timed Automata[END_REF][START_REF] Baier | Almost-Sure Model Checking of Infinite Paths in One-Clock Timed Automata[END_REF] as a probabilistic semantics for timed automata, with the motivation to rule out 'unrealistic' paths in timed automata, and therefore alleviate some drawbacks of the mathematical model such as infinite precision of the clocks and instantaneous events. Of course, STA also form a new stochastic timed model, interesting on its own. Informally, the semantics of a stochastic timed automaton consists of an infinite-state infinitely-branching Markov chain whose underlying graph is the timed transition system associated with a timed automaton. The transitions between states are governed by the following: first, a delay is sampled randomly among possible delays, and second, an enabled transition is chosen randomly among enabled ones. Several models combining dense-time, continuous probabilities, and nondeterminism have been studied [START_REF] Bouyer | Reachability in Stochastic Timed Games[END_REF][START_REF] Brázdil | Stochastic Real-Time Games with Qualitative Timed Automata Objectives[END_REF][START_REF] Chen | Reachability Probabilities in Markovian Timed Automata[END_REF] and most result focus on qualitative questions, such as deciding the existence of a strategy ensuring a reachability objective with probability 1 (see the related work section).

A model that extends stochastic timed automata with nondeterminism was defined in [START_REF] Bertrand | Playing optimally on timed automata with random delays[END_REF]: the delays are random, but the choice between enabled transitions is nondeterministic. For this model, optimal strategies always exist for the time-bounded reachability problem. Yet, a simple example also shows that optimal strategies do not always exist for the reachability problem: there might be strategies to ensure a probability arbitrary close to 1 to reach a target location, and no strategy achieving probability 1.

More generally, the value 1 problem asks whether for every ε > 0 there exists a strategy ensuring a given objective with probability at least 1ε. It can be defined in various game-like contexts, ranging from probabilistic finite automata (PFA) to concurrent games. In most models where the agent has full information, the value 1 problem coincides with the almost-sure problem, that is, whether there exists a strategy to ensure a given objective with probability 1. For partial observation models however, the value 1 problem and the almost-sure problem often differ: for concurrent games, both are decidable [START_REF] De Alfaro | Concurrent reachability games[END_REF][START_REF] Chatterjee | Qualitative concurrent parity games[END_REF], whereas the value 1 problem is undecidable for PFA [START_REF] Gimbert | Probabilistic automata on finite words: Decidable and undecidable problems[END_REF], and decidable only for subclasses [START_REF] Fijalkow | Deciding the value 1 problem for probabilistic leaktight automata[END_REF][START_REF] Chatterjee | Decidable problems for probabilistic automata on infinite words[END_REF].

In this paper, we consider a probabilistic and nondeterministic version of stochastic timed automata, called decision stochastic timed automata (DSTA), in which delays are random but edges are selected by the player. Contrary to most existing frameworks on stochastic and timed models, we do not assume the distributions over delays to be exponential. We consider (time-unbounded) reachability objectives on DSTA with a single clock. The restriction to 1-clock DSTA derives from the fact that even for purely stochastic models without decisions (i.e. STA), the decidability of the almost-sure reachability problem is open, for models with at least two clocks. Using the classical region abstraction we show that the existence of an almost-surely winning strategy is decidable for reachability objectives on 1-clock DSTA. Interestingly, in our context, the value 1 problem does not coincide with the almost-sure problem, although the agent has full information. The main contribution of the paper is then to prove that the value 1 problem is decidable too. To do so, we build an ad hoc abstraction based on a refinement of regions, and reduce to an almost-sure reachability question in the derived finite-state Markov decision process (MDP). The correctness proof is complex, and ε-optimal strategies are involved: first they are not uniform within a region as actions they dictate depend on the comparison of the precise clock value with some cutpoint. Second, and more surprisingly, these cutpoints cannot be chosen uniformly over the set of regions.

Related work

In stochastic timed games [START_REF] Bouyer | Reachability in Stochastic Timed Games[END_REF], locations are partitioned into locations owned by three players, a reachability player (who has a time-bounded reachability objective), a safety player (who has the opposite objective), and an environment player (who makes random moves). In a location of the reachability or safety player, the respective player decides both the sojourn time and the edge to fire, whereas in the environment's locations, the delay as well as the edge are chosen randomly. For this model, it was shown that, assuming there is a single player and the underlying timed automaton has only one clock, the existence of a strategy for a reachability goal almost-surely (resp. with positive probability) is PTIME-complete (resp. NLOGSPACE-complete). For two-player games, quantitative questions are undecidable. Simple examples show that even for one player and 1-clock timed automata, the value 1 and probability 1 problems differ. This is due to strict inequalities in guards, that prevent the player to choose an optimal delay. We believe that our proof techniques can be adapted to solve the value 1 problem in 1-player stochastic timed games over 1-clock timed automata.

In stochastic real-time games [START_REF] Brázdil | Stochastic Real-Time Games with Qualitative Timed Automata Objectives[END_REF], environment nodes (in which the behaviour is similar to continuous time Markov decision processes (CTMDPs)) and control nodes (where players choose a distribution over actions) induce a probability distribution on runs. The objective for player 0 is to maximise the probability that a run satisfies a specification given by a deterministic timed automaton (DTA). The main result states that if player 0 has an almost-sure winning strategy, then she also has a simple one which can be described by a DTA.

Markovian timed automata (MTA) consist in an extension of timed automata with exponentially distributed sojourn time. Optimal probabilities can be approximated for time-(un)bounded reachability properties in MTA [START_REF] Chen | Reachability Probabilities in Markovian Timed Automata[END_REF].

Definitions and problem statement

Timed automata

Timed automata [START_REF] Alur | A Theory of Timed Automata[END_REF] were introduced in the early nineties. We recall the definition and semantics of one-clock timed automata. Given a clock x, a guard is a finite conjunction of expressions of the form x ∼ c where c ∈ N is an integer, and ∼ is one of the symbols {<, ≤, =, ≥, >}. We denote by G(x) the set of guards over clock x. Often, for g ∈ G(x) a guard and t a clock value, we will write t ∈ g to express that t satisfies the constraints expressed in g.

Definition 1. A one-clock timed automaton is a tuple (L, ℓ 0 , E, I) such that: L is a finite set of locations, ℓ 0 ∈ L is the initial location, E ⊆ L × G(x) × 2 {x} × L
is a finite set of edges, and I : L → G(x) assigns an invariant to each location.

In the following, we assume all timed automata to be well-formed : for every location ℓ ∈ L, I(ℓ) = (ℓ,g,a,r,ℓ ′ )∈E g, that is, the invariant in a location coincides with the union of the guards on its outgoing edges. This implies in particular that the union of guards outgoing a location is an interval.

The semantics of a one-clock timed automaton (L, ℓ 0 , E, I) is a timed transition system T = (S, s 0 , δ) where S = L × R ≥0 , s 0 = (ℓ 0 , 0) and the transition function δ ⊆ S × (R ≥0 ∪ E) × S is composed of -Delay transitions: (ℓ, t), τ, (ℓ, t + τ ) ∈ δ whenever [t, t + τ ] ⊆ I(ℓ) -Discrete transitions: (ℓ, t), e, (ℓ ′ , t ′ ) ∈ δ as soon as the edge e = (ℓ, g, r, ℓ ′ ) ∈ E satisfies t ∈ g and if r = {x}, t ′ = 0 else t ′ = t.

When convenient, we will use the alternative notations (ℓ, t) τ -→ (ℓ, t + τ ) and (ℓ, t) e -→ (ℓ ′ , t ′ ). Edge e is said enabled in state s = (ℓ, t), whenever there exists s ′ ∈ S such that s e -→ s ′ .

Decision stochastic timed automata

We now introduce the concept of decision stochastic timed automaton (DSTA). Roughly speaking, a decision stochastic timed automaton is a one-clock timed automaton equipped with probability distributions over delays. The semantics of DSTA is provided by an infinite-state MDP, in the spirit of [START_REF] Bertrand | Playing optimally on timed automata with random delays[END_REF].

In the following, given X ⊆ R ≥0 , we denote by Dist(X) the set of probability distributions on X. Definition 2. A decision stochastic timed automaton is a tuple A = (L, ℓ 0 , E, I, µ) where (L, ℓ 0 , E, I) is a one-clock timed automaton and µ = (µ ℓ,t ) is a family of distributions, one for each state (ℓ, t) ∈ L × R ≥0 , and such that µ ℓ,t ∈ Dist(I(ℓ) ∩ [t, +∞[).

Intuitively, for every state (ℓ, t) ∈ S, for every interval I ⊆ R ≥0 , µ ℓ,t (I) is the probability that from (ℓ, t) a delay d 0 , such that t + d 0 ∈ I, is chosen by µ.

We make some reasonable assumptions on the distributions. For every location ℓ, the function must satisfy the following sanity conditions: (c 1 ) for every t ∈ I(ℓ), and any non-punctual interval I ⊆ I(ℓ) ∩ [t, +∞[, µ ℓ,t (I) > 0; also if [t, +∞[∩I(ℓ) = {t}, then for any a ∈ R ≥0 , µ ℓ,t ({a}) = 0; (c 2 ) for every t < t ′ ∈ I(ℓ), and

I ⊆ [t ′ , +∞[, µ ℓ,t (I) ≤ µ ℓ,t ′ (I); (c 3 ) if |I(ℓ)| = ∞, then for every t, t ′ ∈ I(ℓ), for every a, b ∈ R ≥0 , µ ℓ,t ([t + a, t + b]) = µ ℓ,t ′ (t ′ + a, t ′ + b); if |I(ℓ)| < ∞, and m = sup{t | t ∈ I(ℓ)}, then for every t, t ′ ∈ I(ℓ), for every a, b ∈ R ≥0 , µ ℓ,t (t + a m-t , t + b m-t ) = µ ℓ,t ′ (t ′ + a m-t ′ , t ′ + b m-t ′ ).
Let us comment on these conditions. First, (c 1 ) states that the distributions are equivalent to the Lebesgue measure: they do not assign 0 measure to interval with non-empty interior, and do not assign positive probability to points. Then, (c 2 ) is a monotonicity condition: the higher the clock value, the more likely a fixed interval is to be sampled. Last, with (c 3 ) one assumes that distributions depend only on the location, not on the precise clock value. More precisely, in case the invariant is not bounded, the distributions should be equal in all states; and if the invariant is bounded, they should coincide up to normalisation. It is important to notice the classical exponential and uniform distributions satisfy these three hypotheses.

Notice that stochastic timed automata (STA) [START_REF] Baier | Probabilistic and Topological Semantics for Timed Automata[END_REF][START_REF] Baier | Almost-Sure Model Checking of Infinite Paths in One-Clock Timed Automata[END_REF] and DSTA share the same syntax, and only differ in their semantics: STA are interpreted as purely stochastic system whereas DSTA are interpreted as stochastic and nondeterministic systems. Let A be a decision stochastic timed automaton. Its semantics is given in terms of an infinite state MDP (or equivalently a 1-1/2 player game), based on the timed transition system T of the underlying timed automaton. The set of states is composed of two copies S and S of S: stochastic states S = { s | s ∈ S} and player states S = {[s] | s ∈ S}. The transitions are of the form:

-stochastic transition: s τ -→ [s ′ ] if (s, τ, s ′ ) ∈ δ; -player transition: [s] e -→ s ′ if (s, e, s ′ ) ∈ δ.
The result of each transition is thus deterministic. However stochastic transitions are not played in an arbitrary way, but follow the family of probability distributions (µ ℓ,t ). Precisely, for I ⊆ R ≥0 an interval, the probability from ℓ, t to reach a clock value in I is given by P( ℓ, t

τ -→ [ℓ, t ′ ] ∧ t ′ ∈ I) = µ ℓ,t (I).
Decisions of the nondeterministic player are specified through the notion of strategy. A history is a finite path in the MDP, ending in a player state:

s 0 τ0 -→ [s ′ 0 ] e0 -→ s 1 τ1 -→ [s ′ 1 ] • • • s n τn -→ [s ′ n ].
The set of all histories is denoted Hist. A strategy dictates the decision in states of S , given the history so far. Formally, a strategy is a function σ :

Hist → E such that σ( s 0 τ0 -→ [s ′ 0 ] e0 -→ s 1 τ1 -→ [s ′ 1 ] • • • s n τn -→ [s ′ n ]) is enabled in s ′ n .
As pointed out in [START_REF] Wolovick | A Characterization of Meaningful Schedulers for Continuous-Time Markov Decision Processes[END_REF] in the context of continuous-time Markov decision processes, not all strategies are meaningful. The same phenomenon appears for DSTA, and in the following we thus restrict to so-called measurable strategies that induce measurable sets of runs for reachability objectives.

For a fixed measurable strategy σ, and an initial state s 0 ∈ S ∪ S , the decision stochastic timed automaton A gives rise to a stochastic process. For a measurable event E , we write P A σ s 0 |= E for the probability of E starting from s 0 and under strategy σ. Given a target set F ⊆ S ∪ S in the DSTA, the event F , denotes the set of paths that eventually visit F .

Problem definition

Let A be a decision stochastic timed automaton, Goal ⊆ L and s ∈ S ∪ S . We define F = { ℓ, t | ℓ ∈ Goal}. The value of s, with respect to the objective Goal, is the supremum, over all strategies, of the probability from s to reach F .

Definition 3. The value of state s is val A (s) = sup σ P A σ s |= F .
The value 1 problem asks, given a decision stochastic timed automaton A, a target set Goal ⊆ L and an initial state s ∈ S ∪ S , whether val A (s) = 1.

F is said limit-surely reachable from s if val A (s) = 1.
Notice that this definition is different from the almost-sure reachability problem, which asks whether there exists a strategy σ such that P A σ s |= F = 1. From a state with value 1, for every ε, there exists a strategy achieving probability 1ε to reach F , yet it does not imply that some strategy realises the objective with probability 1. For finite-state Markov decision processes, and in many simple frameworks, value 1 and probability 1 coincide. However, this is untrue for DSTA, as shown in the example below. Example 1. Figure 1 shows a basic example of a DSTA, where the distributions µ are uniform in ℓ 0 and exponential with rate 1 in location ℓ 1 . The smiley location is limit-surely reachable from the initial location ℓ 0 with clock value 0. Indeed, the idea, in order to ensure a high probability 1ε to reach the target is to loop on ℓ 0 until a player state [ℓ 0 , 1τ ] is reached (this happens almost surely) for a small τ , and then to move to location ℓ 1 . Now, the probability from ℓ 1 , 1τ to reach the target converges to 1 as τ converges to 0. Yet, no strategy can ensure to reach the target with probability 1. This is thus a simple example where limit-sure reachability and almost-sure reachability differ. Such phenomena are not due to invariants, and already occur in DSTA where only exponential distributions are allowed. Indeed, one can adapt the above example and consider an exponential distribution in ℓ 0 , while transferring the invariant x ≤ 1 to the guard of e 2 .

Limit corner-point MDP

As an extension of timed automata, DSTA have infinitely many states, because of continuous time. The usual technique to deal with this issue for timed automata, is to resort to the region abstraction [START_REF] Alur | A Theory of Timed Automata[END_REF], which we recall here. For one-clock timed automata, the number of regions is linear [START_REF] Laroussinie | Model checking timed automata with one or two clocks[END_REF]: they all are intervals, either punctual {c}, open and bounded (c, d), or open and unbounded (c, +∞), for c, d ∈ N.

We write R for the set of such regions, and r denotes a typical element of R.

Beyond these classical regions, we will use pointed regions, similar to the notion introduced for the corner-point abstraction by [START_REF] Bouyer | Optimal infinite scheduling for multipriced timed automata[END_REF]: every bounded open region (c, d) is duplicated into (c, d) and (c, d), with the intuitive meaning of being close to the left limit, or to the right limit of the interval. Other regions (unbounded or punctual) are kept as is. When a timed automaton is fixed, R denotes the set of pointed regions, with r a typical element, and it is partitioned into: R right (resp. R left ) for the set of pointed regions of the form (c, d) (resp. (c, d)), and R plain for punctual regions or the unbounded region. Pointed regions are equipped with a natural total order <; for example {0} < (0, 1) < (0, 1). We say that pointed region r ′ is a successor of r if r < r ′ . The immediate open successor of r is the least region r ′ , for the order <, that is different from r and open. The set of all successors of a region r is denoted -→ r . A pointed region r ′ is said negligible with respect to location ℓ and region r, if r ′ ∈ -→ r , r ′ is punctual and I(ℓ) ∩ -→ r is not.

We now define the limit corner-point MDP associated with a DSTA.

Definition 4. Given A = (L, ℓ 0 , E, I, µ) a DSTA, its limit corner-point MDP is A cp = (S, s 0 , Act, ∆), where -S = S ∪ S is partitioned into player states and stochastic states:

S = {[ℓ, r] | ℓ ∈ L, r ∈ R} and S = { ℓ, r | ℓ ∈ L, r ∈ R}; -s 0 = ℓ 0 , {0} ; -Act = E ∪ E limit
, where E limit is a copy of E; -∆ consists of the following transitions:

• ℓ, r τ -→ [ℓ, r ′ ] as soon as r ′ ≥ r and r ′ is not negligible w.r.t. ℓ, and the probabilities are uniform over all τ -successors;

• [ℓ, r] e -→ ℓ ′ , {0} as soon as e = (ℓ, g, {x}, ℓ ′ ) ∈ E, and r |= g; • [ℓ, r]
e -→ ℓ ′ , r as soon as e = (ℓ, g, ∅, ℓ ′ ) ∈ E, and r |= g;

• [ℓ, r] e limit --→ ℓ ′ , r ′ as soon as r ∈ R right , e = (ℓ, g, ∅, ℓ ′ ) ∈ E, r |= g, r ′
is the immediate open successor of r, and r ′ |= I(ℓ ′ ).

With the exception of limit-edges, the definition of the limit corner-point MDP is natural since it mimics the behaviour of the DSTA, at the region level and abstracting precise probabilities. Limit-edges are particular to the value 1 problem. Roughly speaking, they offer the player, from region [ℓ, r], the possibility to play as if the clock value was arbitrarily close to the right border of r, therefore as if it was in r ′ the immediate open successor of r. In particular, there cannot be two consecutive transitions starting with a limit edge and staying in the same pointed region [ℓ, r]

e limit --→ τ -→ [ℓ ′ , r].
Example 2. Let us illustrate Definition 4 on the example of Fig. 2 below. Its limit corner-point MDP is represented in Fig. 3. For readability reasons we only represented states with left-pointed region for (1, 2), since the behaviour is exactly the same from right-pointed regions. We let F = {[ℓ, r] | ℓ ∈ Goal} in the rest of the paper. A cp is a finite MDP, and one can define strategies in the usual way. In the following, for s a state of A cp , and F ⊆ S we write P Acp max (s |= F) for the maximum probability, over all strategies, to reach F from s.

ℓ0 ℓ1 ℓ2 e0, x < 1 x := 0 e1, 0 < x < 1 e2, 1 < x < 2 x := 0 e3, 0 < x < 1 e4 , 0 < x < 1 e 5 , 1 ≤ x < 2
Last, we introduce some notations: First, for any region r ∈ R, we define

•r ∈ R left ∪ R plain (resp. r• ∈ R right ∪ R plain ) with: •(c, d) = (c, d) (resp. (c, d)• = (c, d)), •{c} = {c} = {c}• and •(c, +∞) = (c, +∞) = (c, +∞)•. Now, given t ∈ R ≥0 , r left (t) (resp. r right (t)) represents the left (resp. right) pointed region t belongs to: if t ∈ r, then r left (t) = •r (resp. r right (t) = r•).

Main results

We now state the main results of our paper. We start with an expected result: Proposition 1. The almost-sure reachability problem is decidable in PTIME for DSTA.

Proposition 1 is not a consequence of the decidability result in [START_REF] Bouyer | Reachability in Stochastic Timed Games[END_REF]. Although our model of DSTA can be encoded into the stochastic timed games of [START_REF] Bouyer | Reachability in Stochastic Timed Games[END_REF], the naive encoding requires an additional clock, in order to prevent players from letting time elapse. Since their decidability result applies only to stochastic timed games with a single clock, this simple reduction is of no help here. We believe their techniques can be adapted though. An alternative, which we take here, is to use the region abstraction, in order to solve the almost sure reachability problem. Details are provided Section 5.

As value 1 and probability 1 do not coincide for DSTA, the following theorem is non trivial, and is the main contribution of this paper.

Theorem 1. The value 1 problem is decidable in PTIME for DSTA.

To obtain Theorem 1, we reduce the value 1 problem for DSTA to the almost-sure reachability problem in the limit corner-point abstraction.

Proposition 2. Let A be a decision stochastic timed automaton, A cp its limit corner point abstraction, and ℓ ∈ L a location, and t ∈ R ≥0 a clock value. Then

val A ([ℓ, t]) = 1 ⇐⇒ P Acp max ([ℓ, r left (t)]) |= F) = 1 and val A ( ℓ, t ) = 1 ⇐⇒ P Acp max ( ℓ, r left (t) ) |= F) = 1 .
Example 3. Let us illustrate the result of Proposition 2 on the example of Fig. 2, whose limit corner-point MDP is represented on Fig. 3. Bold edges give a winning strategy in the MDP for the almost-sure reachability of the smiley state.

According to Proposition 2, the set of states with value 1 for the target in the stochastic timed automaton, is thus (ℓ 0 , [0, 1))

∪ (ℓ 1 , [1, 2)) ∪ (ℓ 2 , [1, 2)).
(Here, we use brackets as a short-cut, rather than square brackets or angle brackets, not to distinguish stochastic and player states.) Intuitively, an ε-optimal strategy from ℓ 0 , 0 to reach is the following: stay in ℓ 0 until a large clock value is sampled, then move to ℓ 1 ; if then the sampled clock value is above 1, move back to ℓ 0 and iterate the same process, otherwise, proceed to ℓ 2 ; finally, reach or from ℓ 2 depending on the last sampled clock value.

Theorem 1 is a consequence of Proposition 2. To obtain a polynomial-time algorithm, one exploits that for 1-clock decision stochastic timed automaton, the number of regions, and thus the number of states in the limit corner-point MDP is linear [START_REF] Laroussinie | Model checking timed automata with one or two clocks[END_REF], and almost-sure reachability properties can be checked in polynomial-time for finite MDP.

In order to show Proposition 2 we proceed in two steps: first, we prove it for player states [ℓ, t] ∈ S . This suffices to prove it as well for stochastic states ℓ, t ∈ S thanks to the structure of the limit corner-point MDP. Given A cp , we write W ⊆ S for the set of states from which there exists an almost-sure winning strategy for the reachability objective. We now detail what having left and/or right pointed region winning in the limit corner-point MDP abstraction implies:

Proposition 3. Let r ∈ R be a region and ℓ ∈ L a location.

-

If [ℓ, •r] ∈ W, then [ℓ, r•] ∈ W. -If [ℓ, •r] ∈ W, then for every t ∈ r, val A ([ℓ, t]) = 1; -Else, if [ℓ, r•] ∈ W, then for every t ∈ r, val A ([ℓ, t]) < 1; -Else, there exists ε > 0 such that for every t ∈ r, val A ([ℓ, t]) ≤ 1 -ε.
The first item is a simple observation: for every location ℓ and region r ∈ R, any winning strategy from [ℓ, •r] can be mimicked from [ℓ, r•], and is also winning from there. Section 4 is devoted to the rest of the proof of Proposition 3. Proposition 3 suffices to prove Proposition 2, in the case of player states. Indeed, the second item (whose proof is in Section 4.2) shows the right-to-left implication of Proposition 2, and the third and fourth items show the other implication by contraposition (the proof is in Section 4.1). Remark that we can be more specific in the third case and state: when [ℓ, •r] / ∈ W and [ℓ, r•] ∈ W, then sup t∈r val A ([ℓ, t]) = 1. This explains the difference between the third and fourth items.

Before moving to the proofs, we show an example where ε-optimal strategies need to be conceptually complex: the cutpoint inside regions where the strategy changes decision cannot be chosen independently of the location.

ℓ0 ℓ1 ℓ2 ℓ3 e1, x ≤ 1 e2, 1 ≤ x ≤ 2 x := 0 e3, x ≤ 1 e 4 , x ≤ 1 e 5 , x ≤ 1 e7, x ≤ 1 e6, 1 ≤ x ≤ 2 e0, x ≤ 1
Fig. 4. An example where non-uniform strategies are needed.

Consider the example from Fig. 4, where the implicit probability distributions over delays are all uniformly distributed. Decisions can only be taken in locations ℓ 0 and ℓ 2 , where transitions with overlapping guards are possible. Intuitively, from ℓ 0 to reach , transition e 1 needs to be taken, with a risk that once ℓ 1 is reached, transition e 5 is triggered. Let t 0 be the cutpoint in ℓ 0 such that if t 0 < t < 1, the player decides to take e 1 from (ℓ 0 , t). In the same way, let t 2 ∈ (0, 1) be the cutpoint in ℓ 2 such that if t 2 < t < 1, the player decides to take e 3 from (ℓ 2 , t). To reach a contradiction, we assume t 0 = t 2 , and write τ for this value. From [ℓ 2 , t] with 1τ < t < 1, a simple calculation shows that the probability to lose is p T lose (ℓ 2 , t) = (1t)/(2t). Also, from [ℓ 0 , t], the losing probability is lower bounded by the probability to lose in two steps, directly from ℓ 1 , hence p T lose (ℓ 0 , t) ≥ (1t)/(2t). Moreover, p T win (ℓ 0 , t) ≤ p T win (ℓ 1 , t) ≤ (1t)p T win (ℓ 3 , t) ≤ (1t). Hence, p T lose (ℓ 0 , t) > p T win (ℓ 0 , t)/2 for all t > 1τ , that is P T ( ℓ 0 , t |= F ) < 2/3. This shows that F is not limit-surely reachable under simple strategies, defined by constant mappings. Yet, the -state is limit-surely reachable from [ℓ 0 , 0]. However, to achieve this, t 0 needs to be set to a much lower value than t 2 , e.g. t 2 = τ and t 0 = τ 2 .

Deciding the value 1 problem

The goal of this section is to provide a proof of Proposition 3 (and thus of Proposition 2 and of Theorem 1). For the sake of completeness, we recall the algorithm to compute the set of states of an MDP from which there exists a strategy to reach a target set F almost-surely (see e.g. [START_REF] Baier | Principles of model checking[END_REF]). We denote by W the winning states for this objective, and W the subset of winning player states. The algorithm that computes W computes at the same time for every player state w ∈ W , the largest set of safe actions Safe(w), i.e. the set of all actions that ensure staying in W.

-Initially: L = ∅, and for every s ∈ S , Safe(s) = {e ∈ E ∪ E limit | ∃s e -→ s ′ }.

-Perform steps 1 and 2 until convergence.

• Step 1: Move to L every [ℓ, r] from which there is no path to F via states in S \ L only.

• Step 2: Remove from Safe([ℓ, r]) any e such that if [ℓ, r] e -→ ℓ ′ , r ′ , there exists [ℓ ′ , r ′′ ] ∈ L with ℓ ′ , r ′ → [ℓ ′ , r ′′ ]. Move to L every [ℓ, r] such that Safe([ℓ, r]) = ∅. -Return (W = S \ L, Safe).
The rest of the section is organised as follows. Subsection 4.1 establishes the third and fourth items of Proposition 3: states whose left region is not winning in the limit corner-point MDP, do not have value 1 in the decision stochastic timed automaton. Then, Subsection 4.2 shows its second item: states whose left region is winning in the limit corner-point MDP do have value 1 in the decision stochastic timed automaton.

Non limit-surely winning states

We first aim at showing the right-to-left implication in Proposition 2, by contraposition:

P Acp max ((ℓ, r left (t)) |= F) < 1 implies val A ([ℓ, t]) < 1.
This corresponds to proving the third and fourth items of Proposition 3. Lemma 1. Let ℓ ∈ L be a location and r ∈ R a region.

-If [ℓ, r•] ∈ L, then there exists ε ℓ,r > 0 such that for every t ∈ r, val A ([ℓ, t]) ≤ 1ε ℓ,r ; -If [ℓ, •r] ∈ L, then for every t ∈ r, there exists ε ℓ,t > 0 such that val A ([ℓ, t]) ≤ 1ε ℓ,t ; Moreover, one can pick non-increasing values for the ε ℓ,t 's, that is, ε ℓ,t ≤ ε ℓ,t ′ as soon as t ≥ t ′ .

Proof (Sketch). The proof is by induction on the moment in the MDP algorithm at which [ℓ, r] has been moved to L. We thus define

∅ = L 0 ⊆ L 1 ⊆ • • • L n = L
to describe the evolution of L during time with |L i | = i. Notice that this decomposition is finer than steps (this is important for step 2 of the MDP algorithm). We show one important subcase here. Assume [ℓ, (a, b)] ∈ L because of step 2. Every transition e in the DSTA are associated with a transition e in the MDP which leads from [ℓ, (a, b)] to ℓ ′ , r ′ , and there exists ℓ

′ , r ′ τ -→ [ℓ ′ , r ′′ ] with [ℓ ′ , r ′′ ] ∈ L i . The hardest case is when r ′′ = r ′ = r = (a, b).
Other cases are actually easier to treat and lead to a uniform bound ε over t. Let ν ℓ,t = µ ℓ,t (t, (t + b)/2) for every t ∈ (a, b). Observe that ν ℓ,t > 0 and is non increasing with t ∈ (a, b), by assumption (c 3 ) on the measure functions µ. We then set ε ℓ,t e = ν ℓ,t • ε ℓ ′ ,(t+b)/2 > 0 for all t ∈ (a, b). Note that ε ℓ,t e depends upon t. Last, we define ε ℓ,t = min e ε ℓ,t e , the minimum over all transitions e outgoing from [ℓ, t]. So defined, ε ℓ,t is positive and non increasing because ν ℓ,t and ε ′ ℓ ′ ,(t+b)/2 are positive and non increasing.

⊓ ⊔

Limit-surely winning states

We now prove that

P Acp max ((ℓ, r left (t)) |= F) = 1 implies val A ([ℓ, t]) = 1
. This amounts to show the second item of Proposition 3.

Covering forest and golden paths. Let A be a decision stochastic timed automaton, and A cp the associated limit corner-point MDP. From the almost sure winning set of states and actions (W, Safe) of A cp , we extract a covering forest whose roots are elements of F. Each edge of the forest from a player state w ∈ W to its unique parent is a transition of A cp , labelled with action sel(w) ∈ Safe(w). Globally, for every w ∈ W , the unique path to a root of the forest w ′ n ∈ F is a path in A cp : there are

w 1 • • • w n ∈ W and w ′ 1 • • • w ′ n ∈ W with w sel(w) ----→ w ′ τ -→ w 1 sel(w1) -----→ w ′ 1 • • • w n+1 sel(wn)
-----→ w ′ n , and such a path is called a golden path in the following. Notice that many edges emanating from stochastic states do not appear in this forest. They may lead to states that are further from F. The intuition is that this forest represents the ideal situation. Even if it is not guaranteed to take these ideal edges from stochastic states, there is a chance to follow the forest towards F, and we will show it is sufficient.

Example 4. Fig. 5 represents the covering forest, here a tree, on our running example from Fig. 2. Remark here that e 0 is selected in [ℓ 0 , (0, 1)] and e 1 in [ℓ 0 , (0, 1)]. The fact that they differ reflects that the decision for an optimal strategy should not be uniform within region (0, 1) in location ℓ 0 . ℓ1, (1, 2) ℓ0, (0, 1) ℓ0, (0, 1) ℓ1, ( Assume now that F is almost-surely reachable from (ℓ, r left (t)) in the limit corner-point A cp , and let us exhibit a family of ε-optimal strategies, showing that F is limit-surely reachable from ℓ, t in A. More precisely, these ε-optimal strategies are positional but not region uniform: for every location ℓ and bounded open region r = (c, d), there can be a cut-point c + τ ∈ (c, d) such that the decisions in the left part of r, (c, c+τ ) and in its right part (c+τ, d) differ, but are uniform over each of these sub-intervals. These cut-points can be defined through a mapping T : L × R → R ≥0 . When T is fixed, we write left T (ℓ, r) for the subregion of (ℓ, r), to the left of its cutpoint T (ℓ, r). Similarly, right T (ℓ, r) denotes the states to the right of the cutpoint. For t ∈ r, we write r T ([ℓ, t]) = [ℓ, r left (t)] if t ∈ left T (ℓ, r), and r T ([ℓ, t]) = [ℓ, r right (t)] if t ∈ right T (ℓ, r). We will abuse the notation and call a path s 1 • • • s n in the DSTA A a golden path if for (ℓ i , r i ) the golden path associated with r T (s 1 ), we have r T (s 2i+1 ) = [ℓ 2i+1 , r 2i+1 ] for all i (if a limit edge is played, it is not possible to agree on the stochastic state).

Based on the covering forest of selected actions, we build a family of strategies (σ T ) T :L×R→R ≥0 , parametrised by a cutpoint function ,(c,d)) and σ T (s) = sel((ℓ, (c, d))). In short, when T is fixed, σ T (s) = sel(r T (s)). Since limit edges do not exist in the DSTA, by σ T (s) = e limit , we implicitly mean σ T (s) = e, where e ∈ E is the unique edge associated with e limit ∈ E limit .

T : L × R → R ≥0 : if s ∈ left T (ℓ, (c, d)), then σ T (s) = sel((ℓ, (c, d))), else s ∈ right T (ℓ
We define the following subset of states in the DSTA A:

S win = {[ℓ, t] ∈ S | [ℓ, r left (t)] ∈ W}.
We show that all states in S win have value 1 for the reachability objective in A. Further, S right

T = {[ℓ, t] ∈ S | r T ([ℓ, t]) = [ℓ, r right (t)] ∈ W}
is the set of states belonging to the right-part (as specified by the cut-point function T ) of limit winning bounded open regions; Note that S right T and S win are not necessarily disjoint. Our objective is to show that for every ε > 0, there exists a mapping T such that, from any state s ∈ S win , the probability to reach F under σ T is at least 1ε.

Lemma 2. For every s ∈ S win ,

P A σ T (s |= (F ∪ S right T )) = 1.
When the mapping T is fixed, we let W T = {s | r T (s) ∈ W}, that is, states whose pointed-region (relatively to T ) is winning in the limit corner point. Notice that W T = S right T ∪ S win . We show that the probability to leave W T can be made arbitrarily small. Lemma 3. For every ε > 0, there exists a function T : L × R → R ≥0 such that, writing for the next-step operator, for every

s ∈ W T -if σ T (s) ∈ E limit then P s σ T ( W T ) ≥ 1 -ε, -else P s σ T ( W T ) = 1.
Taking a limit edge in the limit corner-point MDP is the only case where a losing state can be reached in the concrete DSTA. However, staying in the current region when the decision in the abstraction was a limit-edge may not necessarily lead to a losing state. Actually, limit-edges are not always the best choice: the only way to reach F might be to stay in the current region (and therefore avoid limit-edges) even if the probability to stay there is very small. This is illustrated on the example from Fig. 3 in which from [ℓ 0 , (0, 1)], in order to eventually reach F, one should pick e 1 rather than e limit 1 . We now explain that the probability to follow the covering forest towards F, although small, will be arbitrarily bigger than the probability to follow the forest until reaching a losing state.

Given T a mapping assigning cut-points to each bounded open region, and [ℓ, t] a player state in W T , we write p T win (ℓ, t) for the probability, from [ℓ, t] and under σ T , to execute a golden path (which therefore reach F ). Also, p T lose (ℓ, t) is the probability to execute a golden path until a losing state in S \ W T is reached. If from a stochastic state, a golden path is not executed, and yet L is not immediately reached either (this corresponds to behaviours not "counted" in p T lose and p T win ), then a winning region will be reached, possibly further away from F. Lemma 4. For every ε > 0, there exists a function T :

L × R → R ≥0 such that for every [ℓ, t] ∈ W T p T win (ℓ, t) • ε ≥ p T lose (ℓ, t
) . Given a tolerance ε, the proof of Lemma 4 details how to define a mapping, denoted T (ε) to make the dependency explicit, under which the probability to reach F by progressing in the covering forest is arbitrarily bigger than the probability to reach a losing state. The definition of T (ε) is non trivial and is done by induction on the distance to F in the covering forest. Recall that once a cut-point mapping T is fixed, the strategy σ T is perfectly defined. It now remains to justify that, the strategies (σ T (ε) ) form a family of limit-sure strategies.

Lemma 5. For every s ∈ S win , P

A σ T (ε) (s |= F ) ≥ 1 -ε. Proof. Let ε > 0, T (ε) : L × R → (0, 1
) the mapping as defined in Lemma 4, and σ T (ε) the corresponding strategy. To establish Lemma 5 we provide a lower bound on the probability, under σ T (ε) to reach F from winning states.

To do so, we consider the set X of runs under σ T (ε) that stay forever in W T \ F . Such runs never reach the target, and also stay away from the losing states. We will show that P A σ T (ε) (s |= X) = 0. To do so, we again partition X into three categories: X 1 gathers runs with infinitely many resets; X 2 consists of runs with finitely many resets and ending in the unbounded clock region (M, ∞); and X 3 is the set of runs with finitely many resets eventually staying in a bounded region (c, d). Let us first consider X 1 . Runs in X 1 necessarily visit some some state (ℓ 0 , 0) infinitely often. Since, at each visit of (ℓ 0 , 0), there is a strictly positive probability to execute a golden path and thus reach F , we reach a contradiction. Thus P A σ T (ε) (s |= X 1 ) = 0. We now consider runs in X 2 , that ultimately stay in the unbounded region. As explained earlier, almost surely F will be reached, a contradiction: P A σ T (ε) (s |= X 2 ) = 0. Last, for runs in X 3 , that ultimately stay in a bounded region (c, d), the reasoning is exactly the same as for runs of X 2 . Thus, P A σ T (ε) (s |= X 3 ) = 0. We now exploit Lemma 4 to conclude. Since almost all runs leave W T \ F , it must be that either a losing states or F is reached, and it suffices to compare the probabilities in each case. Thanks to Lemma 4, for all states in W T , it is much more likely to reach F than to reach a losing state. More precisely, p T win (ℓ, t) p T win (ℓ, t) + p T lose (ℓ, t) ≥ p T win (ℓ, t) p T win (ℓ, t) + p T win (ℓ, t)

• ε ≥ 1 1 + ε ≥ 1 -ε .
As a consequence P A σ T (ε) (s |= F ) ≥ (1ε).

⊓ ⊔

This ends the proof of the left-to-right implication in Proposition 2.

Deciding the probability 1 problem

If one wants to solve the probability 1 problem, rather than the more difficult value 1 problem, it suffices to consider the region MDP A R . This MDP A R is equivalent to the fragment of A cp restricted to left and plain regions, and hence without limit edges. As for the value 1 problem, the decidability of the probability 1 problem is given thanks to the following reduction: Proof. The proof is not different for player and stochastic states, so we treat them indistinctly, and use brackets in place of square or angle brackets. Let (ℓ, t) with t ∈ R, be a state of A such that P A R max ((ℓ, r) |= F) < 1. One can easily adapt the inductive proof of Lemma 1, showing that if (ℓ, r) is losing in the MDP A R , then for every t ∈ r, there exists ε ℓ,t with P A σ ((ℓ, t) |= F ) < 1ε ℓ,t whatever the strategy σ. For the other implication, it suffices to mimic faithfully in A the positional winning strategy σ A R from A R . For every (ℓ, r) a winning state in the region MDP A R , for every t ∈ r, we let σ(ℓ, t) = σ A R (ℓ, r). Now that the strategy is fixed, we recover the purely probabilistic framework of Stochastic Timed Automata, and can apply the results of [START_REF] Baier | Almost-Sure Model Checking of Infinite Paths in One-Clock Timed Automata[END_REF] to conclude that P A σ ((ℓ, t) |= F ) = 1. Alternatively, partitioning runs into three categories, as we did for the proofs of Lemmas 2 and 5, allows one to conclude that σ is almost-surely winning in A.

⊓ ⊔ Lemma 6, and precisely its right-to-left implication, does not hold in DSTA with at least two clocks. We emphasise here again that the decomposition of runs we use is only valid for 1-clock timed automata.

As an immediate consequence, we obtain the decidability in PTIME of the probability 1 problem for reachability objectives in DSTA (see Proposition 1).

Conclusion

This paper shows the decidability in PTIME of the probability 1 and value 1 problems for reachability objectives on an extension of 1-clock timed automata with random delays, and in which edges are chosen according to a strategy. It would be natural to allow for more general objectives (e.g. Büchi or parity). We could also investigate the extension of our framework to 2 players, taking decisions in turn or concurrently. Moving to more quantitative questions, such as computing the value would probably require a finer abstraction than the limit corner-point MDP. Last, the class of 1-clock DSTA can seem restrictive, and it is definitely a challenge to tackle already stochastic timed automata without decisions, for which the almost-sure model checking of reachability properties is still open.

Fig. 1 .

 1 Fig. 1. A simple example of decision stochastic timed automaton.

Fig. 2 .Fig. 3 .

 23 Fig. 2. The first illustrating example.

3 e5Fig. 5 .

 35 Fig. 5. The covering forest on our running example.

Lemma 6 .

 6 Let A be a decision stochastic timed automaton, A R its region MDP, r ∈ R a region, and ℓ ∈ L a location and t ∈ R ≥0 a clock value with t ∈ r. Then∃σ, P A σ ([ℓ, t] |= F ) = 1 ⇐⇒ P A R max ([ℓ, r] |= F) = 1 and ∃σ, P A σ ( ℓ, t |= F ) = 1 ⇐⇒ P A R max ( ℓ, r |= F) = 1 .

⋆ The research leading to these results has received funding from 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), the European Union Seventh Framework Programme (FP7/2007-2013) under Grant Agreement number 601148 (CASSTING), the project ANR-13-BS02-0011-01 STOCH-MC, and the professeur invité ISTIC-Rennes 1 programme.