======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. 

{{ :incprob.jpg?nolink |An Example of Language Inclusion Problems}}\\
{{:Slides2014.pdf|Slides of an overview talk on language inclusion and automata minimization.}}

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

  - **[[ramseySimsub|Buchi automata]]**
  - **[[NFASimsub|Finite-word Automata]]**
  - **[[TASimsub|Tree Automata]]**