Simulation relations for alternating Büchi automata (Q557801)

The authors adapt the technique for minimalization of the nondeterministic Büchi automata to alternating Büchi automata. Based on the same simple game the authors define three types of simulation relations (direct, delayed and fair) for alternating Büchi automata and show that all these simulations can be used for checking language containment. Two new quotients (minimax and semi-elective) are presented and it is shown that the quotients preserve the languages recognized. It is shown that the simulation relations defined by the authors are compatible with standard translation of alternating Büchi automata to nondeterministic Büchi automata, due to Miyano and Hayashi. At the end an efficient algorithm for computing the simulation relations is presented. This algorithm has a lower time complexity than other existing algorithms.