Lightweight Statistical Model Checking in Nondeterministic Continuous Time

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

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

    7 Citations (Scopus)

    Abstract

    Lightweight scheduler sampling brings statistical model checking to nondeterministic formalisms with undiscounted properties, in constant memory. Its direct application to continuous-time models is rendered ineffective by their dense concrete state spaces and the need to consider continuous input for optimal decisions. In this paper we describe the challenges and state of the art in applying lightweight scheduler sampling to three continuous-time formalisms: After a review of recent work on exploiting discrete abstractions for probabilistic timed automata, we discuss scheduler sampling for Markov automata and apply it on two case studies. We provide further insights into the tradeoffs between scheduler classes for stochastic automata. Throughout, we present extended experiments and new visualisations of the distribution of schedulers.

    Original languageEnglish
    Title of host publicationProceedings of the 8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2018)
    EditorsTiziana Margaria, Bernhard Steffen
    PublisherSpringer
    Pages336-353
    Number of pages18
    Volume11245
    ISBN (Print)978-3-030-03420-7
    DOIs
    Publication statusPublished - 2018
    Event8th International Symposium, ISoLA 2018 - Royal Apollonia Beach Hotel, Limassol, Cyprus
    Duration: 5 Nov 20189 Nov 2018
    Conference number: 8
    http://www.isola-conference.org/isola2018/

    Publication series

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

    Conference

    Conference8th International Symposium, ISoLA 2018
    Abbreviated titleISoLA 2018
    CountryCyprus
    CityLimassol
    Period5/11/189/11/18
    Internet address

    Fingerprint Dive into the research topics of 'Lightweight Statistical Model Checking in Nondeterministic Continuous Time'. Together they form a unique fingerprint.

    Cite this