Jump to : Download | Abstract | Contact | BibTex reference | EndNote reference |

QEST14

N. Bertrand, Th. Brihaye, B. Genest. Deciding the value 1 problem for reachability in 1-clock decision stochastic timed automata. In proceedings of the 11th International Conference on Quantitative Evaluation of Systems (QEST'14), Springer (ed.), LNCS, Volume 8657, Pages 313-328, Firenze, Italy, September 2014.

Download [help]

Download paper: Doi page

Download Hal paper: Hal : Hyper Archive en ligne

Download paper: Adobe portable document (pdf) pdf

Copyright notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.
This page is automatically generated by bib2html v216, © INRIA 2002-2007, Projet Lagadic

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 epsilon-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 epsilon-optimal strategies must change their decisions, and more surprisingly these timings cannot be chosen uniformly over the set of regions

Contact

Nathalie Bertrand http://www.irisa.fr/prive/nbertran/
Blaise Genest http://perso.crans.org/~genest/

BibTex Reference

@InProceedings{QEST14,
   Author = {Bertrand, N. and Brihaye, Th. and Genest, B.},
   Title = {Deciding the value 1 problem for reachability in 1-clock decision stochastic timed automata},
   BookTitle = {proceedings of the 11th International Conference on Quantitative Evaluation of Systems (QEST'14)},
   editor = {Springer, },
   Volume = {8657},
   Pages = {313--328},
   Series = {LNCS},
   Publisher = {Springer},
   Address = {Firenze, Italy},
   Month = {September},
   Year = {2014}
}

EndNote Reference [help]

Get EndNote Reference (.ref)