Existence of Reduction Hierarchies
----------------------------------

In the automata-theoretic approach to verification, we model
programs and specifications by automata on infinite words.
Correctness of a program with respect to a specification can then be
reduced to the {\em language-containment} problem.
In a concurrent setting, the program is typically a parallel
composition of many coordinating processes, and the
language-containment problem that corresponds to verification is

    (*)   {\cal L}(P_1) \cap {\cal L}(P_2) \cap \cdots
          \cap {\cal L}(P_n) \subseteq {\cal L}(T)

where $P_1,P_2,\ldots,P_n$ are automata that model the underlying 
coordinating processes, and $T$ is the task they should perform.
In 1994, Kurshan suggested the heuristic of Reduction Hierarchies 
for circumventing the exponential blow-up introduced by conventional
methods that solve the problem (*). In the reduction-hierarchy
heuristic, we solve the problem (*) by solving a sequence of
easier problems, which involve only automata of tractable sizes.
Complexity-theoretic conjectures (NP $\neq$ PSPACE) imply that
there are settings in which the heuristic cannot circumvent the
exponential blow-up. 
In this paper, we demonstrate the strength of the heuristic, study
its properties, characterize settings in which it performs effectively,
and suggest a method for searching for reduction hierarchies.
In particular, we prove, independently of the NP $\neq$ PSPACE question,
that reduction hierarchies of tractable sizes do not always exist.