Emptiness Check of Powerset Buchi Automata using Inclusion Tests
Souheib Baarir, Alexandre Duret-Lutz · Proceedings · 2007
We introduce two emptiness checks for buchi automata whose states represent sets that may include each other. The first is equivalent to a traditional emptiness check but uses inclusion tests to direct the on-the-fly construction of the automaton. The second is impressively faster but may return false negatives. We illustrate and benchmark the improvement on a symmetry-based reduction.