@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}
}