Efficient simulation-based verification of probabilistic timed automata

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

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

    5 Citations (Scopus)

    Abstract

    Probabilistic timed automata are a formal model for real-time systems with discrete probabilistic and nondeterministic choices. To overcome the state space explosion problem of exhaustive verification, a symbolic simulation-based approach that soundly treats nondeterminism to approximate maximum and minimum reachability probabilities has recently become available. Its use of difference-bound matrices to handle continuous real time however leads to poor performance: most operations are cubic or even exponential in the number of clock variables. In this paper, we propose a novel region-based approach and data structure that reduce the complexity of all operations to being linear. It relies on a particular mapping between symbolic regions and concrete representative valuations. Using an implementation within the MODEST TOOLSET, we show that the new approach is not only easier to implement, but indeed significantly outperforms all current alternatives on standard benchmark models.
    Original languageEnglish
    Title of host publicationProceedings of the 2017 Winter Simulation Conference
    EditorsW.K.V. Chan, A. D’Ambrogio, G. Zacharewicz, N. Mustafee, G. Wainer, E. Page
    PublisherIEEE
    Pages1419-1430
    Number of pages12
    ISBN (Electronic)978-1-5386-3428-8
    ISBN (Print)978-1-5386-3430-1
    DOIs
    Publication statusPublished - 2017
    Event2017 Winter Simulation Conference - Las Vegas, United States
    Duration: 3 Dec 20176 Dec 2017

    Conference

    Conference2017 Winter Simulation Conference
    Abbreviated titleWSC 2017
    CountryUnited States
    CityLas Vegas
    Period3/12/176/12/17

    Fingerprint Dive into the research topics of 'Efficient simulation-based verification of probabilistic timed automata'. Together they form a unique fingerprint.

    Cite this