  We consider the two categories of termination problems of quantum programs
with nondeterminism: 1) Is an input of a program terminating with probability
one under all schedulers? If not, how can a scheduler be synthesized to
evidence the nontermination? 2) Are all inputs terminating with probability one
under their respective schedulers? If yes, a further question asks whether
there is a scheduler that forces all inputs to be terminating with probability
one together with how to synthesize it; otherwise, how can an input be provided
to refute the universal termination?
  For the effective verification of the first category, we over-approximate the
reachable set of quantum program states by the reachable subspace, whose
algebraic structure is a linear space. On the other hand, we study the set of
divergent states from which the program terminates with probability zero under
some scheduler. The divergent set has an explicit algebraic structure.
Exploiting them, we address the decision problem by a necessary and sufficient
condition, i.e. the disjointness of the reachable subspace and the divergent
set. Furthermore, the scheduler synthesis is completed in exponential time.
  For the second category, we reduce the decision problem to the existence of
invariant subspace, from which the program terminates with probability zero
under all schedulers. The invariant subspace is characterized by linear
equations. The states on that invariant subspace are evidence of the
nontermination. Furthermore, the scheduler synthesis is completed by seeking a
pattern of finite schedulers that forces all inputs to be terminating with
positive probability. The repetition of that pattern yields the desired
universal scheduler that forces all inputs to be terminating with probability
one. All the problems in the second category are shown to be solved in
polynomial time.
