Parallel Model Checking Algorithms for Linear-Time Temporal Logic
From LRDE
- Authors
- Jiri Barnat, Vincent Bloemen, Alexandre Duret-Lutz, Alfons Laarman, Laure Petrucci, Jaco van de Pol, Etienne Renault
- Where
- Handbook of Parallel Constraint Reasoning
- Place
- Cham
- Type
- incollection
- Publisher
- Springer International Publishing
- Projects
- Spot
- Keywords
- Verification
- Date
- 2018-04-10
Abstract
Model checking is a fully automated, formal method for demonstrating absence of bugs in reactive systems. Herebugs are violations of properties in Linear-time Temporal Logic (LTL). A fundamental challenge to its application is the exponential explosion in the number of system states. The current chapter discusses the use of parallelism in order to overcome this challenge. We reiterate the textbook automata-theoretic approach, which reduces the model checking problem to the graph problem of finding cycles. We discuss several parallel algorithms that attack this problem in various ways, each with different characteristics: Depth-first search (DFS) based algorithms rely on heuristics for good parallelization, but exhibit a low complexity and good on-the-fly behavior. Breadth-first search (BFS) based approaches, on the other hand, offer good parallel scalability and support distributed parallelism. In addition, we present various simpler model checking tasks, which still solve a large and important subset of the LTL model checking problem, and show how these can be exploited to yield more efficient algorithms. In particular, we provide simplified DFS-based search algorithms and show that the BFS-based algorithms exhibit optimal runtimes in certain cases.
Documents
Bibtex (lrde.bib)
@InCollection{ barnat.18.hpcr, author = {Jiri Barnat and Vincent Bloemen and Alexandre Duret-Lutz and Alfons Laarman and Laure Petrucci and Jaco van de Pol and Etienne Renault}, editor = {Youssef Hamadi and Lakhdar Sais}, title = {Parallel Model Checking Algorithms for Linear-Time Temporal Logic}, booktitle = {Handbook of Parallel Constraint Reasoning}, year = {2018}, publisher = {Springer International Publishing}, address = {Cham}, chapter = 12, pages = {457--507}, abstract = {Model checking is a fully automated, formal method for demonstrating absence of bugs in reactive systems. Here, bugs are violations of properties in Linear-time Temporal Logic (LTL). A fundamental challenge to its application is the exponential explosion in the number of system states. The current chapter discusses the use of parallelism in order to overcome this challenge. We reiterate the textbook automata-theoretic approach, which reduces the model checking problem to the graph problem of finding cycles. We discuss several parallel algorithms that attack this problem in various ways, each with different characteristics: Depth-first search (DFS) based algorithms rely on heuristics for good parallelization, but exhibit a low complexity and good on-the-fly behavior. Breadth-first search (BFS) based approaches, on the other hand, offer good parallel scalability and support distributed parallelism. In addition, we present various simpler model checking tasks, which still solve a large and important subset of the LTL model checking problem, and show how these can be exploited to yield more efficient algorithms. In particular, we provide simplified DFS-based search algorithms and show that the BFS-based algorithms exhibit optimal runtimes in certain cases.}, isbn = {978-3-319-63516-3}, doi = {10.1007/978-3-319-63516-3_12} }