The automata language inclusion problem is important in many application domains, e.g., formal verification. Many verification problems can be formulated as a language inclusion problem. For example, one may describe the actual behaviors of an implementation in an automaton A and all of the behaviors permitted by the specification in another automaton B. Then, the problem of whether the implementation meets the specification is equivalent to the problem L(A)⊆ L(B).

In program verification, language inclusion of Buchi Automata, Finite Automata and Tree Automata are most studied. Below we list research projects on these topics

1. Buchi automata
   1. Ramsey-based Approach Using Simulation Subsumption
   2. Ramsey-based Approach Using Basic Subsumption
   3. Rank-based Approach
   4. Safra-based Approach
   5. Performance comparison of Ramsey and Rank
2. Finite State Automata
3. Tree Automata