@inproceedings{renault.13.lpar,
  author = {Etienne Renault and Alexandre Duret-Lutz and Fabrice
  	   Kordon and Denis Poitrenaud},
  title = {Three {SCC}-based Emptiness Checks for Generalized
  {B\"u}chi Automata},
  booktitle = {Proceedings of the 19th International Conference on
                  Logic for Programming, Artificial Intelligence, and
  Reasoning (LPAR'13)},
  editor = {Ken McMillan and Aart Middeldorp and Andrei Voronkov },
  year = {2013},
  month = dec,
  pages = {668--682},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {8312},
  abstract = { The automata-theoretic approach for the verification of
  linear time properties involves checking the emptiness of a
  B{\"u}chi automaton.  However generalized B{\"u}chi automata, with
  multiple acceptance sets, are preferred when verifying under weak
  fairness hypotheses.  Existing emptiness checks for which the
  complexity is independent of the number of acceptance sets are all
  based on the enumeration of Strongly Connected Components (SCCs).

  In this paper, we review the state of the art SCC enumeration
  algorithms to study how they can be turned into emptiness
  checks. This leads us to define two new emptiness check algorithms
  (one of them based on the Union Find data structure), introduce new
  optimizations, and show that one of these can be of benefit to a
  classic SCCs enumeration algorithm.  We have implemented all these
  variants to compare their relative performances and the overhead
  induced by the emptiness check compared to the corresponding SCCs
  enumeration algorithm.  Our experiments shows that these three
  algorithms are comparable.},
}