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.

翻译：我们考虑包含非确定性的量子程序的两类终止问题：1) 在任意调度器下，某输入是否以概率1终止？若非如此，如何综合出一个调度器来证明非终止性？2) 所有输入是否在各自对应的调度器下以概率1终止？若是，则进一步询问是否存在一个调度器能迫使所有输入以概率1终止，以及如何综合该调度器；否则，如何提供反例输入来否定全局终止性？针对第一类问题的有效验证，我们通过可到达子空间来过度近似量子程序状态的可达集，该子空间的代数结构为线性空间。另一方面，我们研究发散状态集合——在这些状态下，程序在某些调度器下以概率0终止。该发散集合具有显式的代数结构。利用这些性质，我们通过充要条件（即可达子空间与发散集合的不交性）解决了判定问题。此外，调度器综合可在指数时间内完成。针对第二类问题，我们将判定问题归约为不变子空间的存在性——程序在该子空间上对所有调度器均以概率0终止。该不变子空间由线性方程组刻画，其上的状态即为非终止性的证据。进一步，我们通过寻找有限调度器的模式来完成调度器综合，该模式能迫使所有输入以正概率终止。该模式的重复执行即可得到所需的全局调度器，迫使所有输入以概率1终止。第二类中的所有问题均可在多项式时间内求解。