We are pleased to inform you that the following paper has been accepted in the 19th International
Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR). Please find the
title and abstract below.
The automata-theoretic approach for the verification of linear time
properties involves checking the emptiness of a Büchi automaton.
However generalized Bü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.