Parallel Model Checking Algorithms for Linear-Time Temporal Logic

Jiri Barnat, Vincent Bloemen, Alexandre Duret-Lutz, Alfons Laarman, Laure Petrucci, Jaco van de Pol, Etienne Renault

Research output: Chapter in Book/Report/Conference proceedingChapterAcademicpeer-review

1 Citation (Scopus)
22 Downloads (Pure)

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 how 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.
Original languageEnglish
Title of host publicationHandbook of Parallel Constraint Reasoning
EditorsYoussef Hamadi, Lakhdar Sais
Place of PublicationCham
PublisherSpringer
Chapter12
Pages457-507
Number of pages51
ISBN (Electronic)978-3-319-63516-3
ISBN (Print)978-3-319-63515-6
DOIs
Publication statusPublished - 2018

Fingerprint

Temporal logic
Model checking
Temporal Logic
Model Checking
Linear Time
Breadth-first Search
Depth-first Search
Parallelism
Reactive Systems
Formal methods
Textbooks
Formal Methods
Parallel algorithms
Parallelization
Explosion
Parallel Algorithms
Low Complexity
Search Algorithm
Explosions
Automata

Keywords

  • LTL model checking
  • nested depth-first search
  • strongly connected components
  • NDFS
  • SCC-detection
  • Büchi emptiness
  • TGBA

Cite this

Barnat, J., Bloemen, V., Duret-Lutz, A., Laarman, A., Petrucci, L., van de Pol, J., & Renault, E. (2018). Parallel Model Checking Algorithms for Linear-Time Temporal Logic. In Y. Hamadi, & L. Sais (Eds.), Handbook of Parallel Constraint Reasoning (pp. 457-507). Cham: Springer. https://doi.org/10.1007/978-3-319-63516-3_12
Barnat, Jiri ; Bloemen, Vincent ; Duret-Lutz, Alexandre ; Laarman, Alfons ; Petrucci, Laure ; van de Pol, Jaco ; Renault, Etienne. / Parallel Model Checking Algorithms for Linear-Time Temporal Logic. Handbook of Parallel Constraint Reasoning. editor / Youssef Hamadi ; Lakhdar Sais. Cham : Springer, 2018. pp. 457-507
@inbook{68f894f12e5c4b1e8f4d04739f68f673,
title = "Parallel Model Checking Algorithms for Linear-Time Temporal Logic",
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 how 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.",
keywords = "LTL model checking, nested depth-first search, strongly connected components, NDFS, SCC-detection, B{\"u}chi emptiness, TGBA",
author = "Jiri Barnat and Vincent Bloemen and Alexandre Duret-Lutz and Alfons Laarman and Laure Petrucci and {van de Pol}, Jaco and Etienne Renault",
year = "2018",
doi = "10.1007/978-3-319-63516-3_12",
language = "English",
isbn = "978-3-319-63515-6",
pages = "457--507",
editor = "Youssef Hamadi and Lakhdar Sais",
booktitle = "Handbook of Parallel Constraint Reasoning",
publisher = "Springer",

}

Barnat, J, Bloemen, V, Duret-Lutz, A, Laarman, A, Petrucci, L, van de Pol, J & Renault, E 2018, Parallel Model Checking Algorithms for Linear-Time Temporal Logic. in Y Hamadi & L Sais (eds), Handbook of Parallel Constraint Reasoning. Springer, Cham, pp. 457-507. https://doi.org/10.1007/978-3-319-63516-3_12

Parallel Model Checking Algorithms for Linear-Time Temporal Logic. / Barnat, Jiri; Bloemen, Vincent; Duret-Lutz, Alexandre; Laarman, Alfons; Petrucci, Laure; van de Pol, Jaco; Renault, Etienne.

Handbook of Parallel Constraint Reasoning. ed. / Youssef Hamadi; Lakhdar Sais. Cham : Springer, 2018. p. 457-507.

Research output: Chapter in Book/Report/Conference proceedingChapterAcademicpeer-review

TY - CHAP

T1 - Parallel Model Checking Algorithms for Linear-Time Temporal Logic

AU - Barnat, Jiri

AU - Bloemen, Vincent

AU - Duret-Lutz, Alexandre

AU - Laarman, Alfons

AU - Petrucci, Laure

AU - van de Pol, Jaco

AU - Renault, Etienne

PY - 2018

Y1 - 2018

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

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

KW - LTL model checking

KW - nested depth-first search

KW - strongly connected components

KW - NDFS

KW - SCC-detection

KW - Büchi emptiness

KW - TGBA

U2 - 10.1007/978-3-319-63516-3_12

DO - 10.1007/978-3-319-63516-3_12

M3 - Chapter

SN - 978-3-319-63515-6

SP - 457

EP - 507

BT - Handbook of Parallel Constraint Reasoning

A2 - Hamadi, Youssef

A2 - Sais, Lakhdar

PB - Springer

CY - Cham

ER -

Barnat J, Bloemen V, Duret-Lutz A, Laarman A, Petrucci L, van de Pol J et al. Parallel Model Checking Algorithms for Linear-Time Temporal Logic. In Hamadi Y, Sais L, editors, Handbook of Parallel Constraint Reasoning. Cham: Springer. 2018. p. 457-507 https://doi.org/10.1007/978-3-319-63516-3_12