Long-distance atom shuttling between the storage zone (SZ) and the entangling zone (EZ) degrades the fidelity of quantum programs on large-scale neutral atom processors. Existing compilers often place entangling qubits near the zone boundary, underutilizing deeper EZ sites and repeatedly moving idle qubits across zones. With spatially selective laser excitation, only part of the EZ is illuminated for entangling gates while the rest stays unilluminated, which turns compilation into a constrained time-aware placement problem. We present EZCache, a hierarchical memory-system abstraction that uses the dark EZ region as a capacity-limited residency layer for idle qubits. It heuristically decides where entangling qubits execute in the illuminated EZ and which idle qubits stay resident versus return to the SZ based on near-future reuse. Across parallel entangling gates, EZCache reduces unnecessary qubit shuttling by combining reuse-window residency with look-ahead parking, thereby reducing decoherence and crosstalk exposure. Simulations show that EZCache improves fidelity by 18.1% over PowerMove and 64.2% over ZAC, and reduces total movement by 52.4% over PowerMove.

Reachability analysis plays a central role in system design and verification. The reachability problem, denoted ◊jΦ, asks whether the system will meet the property Φ after some time in a given time interval j. Recently, it has been considered on a novel kind of real-time systems — quantum continuous-time Markov chains (QCTMCs), and embedded into the model-checking algorithm. In this paper, we further study the repeated reachability problem in QCTMCs, denoted □Ι◊jΦ, which concerns whether the system starting from each absolute time in Ι meet the property Φ after some coming relative time in j. First of all, we reduce it to the real root isolation of a class of real-valued functions (exponential polynomials), whose solvability is conditional to Schanuel’s conjecture being true. To speed up the procedure, we employ the strategy of sampling. The original problem is shown to be equivalent to the existence of a finite collection of satisfying samples. We then present a sample-driven procedure, which can effectively refine the sample space after each time of sampling, no matter whether the sample itself is satisfying or conflicting. The improvement on efficiency is validated by randomly generated instances. Hence the proposed method would be promising to attack the repeated reachability problems together with checking other ω -regular properties in a wide scope of real-time systems.

Verifying quantum programs has attracted a lot of interest in recent years. In this article, we consider the following two categories of termination problems of quantum programs with nondeterminism, namely: (1) (termination) 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) (universal termination) 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 also has an explicit algebraic structure. Exploiting these explicit algebraic structures, 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, whose bottleneck lies in computing the divergent set reported for the first time. For the second category, we reduce the decision problem to the existence of an invariant subspace, from which the program terminates with probability zero under all schedulers. The invariant subspace is characterized by linear equations and thus can be efficiently computed. 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, also for the first time, to be solved in polynomial time. Finally, we demonstrate the aforementioned methods via a running example—the quantum Bernoulli factory protocol.