Greetings,
We are pleased to announce that the following chapter has been published in
Handbook of Parallel Constraint Reasoning (Springer). Please find the title and
abstract below.
Title and corresponding authors:
"Parallel Model Checking Algorithms for Linear-Time Temporal Logic"
Jiri Barnat (1), Vincent Bloemen (2), Alexandre Duret-Lutz (3), Alfons Laarman (4),
Laure Petrucci(5), Jaco van de Pol (2), and Etienne Renault (3)
(1) Masaryk University, Brno, Czech Republic
(2) University of Twente, Enschede, The Netherlands
(3) LRDE, Epita, Paris, France
(4) Leiden University, Leiden, The Netherlands
(5) LIPN, CNRS, Paris, France
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.
More information at :
https://www.lrde.epita.fr/wiki/Publications/barnat.18.hpcr
<https://www.lrde.epita.fr/wiki/Publications/barnat.18.hpcr>