Statistical Approximation of Optimal Schedulers for Probabilistic Timed Automata

Abstract : The verification of probabilistic timed automata involves finding schedulers that optimise their nondeterministic choices with respect to the probability of a property. In practice, approaches based on model checking fail due to state-space explosion, while simulation-based techniques like statistical model checking are not applicable due to the nondeterminism. We present a new lightweight on-the-fly algorithm to find near-optimal schedulers for probabilistic timed automata. We make use of the classical region and zone abstractions from timed automata model checking, coupled with a recently developed smart sampling technique for statistical verification of Markov decision processes. Our algorithm provides estimates for both maximum and minimum probabilities. We compare our new approach with alternative techniques, first using tractable examples from the literature, then motivate its scalability using case studies that are intractable to numerical model checking and challenging for existing statistical techniques.
Type de document :
Communication dans un congrès
Integrated Formal Methods, Jun 2016, Reykjavik, Iceland. 9681, pp.99-114, 2016
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01387362
Contributeur : Sean Sedwards <>
Soumis le : mardi 25 octobre 2016 - 16:45:49
Dernière modification le : mercredi 21 février 2018 - 01:54:35

Fichier

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

Identifiants

  • HAL Id : hal-01387362, version 2

Citation

Pedro D'Argenio, Arnd Hartmanns, Axel Legay, Sean Sedwards. Statistical Approximation of Optimal Schedulers for Probabilistic Timed Automata. Integrated Formal Methods, Jun 2016, Reykjavik, Iceland. 9681, pp.99-114, 2016. 〈hal-01387362v2〉

Partager

Métriques

Consultations de la notice

624

Téléchargements de fichiers

112