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).
Since we consider general nondeterministic automata, language inclusion/equivalence checking is computationally hard (PSPACE-complete for word automata and EXPTIME-complete for trees). Still, fairly large instances can be solved with the right techniques. The goal is to make similar progress on solving PSPACE-hard automata problems, as the progress made by SAT-solvers on NP-hard logic problems.
In program verification, language inclusion of Buchi Automata, Finite Automata and Tree Automata are most studied. Below we list research projects on these topics.