Statistical Approximation of Optimal Schedulers for Probabilistic Timed Automata

Pedro R. D'Argenio, Arnd Hartmanns, Axel Legay, Sean Sedwards

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    10 Citations (Scopus)
    93 Downloads (Pure)

    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 languageEnglish
    Title of host publicationProceedings of the 12th International Conference on Integrated Formal Methods (IFM 2016)
    Place of PublicationCham
    PublisherSpringer
    Pages99-114
    Number of pages16
    ISBN (Print)978-3-319-33692-3
    DOIs
    Publication statusPublished - Jun 2016
    Event12th International Conference on integrated Formal Methods 2016 - Reykjavik Iceland, Reykjavik, Iceland
    Duration: 1 Jun 20165 Jun 2016
    Conference number: 12

    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

    Keywords

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

    Fingerprint Dive into the research topics of 'Statistical Approximation of Optimal Schedulers for Probabilistic Timed Automata'. Together they form a unique fingerprint.

    Cite this