Parallel Algorithms for Model Checking

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

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.
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
StatePublished - 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

Fingerprint

Model checking
Parallel algorithms
Binary decision diagrams
Trees (mathematics)
Automata theory
Temporal logic
Data structures
Scalability
Servers
Decomposition
Hardware
Data storage equipment

Keywords

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

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.
van de Pol, Jaco. / Parallel Algorithms for Model Checking. Topics in Theoretical Computer Science: Second IFIP WG 1.8 International Conference, TTCS 2017, Tehran, Iran, September 12-14, 2017, Proceedings. editor / Mohammad Reza Mousavi ; Jiri Sgall. Springer, 2017. pp. xv-xvi (Lecture Notes in Computer Science).
@inproceedings{d4cd2f40ecbb446d8d57abd4449e944b,
title = "Parallel Algorithms for Model Checking",
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{\"u}chi automata. LTL model checking can be reduced to the emptiness problem of B{\"u}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{\"u}chi and Rabin automata. SCCs are also useful for model checking with fairness, probabilistic model checking, and implementing partial-order reduction.",
keywords = "parallel model checking, decision diagrams, nested depth-first search, rabin automata, strongly connected components, lock-free hashtables",
author = "{van de Pol}, Jaco",
year = "2017",
month = "11",
language = "English",
isbn = "978-3-319-68952-4",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "xv--xvi",
editor = "Mousavi, {Mohammad Reza} and Jiri Sgall",
booktitle = "Topics in Theoretical Computer Science",

}

van de Pol, J 2017, Parallel Algorithms for Model Checking. in MR 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. Lecture Notes in Computer Science, vol. 10608, Springer, pp. xv-xvi, Second IFIP WG 1.8 International Conference on Topics in Theoretical Computer Science, TTCS 2017, Tehran, Iran, Islamic Republic of, 12/09/17.

Parallel Algorithms for Model Checking. / van de Pol, Jaco.

Topics in Theoretical Computer Science: Second IFIP WG 1.8 International Conference, TTCS 2017, Tehran, Iran, September 12-14, 2017, Proceedings. ed. / Mohammad Reza Mousavi; Jiri Sgall. Springer, 2017. p. xv-xvi (Lecture Notes in Computer Science; Vol. 10608).

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

TY - GEN

T1 - Parallel Algorithms for Model Checking

AU - van de Pol,Jaco

PY - 2017/11

Y1 - 2017/11

N2 - 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.

AB - 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.

KW - parallel model checking

KW - decision diagrams

KW - nested depth-first search

KW - rabin automata

KW - strongly connected components

KW - lock-free hashtables

UR - http://10.1007/978-3-319-68953-1

M3 - Conference contribution

SN - 978-3-319-68952-4

T3 - Lecture Notes in Computer Science

SP - xv-xvi

BT - Topics in Theoretical Computer Science

PB - Springer

ER -

van de Pol J. Parallel Algorithms for Model Checking. In Mousavi MR, Sgall J, editors, Topics in Theoretical Computer Science: Second IFIP WG 1.8 International Conference, TTCS 2017, Tehran, Iran, September 12-14, 2017, Proceedings. Springer. 2017. p. xv-xvi. (Lecture Notes in Computer Science).