Parallel Explicit Model Checking for Generalized Büchi Automata

From LRDE

Revision as of 17:52, 4 January 2018 by Bot (talk | contribs)

Abstract

We present new parallel emptiness checks for LTL model checking. Unlike existing parallel emptiness checks, these are based on an SCC enumeration, support generalized Buchi acceptance, and require no synchronization points nor repair procedures. A salient feature of our algorithms is the use of a global union-find data structure in which multiple threads share structural information about the automaton being checked. Our prototype implementation has encouraging performances: the new emptiness checks have better speedup than existing algorithms in half of our experiments.

Documents

Bibtex (lrde.bib)

@InProceedings{	  renault.15.tacas,
  author	= {Etienne Renault and Alexandre Duret-Lutz and Fabrice
		  Kordon and Denis Poitrenaud},
  title		= {Parallel Explicit Model Checking for Generalized {B\"u}chi
		  Automata},
  booktitle	= {Proceedings of the 19th International Conference on Tools
		  and Algorithms for the Construction and Analysis of Systems
		  (TACAS'15)},
  editor	= {Christel Baier and Cesare Tinelli},
  year		= 2015,
  month		= apr,
  pages		= {613--627},
  publisher	= {Springer},
  series	= {Lecture Notes in Computer Science},
  volume	= 9035,
  abstract	= {We present new parallel emptiness checks for LTL model
		  checking. Unlike existing parallel emptiness checks, these
		  are based on an SCC enumeration, support generalized Buchi
		  acceptance, and require no synchronization points nor
		  repair procedures. A salient feature of our algorithms is
		  the use of a global union-find data structure in which
		  multiple threads share structural information about the
		  automaton being checked. Our prototype implementation has
		  encouraging performances: the new emptiness checks have
		  better speedup than existing algorithms in half of our
		  experiments.}
}