Antichain Algorithms for Finite Automata

October 5, 2010

Jean-François Raskin


Antichain Algorithms for Finite Automata

Time:   11:00am
Location:   Amphitheatre H-1005

We present a general theory that exploits simulation relations on transition systems to obtain antichain algorithms for solving the reachability and repeated reachability problems. Antichains are more succinct than the sets of states manipulated by the traditional fixpoint algorithms. The theory justifies the correctness of the antichain algorithms, and applications such as the universality problem for finite automata illustrate efficiency improvements. Finally, we show that new and provably better antichain algorithms can be obtained for the emptiness problem of alternating automata over finite and infinite words.