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

The complexity of showing language containment and equivalence between a Buchi automaton and a Muller or Streett automaton is given and a six by six matrix in which each row and column is associated with one of these types of automata is given.

Abstract

We consider the language inclusion and equivalence problems for six different types of ω-automata; Büchi, Muller, Rabin, Streett, the L-automata of Kurshan, and the ∀-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 inclusion between the ith type of automaton and the jth. Thus, for example, we give the complexity of showing language inclusion 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 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 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.