Statistical Approximation of Optimal Schedulers for Probabilistic Timed Automata
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 te...
Main Authors: | , , , |
---|---|
Other Authors: | , , , , , , , , , , |
Format: | Conference Object |
Language: | English |
Published: |
HAL CCSD
2016
|
Subjects: | |
Online Access: | https://hal.inria.fr/hal-01387362 https://hal.inria.fr/hal-01387362v2/document https://hal.inria.fr/hal-01387362v2/file/paper.pdf |
id |
ftunivrennes1hal:oai:HAL:hal-01387362v2 |
---|---|
record_format |
openpolar |
spelling |
ftunivrennes1hal:oai:HAL:hal-01387362v2 2023-05-15T16:49:54+02:00 Statistical Approximation of Optimal Schedulers for Probabilistic Timed Automata d'Argenio, Pedro, Hartmanns, Arnd Legay, Axel Sedwards, Sean Facultad de Matemática, Astronomía y Física Cordoba (FaMAF) Universidad Nacional de Córdoba Argentina University of Twente Threat Analysis and Mitigation for Information Security (TAMIS) Inria Rennes – Bretagne Atlantique Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-LANGAGE ET GÉNIE LOGICIEL (IRISA-D4) Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA) Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes) Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes) Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA) Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS) Reykjavik, Iceland 2016-06-01 https://hal.inria.fr/hal-01387362 https://hal.inria.fr/hal-01387362v2/document https://hal.inria.fr/hal-01387362v2/file/paper.pdf en eng HAL CCSD hal-01387362 https://hal.inria.fr/hal-01387362 https://hal.inria.fr/hal-01387362v2/document https://hal.inria.fr/hal-01387362v2/file/paper.pdf info:eu-repo/semantics/OpenAccess Integrated Formal Methods https://hal.inria.fr/hal-01387362 Integrated Formal Methods, Jun 2016, Reykjavik, Iceland. pp.99-114 [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE] [INFO.INFO-PF]Computer Science [cs]/Performance [cs.PF] info:eu-repo/semantics/conferenceObject Conference papers 2016 ftunivrennes1hal 2023-03-22T00:14:21Z 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. Conference Object Iceland Université de Rennes 1: Publications scientifiques (HAL) |
institution |
Open Polar |
collection |
Université de Rennes 1: Publications scientifiques (HAL) |
op_collection_id |
ftunivrennes1hal |
language |
English |
topic |
[INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE] [INFO.INFO-PF]Computer Science [cs]/Performance [cs.PF] |
spellingShingle |
[INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE] [INFO.INFO-PF]Computer Science [cs]/Performance [cs.PF] d'Argenio, Pedro, Hartmanns, Arnd Legay, Axel Sedwards, Sean Statistical Approximation of Optimal Schedulers for Probabilistic Timed Automata |
topic_facet |
[INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE] [INFO.INFO-PF]Computer Science [cs]/Performance [cs.PF] |
description |
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. |
author2 |
Facultad de Matemática, Astronomía y Física Cordoba (FaMAF) Universidad Nacional de Córdoba Argentina University of Twente Threat Analysis and Mitigation for Information Security (TAMIS) Inria Rennes – Bretagne Atlantique Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-LANGAGE ET GÉNIE LOGICIEL (IRISA-D4) Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA) Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes) Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes) Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA) Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS) |
format |
Conference Object |
author |
d'Argenio, Pedro, Hartmanns, Arnd Legay, Axel Sedwards, Sean |
author_facet |
d'Argenio, Pedro, Hartmanns, Arnd Legay, Axel Sedwards, Sean |
author_sort |
d'Argenio, Pedro, |
title |
Statistical Approximation of Optimal Schedulers for Probabilistic Timed Automata |
title_short |
Statistical Approximation of Optimal Schedulers for Probabilistic Timed Automata |
title_full |
Statistical Approximation of Optimal Schedulers for Probabilistic Timed Automata |
title_fullStr |
Statistical Approximation of Optimal Schedulers for Probabilistic Timed Automata |
title_full_unstemmed |
Statistical Approximation of Optimal Schedulers for Probabilistic Timed Automata |
title_sort |
statistical approximation of optimal schedulers for probabilistic timed automata |
publisher |
HAL CCSD |
publishDate |
2016 |
url |
https://hal.inria.fr/hal-01387362 https://hal.inria.fr/hal-01387362v2/document https://hal.inria.fr/hal-01387362v2/file/paper.pdf |
op_coverage |
Reykjavik, Iceland |
genre |
Iceland |
genre_facet |
Iceland |
op_source |
Integrated Formal Methods https://hal.inria.fr/hal-01387362 Integrated Formal Methods, Jun 2016, Reykjavik, Iceland. pp.99-114 |
op_relation |
hal-01387362 https://hal.inria.fr/hal-01387362 https://hal.inria.fr/hal-01387362v2/document https://hal.inria.fr/hal-01387362v2/file/paper.pdf |
op_rights |
info:eu-repo/semantics/OpenAccess |
_version_ |
1766040072734375936 |