Statistical Approximation of Optimal Schedulers for Probabilistic Timed Automata

P.R. d' Argenio, Arnd Hartmanns, A. Legay, S. Sedwards

  • 4 Citations

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.
Original languageUndefined
Title of host publicationProceedings of the 12th International Conference on Integrated Formal Methods (IFM 2016)
Place of PublicationBerlin
PublisherSpringer Verlag
Pages99-114
Number of pages16
ISBN (Print)978-3-319-33692-3
DOIs
StatePublished - Jun 2016
Event12th International Conference on integrated Formal Methods 2016 - Reykjavik, Iceland

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Verlag
Volume9681
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference12th International Conference on integrated Formal Methods 2016
Abbreviated titleiFM 2016
CountryIceland
CityReykjavik
Period1/06/165/06/16

Fingerprint

Model checking
Explosions
Scalability
Numerical models
Sampling

Keywords

  • METIS-317210
  • EWI-27044
  • IR-100708

Cite this

d' Argenio, P. R., Hartmanns, A., Legay, A., & Sedwards, S. (2016). Statistical Approximation of Optimal Schedulers for Probabilistic Timed Automata. In Proceedings of the 12th International Conference on Integrated Formal Methods (IFM 2016) (pp. 99-114). (Lecture Notes in Computer Science; Vol. 9681). Berlin: Springer Verlag. DOI: 10.1007/978-3-319-33693-0_7

d' Argenio, P.R.; Hartmanns, Arnd; Legay, A.; Sedwards, S. / Statistical Approximation of Optimal Schedulers for Probabilistic Timed Automata.

Proceedings of the 12th International Conference on Integrated Formal Methods (IFM 2016). Berlin : Springer Verlag, 2016. p. 99-114 (Lecture Notes in Computer Science; Vol. 9681).

Research output: Scientific - peer-reviewConference contribution

@inbook{19366aa08dfb4785a6531814c5e1df25,
title = "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.",
keywords = "METIS-317210, EWI-27044, IR-100708",
author = "{d' Argenio}, P.R. and Arnd Hartmanns and A. Legay and S. Sedwards",
note = "eemcs-eprint-27044",
year = "2016",
month = "6",
doi = "10.1007/978-3-319-33693-0_7",
isbn = "978-3-319-33692-3",
series = "Lecture Notes in Computer Science",
publisher = "Springer Verlag",
pages = "99--114",
booktitle = "Proceedings of the 12th International Conference on Integrated Formal Methods (IFM 2016)",

}

d' Argenio, PR, Hartmanns, A, Legay, A & Sedwards, S 2016, Statistical Approximation of Optimal Schedulers for Probabilistic Timed Automata. in Proceedings of the 12th International Conference on Integrated Formal Methods (IFM 2016). Lecture Notes in Computer Science, vol. 9681, Springer Verlag, Berlin, pp. 99-114, 12th International Conference on integrated Formal Methods 2016, Reykjavik, Iceland, 1-5 June. DOI: 10.1007/978-3-319-33693-0_7

Statistical Approximation of Optimal Schedulers for Probabilistic Timed Automata. / d' Argenio, P.R.; Hartmanns, Arnd; Legay, A.; Sedwards, S.

Proceedings of the 12th International Conference on Integrated Formal Methods (IFM 2016). Berlin : Springer Verlag, 2016. p. 99-114 (Lecture Notes in Computer Science; Vol. 9681).

Research output: Scientific - peer-reviewConference contribution

TY - CHAP

T1 - Statistical Approximation of Optimal Schedulers for Probabilistic Timed Automata

AU - d' Argenio,P.R.

AU - Hartmanns,Arnd

AU - Legay,A.

AU - Sedwards,S.

N1 - eemcs-eprint-27044

PY - 2016/6

Y1 - 2016/6

N2 - 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.

AB - 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.

KW - METIS-317210

KW - EWI-27044

KW - IR-100708

U2 - 10.1007/978-3-319-33693-0_7

DO - 10.1007/978-3-319-33693-0_7

M3 - Conference contribution

SN - 978-3-319-33692-3

T3 - Lecture Notes in Computer Science

SP - 99

EP - 114

BT - Proceedings of the 12th International Conference on Integrated Formal Methods (IFM 2016)

PB - Springer Verlag

ER -

d' Argenio PR, Hartmanns A, Legay A, Sedwards S. Statistical Approximation of Optimal Schedulers for Probabilistic Timed Automata. In Proceedings of the 12th International Conference on Integrated Formal Methods (IFM 2016). Berlin: Springer Verlag. 2016. p. 99-114. (Lecture Notes in Computer Science). Available from, DOI: 10.1007/978-3-319-33693-0_7