Seventh International Conference on Application of Concurrency to System Design (ACSD 2007)
Emptiness Check of Powerset Buchi Automata using Inclusion Tests
Bratislava, Slovak Republic
July 10-July 13
ISBN: 0-7695-2902-X
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.
Citation:
Souheib Baarir, Alexandre Duret-Lutz, "Emptiness Check of Powerset Buchi Automata using Inclusion Tests," acsd, pp.41-50, Seventh International Conference on Application of Concurrency to System Design (ACSD 2007), 2007