A unified approach for showing language containment and equivalence between various types of ω-automata

Abstract

We consider the language containment and equivalence problems for six different types of ω-automata: Büchi, Muller, Rabin, Streett, the L-automata of Kurshan, and the V-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 ith row and jth column is the complexity of showing containment between the ith type of automaton and the jth. Thus, for example, we give the complexity of showing language containment and equivalence between a Büchi automaton and a Muller or Streett automaton. Our results are obtained by a uniform method that associates a formula of the 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 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 ω-automaton and its specification by another.