Personal tools
You are here: Home Graduate Study Solving PSPACE-complete Problems in Automata Theory

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

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

Slides of a recent survey talk

Potential Supervisor

Richard Mayr
Document Actions