Algorithmic Analysis of Termination Problems for Nondeterministic Quantum Programs
Jianling Fu, Hui Jiang, Ming Xu, Yuxin Deng, Zhi-Bin Li
TL;DR
This work develops a formal framework to decide termination and synthesize schedulers for nondeterministic quantum programs by modeling executions as quantum MDPs. It introduces two polynomial-time over-approximations of the reachable set, the I-reachable subspace and the II-reachable space, and an exponential-time computation of the divergent state set, enabling a necessary-and-sufficient termination test via disjointness. For universal termination, it reduces the problem to the existence of an invariant subspace and achieves polynomial-time termination-decision and universal-scheduler synthesis when such an invariant exists. The approach is instantiated on a quantum Bernoulli factory example and provides practicaltools for verifying termination properties in quantum software with nondeterminism. Overall, the framework delivers tractable algorithms for universal termination while offering rigorous, structure-exploiting methods for more general termination questions in finite-dimensional quantum settings, with clear implications for quantum-program verification and scheduler design.
Abstract
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.