zbMATH — the first resource for mathematics

Parallel explicit model checking for generalized Büchi automata. (English) Zbl 1420.68137
Baier, Christel (ed.) et al., Tools and algorithms for the construction and analysis of systems. 21st international conference, TACAS 2015, held as part of the European joint conferences on theory and practice of software, ETAPS 2015, London, UK, April 11–18, 2015. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 9035, 613-627 (2015).
Summary: 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.
For the entire collection see [Zbl 1360.68006].

68Q60 Specification and verification (program logics, model checking, etc.)
68Q45 Formal languages and automata
Full Text: DOI