We are pleased to announce that the following paper has been accepted in the 21st
International Conference on Tools and Algorithms for the Construction and Analysis of
Systems (TACAS). Find the title and abstract below.
Title and corresponding authors:
Parallel Explicit Model Checking for Generalized Büchi Automata
Etienne Renault(1,2,3), Alexandre Duret-Lutz(1), Fabrice Kordon(2,3) and Denis
Poitrenaud(3,4)
(1) LRDE, EPITA, Kremlin-Bicêtre, France
(2) Sorbonne Universités, UPMC Univ. Paris 06, France
(3) CNRS UMR 7606, LIP6, F-75005 Paris, France
(4) Université Paris Descartes, Paris, France
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 Büchi 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.
Show replies by date