### Abstract

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.

Language | English |
---|---|

Title of host publication | Topics in Theoretical Computer Science |

Subtitle of host publication | Second IFIP WG 1.8 International Conference, TTCS 2017, Tehran, Iran, September 12-14, 2017, Proceedings |

Editors | Mohammad Reza Mousavi, Jiri Sgall |

Publisher | Springer |

Pages | xv-xvi |

Number of pages | 2 |

ISBN (Electronic) | 978-3-319-68953-1 |

ISBN (Print) | 978-3-319-68952-4 |

Publication status | Published - Nov 2017 |

Event | Second 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 2017 → 14 Sep 2017 Conference number: 2 http://ttcs.ir |

### Publication series

Name | Lecture Notes in Computer Science |
---|---|

Publisher | Springer |

Volume | 10608 |

ISSN (Print) | 0302-9743 |

ISSN (Electronic) | 1611-3349 |

### Conference

Conference | Second IFIP WG 1.8 International Conference on Topics in Theoretical Computer Science, TTCS 2017 |
---|---|

Abbreviated title | TTCS |

Country | Iran, Islamic Republic of |

City | Tehran |

Period | 12/09/17 → 14/09/17 |

Internet address |

### Fingerprint

### Keywords

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

### Cite this

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

}

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

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic

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

A2 - Mousavi, Mohammad Reza

A2 - Sgall, Jiri

PB - Springer

ER -