Deciding the Value 1 Problem for Reachability in 1-Clock Decision Stochastic Timed Automata

Nathalie Bertrand 1 Thomas Brihaye 2 Blaise Genest 1
1 SUMO - SUpervision of large MOdular and distributed systems
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
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.
Type de document :
Communication dans un congrès
Quantitative Evaluation of Systems (QEST'14), Sep 2014, Florence, Italy. pp.313 - 328, 2014, 〈10.1007/978-3-319-10696-0_25〉
Liste complète des métadonnées

Littérature citée [16 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01088113
Contributeur : Nathalie Bertrand <>
Soumis le : jeudi 27 novembre 2014 - 14:15:48
Dernière modification le : vendredi 16 novembre 2018 - 01:39:29
Document(s) archivé(s) le : lundi 2 mars 2015 - 09:23:59

Fichier

paper44.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Nathalie Bertrand, Thomas Brihaye, Blaise Genest. Deciding the Value 1 Problem for Reachability in 1-Clock Decision Stochastic Timed Automata. Quantitative Evaluation of Systems (QEST'14), Sep 2014, Florence, Italy. pp.313 - 328, 2014, 〈10.1007/978-3-319-10696-0_25〉. 〈hal-01088113〉

Partager

Métriques

Consultations de la notice

239

Téléchargements de fichiers

68