Parallel Algorithms for Model Checking

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademic

    Abstract

    Model checking is an automated verification procedure, which checks that a model of a system satisfies certain properties. These properties are typically expressed in some temporal logic, like LTL and CTL. Algorithms for LTL model checking (linear time logic) are based on automata theory and graph algorithms, while algorithms for CTL (computation tree logic) are based on fixed-point computations and set operations.

    The basic model checking procedures examine the state space of a system exhaustively, which grows exponentially in the number of variables or parallel components. Scalability of model checking is achieved by clever abstractions (for instance counter-example guided abstraction refinement), clever algorithms (for instance partial-order reduction), clever data-structures (for instance binary decision diagrams) and, finally, clever use of hardware resources, for instance algorithms for distributed and multi-core computers.

    This invited lecture will provide a number of highlights of our research in the last decade on high-performance model checking, as it is implemented in the open source LTSmin tool set, focusing on the algorithms and datastructures in its multi-core tools.

    A lock-free, scalable hash-table maintains a globally shared set of already visited state vectors. Using this, parallel workers can semi-independently explore different parts of the state space, still ensuring that every state will be explored exactly once. Our implementation proved to scale linearly on tens of processors.

    Parallel algorithms for NDFS. Nested Depth-First Search is a linear-time algorithm to detect accepting cycles in Büchi automata. LTL model checking can be reduced to the emptiness problem of Büchi automata, i.e. the absence of accepting cycles. We introduced a parallel version of this algorithm, despite the fact that Depth-First Search is hard to parallelize. Our multi-core implementation is compatible with important state space reduction techniques, in particular state compression and partial-order reduction and generalizes to timed automata.

    A multi-core library for Decision Diagrams, called Sylvan. Binary Decision Diagrams (BDD) have been introduced as concise representations of sets of Boolean vectors. The CTL model checking operations can be expressed directly on the BDD representation. Sylvan provides a parallel implementation of BDD operations for shared-memory, multi-core processors. We also provided successful experiments on distributed BDDs over a cluster of multi-core computer servers. Besides BDDs, Sylvan also supports Multi-way and Multi-terminal Decision Diagrams.

    Multi-core algorithms to detect Strongly Connected Components. An alternative model-checking algorithm is based on the decomposition and analysis of Strongly Connected Components (SCCs). We have implemented a parallel version of Dijkstra’s SCC algorithm. It forms the basis of model checking LTL using generalized Büchi and Rabin automata. SCCs are also useful for model checking with fairness, probabilistic model checking, and implementing partial-order reduction.
    Original languageEnglish
    Title of host publicationTopics in Theoretical Computer Science
    Subtitle of host publicationSecond IFIP WG 1.8 International Conference, TTCS 2017, Tehran, Iran, September 12-14, 2017, Proceedings
    EditorsMohammad Reza Mousavi, Jiri Sgall
    PublisherSpringer
    Pagesxv-xvi
    Number of pages2
    ISBN (Electronic)978-3-319-68953-1
    ISBN (Print)978-3-319-68952-4
    Publication statusPublished - Nov 2017
    EventSecond IFIP WG 1.8 International Conference on Topics in Theoretical Computer Science, TTCS 2017 - Institute for Research in Fundamental Sciences (IPM), Tehran, Iran, Islamic Republic of
    Duration: 12 Sep 201714 Sep 2017
    Conference number: 2
    http://ttcs.ir

    Publication series

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

    Conference

    ConferenceSecond IFIP WG 1.8 International Conference on Topics in Theoretical Computer Science, TTCS 2017
    Abbreviated titleTTCS
    CountryIran, Islamic Republic of
    CityTehran
    Period12/09/1714/09/17
    Internet address

    Keywords

    • parallel model checking
    • decision diagrams
    • nested depth-first search
    • rabin automata
    • strongly connected components
    • lock-free hashtables

    Fingerprint Dive into the research topics of 'Parallel Algorithms for Model Checking'. Together they form a unique fingerprint.

  • Cite this

    van de Pol, J. (2017). Parallel Algorithms for Model Checking. In M. R. Mousavi, & J. Sgall (Eds.), Topics in Theoretical Computer Science: Second IFIP WG 1.8 International Conference, TTCS 2017, Tehran, Iran, September 12-14, 2017, Proceedings (pp. xv-xvi). (Lecture Notes in Computer Science; Vol. 10608). Springer.