# Solving PSPACE-complete Problems in Automata Theory

Develop algorithms and tools for solving most practical instances of PSPACE-complete problems in automata theory, e.g., language inclusion, equivalence and universality (see www.languageinclusion.org).

Finite automata are a fundamental and ubiquitous building block in
many areas of computer science. They can describe and manipulate
infinite (but regular) sets of objects like finite and infinite length
words, and trees with finite and infinite depth. Applications include
reasoning about patterns in database queries, modeling and simulation
of controllers and reactive systems, analyzing DNA sequences, model
checking and formal software verification, natural language processing,
learning theory, and algorithmic decision procedures for logical
theories. Central automata problems like language inclusion, equivalence
and universality are PSPACE-complete. However, such complexity bounds
on the worst-case scenario are not necessarily an obstacle to practical
applications. In recent years, advanced methods have been developed
which can solve many practical instances of other computationally hard
problems, notably the satisfiability problem for boolean formulae (SAT).
The SAT problem is complete for the complexity class NP (which is hard
but still easier than PSPACE), and modern tools can solve highly
non-trivial cases arising in practical applications, e.g., hardware
verification. More recently, similar progress is being made on
PSPACE-complete problems (see www.languageinclusion.org). The vision is
to develop methods to solve PSPACE-complete automata theoretic problems
for automata with 10000-1000000 states.

The methods to be developed include the following:

1.
Subsumption techniques can be used to dynamically prune the search
space of the algorithm. The idea is that certain objects do not need to
be explored, because they are subsumed by other objects which have a
better chance of finding the solution.

2. Minimization techniques aim
to reduce the size of stored data objects by removing parts which are
semantically unimportant for the given problem.

3. Antichain
techniques adapted from the field of verification of infinite-state
systems have found new applications in speeding up computations.

4. Heuristics can guide the search performed by the algorithms and find the solution more quickly.

The goal of this project is to:

1. Develop and improve these techniques and optimize the resulting algorithms.

2.
Extend the applicability of these techniques to different classes of
automata, e.g., tree-automata, pushdown automata, weighted automata and
probabilistic automata.

3. Create an open source library and suite of tools that can be used by other researchers; see www.languageinclusion.org

**Slides of a recent survey talk **