A UNIFIED APPROACH FOR SHOWING LANGUAGE INCLUSION AND EQUIVALENCE BETWEEN VARIOUS TYPES OF OMEGA-AUTOMATA

We consider the language inclusion and equivalence problems for six di fferent types of omega-automata; Buchi, Muller, Rabin, Streett, the L- automata of Kurshan, and the for-all-automata of Manna and Pnueli. We give a six by six matrix in which each row and column is associated wi th one of these types of automata. The entry in the ith row and jth co lumn is the complexity of showing inclusion between the ith type of au tomaton and the jth. Thus, for example, we give the complexity of show ing language inclusion and equivalence between a Buchi automaton and a Muller or Streett automaton. Our results are obtained by a uniform me thod that associates a formula of the computation tree logic CTL with each type of automaton. Our algorithms use a model checking procedure for the logic with the formulas obtained from the automata. The resul ts of our paper are important for verification of finite state concurr ent systems with fairness constraints. A natural way of reasoning abou t such systems is to model the finite state program by one omega-autom aton and its specification by another.