A unified approach for showing language containment and equivalence between various types of [omega]-automata

Abstract: "We consider the language containment and equivalence problems for six different types of [omega]-automata: Büchi, Muller, Rabin, Streett, the L-automata of Kurshan, and the [universal quanitifier] automata of Manna and Pnueli. We give a six by six matrix in which each row and column is associated with one of these types of automata. The entry in the i[superscript th] column is the complexity of showing containment between the i[superscript th] type of automation and j[superscript th]. Thus, for example, we give the complexity of showing language containment and equivalence between a Büchi automation and a Muller or Streett automation. Our results are obtained by a uniform method that associates a formula of the computation tree logic CTL* with each type of automation.Our algorithms use a model checking procedure for the logic with the formulas obtained from the automata. The results of our paper are important for verification of finite state concurrent systems with fairness constraints. A natural way of reasoning about such systems is to model the finite state program by one [omega]-automation and its specification by another.