Statistical Approximation of Optimal Schedulers for Probabilistic Timed Automata

• Main Authors: D'Argenio, Pedro, Hartmanns, Arnd, Legay, Axel, Sedwards, Sean
• Other Authors: Facultad de Matemática, Astronomía y Física Cordoba (FaMAF), Universidad Nacional de Córdoba Argentina, University of Twente Netherlands, Threat Analysis and Mitigation for Information Security (TAMIS), LANGAGE ET GÉNIE LOGICIEL (IRISA-D4), Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), CentraleSupélec-Télécom Bretagne-Université de Rennes 1 (UR1), Université de Rennes (UNIV-RENNES)-Université de Rennes (UNIV-RENNES)-Institut National de Recherche en Informatique et en Automatique (Inria)-École normale supérieure - Rennes (ENS Rennes)-Université de Bretagne Sud (UBS)-Centre National de la Recherche Scientifique (CNRS)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-CentraleSupélec-Télécom Bretagne-Université de Rennes 1 (UR1), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique (Inria)
• Format: Conference Object
• Language: English
• Published: HAL CCSD 2016
• Subjects: [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE]; [INFO.INFO-PF]Computer Science [cs]/Performance [cs.PF]; Iceland
• Online Access: https://hal.inria.fr/hal-01387362; https://hal.inria.fr/hal-01387362v2/document; https://hal.inria.fr/hal-01387362v2/file/paper.pdf

International audience 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.