Parallel Model Checking of ω-Automata

Vincent Bloemen

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

    32 Downloads (Pure)

    Abstract

    Specifications for non-terminating reactive systems are described by ω-regular properties. Such properties can be translated in various types of automata, e.g. Büchi, Rabin, and Parity. A model checker can then check for language containment and determine whether the system meets the specification. Checking these automata becomes more complex when introducing probabilities and/or an adversary, e.g. the uncontrollable environment, to the automaton. Parallel algorithms have become crucial for fully utilizing current hardware systems. With respect to model checking we therefore focus on designing scalable parallel algorithms for emptiness checking. This research focuses on designing and improving parallel graph searching algorithms for emptiness checking on various types of ω-automata. As a basis, we developed a scalable multi-core on-the-fly algorithm for the detection of strongly connected components (SCCs). Our aim is to contribute to the state-of-the-art techniques in parallel model checking, based on both theoretical complexity analysis and empirical studies on suitable benchmarks.
    Original languageEnglish
    Title of host publicationProceedings of the Formal Methods 2016 Doctoral Symposium co-located with 21st International Symposium on Formal Methods (FM 2016)
    EditorsAndrew Butterfield, Matteo Rossi
    Place of PublicationAachen
    PublisherCEUR
    Pages1
    Number of pages6
    Publication statusPublished - 8 Nov 2016
    EventFormal Methods 2016 Doctoral Symposium co-located with 21st International Symposium on Formal Methods (FM 2016) - Limassol, Cyprus, Limassol, Cyprus
    Duration: 8 Nov 20168 Nov 2016

    Publication series

    Name
    PublisherCEUR Workshop Proceedings
    Volume1744
    ISSN (Print)1613-0073

    Conference

    ConferenceFormal Methods 2016 Doctoral Symposium co-located with 21st International Symposium on Formal Methods (FM 2016)
    Abbreviated titleFM-DS 2016
    CountryCyprus
    CityLimassol
    Period8/11/168/11/16
    Other8 Nov 2016

    Keywords

    • EWI-27452
    • Büchi
    • Model Checking
    • Multi-Core
    • IR-102923
    • LTL
    • Parallel
    • Parity
    • METIS-320899
    • Rabin

    Fingerprint Dive into the research topics of 'Parallel Model Checking of ω-Automata'. Together they form a unique fingerprint.

    Cite this