Abstract
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.
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Alur, R., Dill, D.L.: A Theory of Timed Automata. Theoretical Computer Science 126(2), 183–235 (1994)
Baier, C., Bertrand, N., Bouyer, P., Brihaye, T., Größer, M.: Probabilistic and Topological Semantics for Timed Automata. In: Arvind, V., Prasad, S. (eds.) FSTTCS 2007. LNCS, vol. 4855, pp. 179–191. Springer, Heidelberg (2007)
Baier, C., Bertrand, N., Bouyer, P., Brihaye, T., Größer, M.: Almost-Sure Model Checking of Infinite Paths in One-Clock Timed Automata. In: Proceedings of LICS 2008, pp. 217–226. IEEE Comp. Soc. Press (2008)
Baier, C., Katoen, J.-P.: Principles of model checking. MIT Press (2008)
Bertrand, N., Schewe, S.: Playing optimally on timed automata with random delays. In: Jurdziński, M., Ničković, D. (eds.) FORMATS 2012. LNCS, vol. 7595, pp. 43–58. Springer, Heidelberg (2012)
Bouyer, P., Brinksma, E., Larsen, K.G.: Optimal infinite scheduling for multi-priced timed automata. Formal Methods in System Design 32(1), 3–23 (2008)
Bouyer, P., Forejt, V.: Reachability in Stochastic Timed Games. In: Albers, S., Marchetti-Spaccamela, A., Matias, Y., Nikoletseas, S., Thomas, W. (eds.) ICALP 2009, Part II. LNCS, vol. 5556, pp. 103–114. Springer, Heidelberg (2009)
Brázdil, T., Krčál, J., Křetínský, J., Kučera, A., Řehák, V.: Stochastic Real-Time Games with Qualitative Timed Automata Objectives. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 207–221. Springer, Heidelberg (2010)
Chatterjee, K., de Alfaro, L., Henzinger, T.A.: Qualitative concurrent parity games. ACM Transactions on Computation Logic 12(4), 28 (2011)
Chatterjee, K., Tracol, M.: Decidable problems for probabilistic automata on infinite words. In: Proceedings of LICS 2012, pp. 185–194. IEEE (2012)
Chen, T., Han, T., Katoen, J.-P., Mereacre, A.: Reachability Probabilities in Markovian Timed Automata. In: Proceedings of CDC-ECC 2011, pp. 7075–7080. IEEE (2011)
de Alfaro, L., Henzinger, T.A., Kupferman, O.: Concurrent reachability games. Theoretical Computer Science 386(3), 188–217 (2007)
Fijalkow, N., Gimbert, H., Oualhadj, Y.: Deciding the value 1 problem for probabilistic leaktight automata. In: Proceedings of LICS 2012, pp. 295–304. IEEE (2012)
Gimbert, H., Oualhadj, Y.: Probabilistic automata on finite words: Decidable and undecidable problems. In: Abramsky, S., Gavoille, C., Kirchner, C., Meyer auf der Heide, F., Spirakis, P.G. (eds.) ICALP 2010. LNCS, vol. 6199, pp. 527–538. Springer, Heidelberg (2010)
Laroussinie, F., Markey, N., Schnoebelen, P.: Model checking timed automata with one or two clocks. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 387–401. Springer, Heidelberg (2004)
Wolovick, N., Johr, S.: A Characterization of Meaningful Schedulers for Continuous-Time Markov Decision Processes. In: Asarin, E., Bouyer, P. (eds.) FORMATS 2006. LNCS, vol. 4202, pp. 352–367. Springer, Heidelberg (2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Bertrand, N., Brihaye, T., Genest, B. (2014). Deciding the Value 1 Problem for Reachability in 1-Clock Decision Stochastic Timed Automata. In: Norman, G., Sanders, W. (eds) Quantitative Evaluation of Systems. QEST 2014. Lecture Notes in Computer Science, vol 8657. Springer, Cham. https://doi.org/10.1007/978-3-319-10696-0_25
Download citation
DOI: https://doi.org/10.1007/978-3-319-10696-0_25
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-10695-3
Online ISBN: 978-3-319-10696-0
eBook Packages: Computer ScienceComputer Science (R0)