# A collection of recent research results on automata language inclusion testing

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.