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.

Distributed quantum computing (DQC) architectures offer a scalable solution for the computational demands of large-scale quantum computing. In near-term DQC architectures, the costly remote quantum communication and the execution cost within quantum chips together significantly limit the execution efficiency of quantum circuits. To comprehensively optimize both costs, we propose DMapS, which consists of end-to-end algorithms for qubit mapping and routing. The qubit mapping component, DMapS-M, adopts a two-stage mapping strategy that decomposes a large quantum circuit into smaller ones and parallelizes the qubit mapping on quantum chips. The qubit routing component, DMapS-R, reduces remote quantum communication overhead by prioritizing the insertion of local SWAP gates and further improves transpilation efficiency by exploiting parallelism within chips. Our experimental results show that DMapS-M reduces overall overhead (including both remote quantum communication overhead and local SWAP gate overhead) by an average of 43.44% and 59.72%, respectively, compared to two baseline algorithms, and achieves an average speedup of 87.05x. DMapS-R, compared to the baseline algorithm, reduces overall overhead by an average of 8.85% and achieves an average transpilation speedup of 2.78×. Moreover, compared to the DQC-oriented quantum compiler, DMapS reduces remote communication overhead by an average of 75.16%.

ZZ crosstalk and decoherence hinder superconducting quantum computing. Mitigation strategies often require sequential gate execution, which restricts parallelism. We reformulate ZZ crosstalk mitigation as a parallel task scheduling problem by integrating quantum cycles and qubit interference. We then propose CYCO, a CYcle-aware ZZ Crosstalk Optimization algorithm, which uses a timing-based greedy strategy to schedule gates through cycles within quantum circuits. A novel data structure called Time and Distance Dependency Graph (TDDG) is designed to model gate dependencies and physical qubit distances. Based on TDDG, barrier punching is introduced to eliminate redundant synchronization barriers by merging independent gate groups, improving gate concurrency per cycle. Simulations show a reduction of up to 37.44% in quantum program cycle (14.19% on average) on 53- to 127-qubit NISQ devices, with up to 1.6 × higher parallelism than state-of-the-art methods. Real-device experiments demonstrate significant acceleration in quantum computing while maintaining fidelity.

Verifying quantum systems has attracted a lot of interest in the last decades.In this paper, we study the quantitative model-checking of quantum continuous-time Markov chains (quantum CTMCs). The branching-time properties of quantum CTMCs are specified by continuous stochastic logic (CSL), which is well-known for verifying real-time systems, including classical CTMCs. The core of checking the CSL formulas lies in tackling multiphase until formulas. We develop an algebraic method using proper projection, matrix exponentiation, and definite integration to symbolically calculate the probability measures of path formulas. Thus the decidability of CSL is established. To be efficient, numerical methods are incorporated to guarantee that the time complexity is polynomial in the encoding size of the input model and linear in the size of the input formula. A running example of Apollonian networks is further provided to demonstrate our method.

The Domain Generalizable Re-identification (DG ReID) task has attracted significant attention in recent years, as a challenging task but closely aligned with practical applications. Mixture-of-experts (MoE)-based methods have been studied for DG ReID to exploit the discrepancies and inherent correlations between diverse domains. However, most of DG ReID methods, especially MoE-based methods, have to fully fine-tune a large amount of parameters, which are not always practical in real-world scenarios. Considering this problem, we propose a novel MoE-based DG ReID method, named Mixture of Domain Adapters (MoDA), which utilizes many expert adapters and a global adapter to help MoE-based method scale to a much larger model but in a more parameter-efficient way. Furthermore, we conduct our approach with the large-scale vision-language pre-trained model CLIP, which exploits both visual and text encoders, to learn more robust representations based on multimodal information. Extensive experiments verify the effectiveness of our method and show that MoDA achieves competitiveness with state-of-the-art DG ReID methods with much fewer tunable parameters.

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.

Quantum based systems are a relatively new research area for that different modelling languages including process calculi are currently under development. Encodings are often used to compare process calculi. Quality criteria are used then to rule out trivial or meaningless encodings. In this new context of quantum based systems, it is necessary to analyse the applicability of these quality criteria and to potentially extend or adapt them. As a first step, we test the suitability of classical criteria for encodings between quantum based languages and discuss new criteria. Concretely, we present an encoding, from a language inspired by CQP into a language inspired by qCCS. We show that this encoding satisfies compositionality, name invariance (for channel and qubit names), operational correspondence, divergence reflection, success sensitiveness, and that it preserves the size of quantum registers. Then we show that there is no encoding from qCCS into CQP that is compositional, operationally corresponding, and success sensitive.

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.

The increasing control complexity of Noisy Intermediate-Scale Quantum (NISQ) systems underlines the necessity of integrating quantum hardware with quantum software. While mapping heterogeneous quantum-classical computing (HQCC) algorithms to NISQ hardware for execution, we observed a few dissatisfactions in quantum programming languages (QPLs), including difficult mapping to hardware, limited expressiveness, and counter-intuitive code. In addition, noisy qubits require repeatedly performed quantum experiments, which explicitly operate low-level configurations, such as pulses and timing of operations. This requirement is beyond the scope or capability of most existing QPLs. We summarize three execution models to depict the quantum-classical interaction of existing QPLs. Based on the refined HQCC model, we propose the Quingo framework to integrate and manage quantum-classical software and hardware to provide the programmability over HQCC applications and map them to NISQ hardware. We propose a six-phase quantum program life-cycle model matching the refined HQCC model, which is implemented by a runtime system. We also propose the Quingo programming language, an external domain-specific language highlighting timer-based timing control and opaque operation definition, which can be used to describe quantum experiments. We believe the Quingo framework could contribute to the clarification of key techniques in the design of future HQCC systems.

Abstract One important application of quantum process algebras is to formally verify quantum communication protocols. With a suitable notion of behavioural equivalence and a decision method, one can determine if an implementation of a protocol is consistent with its specification. Ground bisimulation is a convenient behavioural equivalence for quantum processes because of its associated coinduction proof technique. We exploit this technique to design and implement two on-the-fly algorithms for the strong and weak versions of ground bisimulation to check if two given processes in quantum CCS are equivalent. We then develop a tool that can verify interesting quantum protocols such as the BB84 quantum key distribution scheme.

The notion of program sensitivity (aka Lipschitz continuity) specifies that changes in the program input result in proportional changes to the program output. For probabilistic programs the notion is naturally extended to expected sensitivity. A previous approach develops a relational program logic framework for proving expected sensitivity of probabilistic while loops, where the number of iterations is fixed and bounded. In this work, we consider probabilistic while loops where the number of iterations is not fixed, but randomized and depends on the initial input values. We present a sound approach for proving expected sensitivity of such programs. Our sound approach is martingale-based and can be automated through existing martingale-synthesis algorithms. Furthermore, our approach is compositional for sequential composition of while loops under a mild side condition. We demonstrate the effectiveness of our approach on several classical examples from Gambler's Ruin, stochastic hybrid systems and stochastic gradient descent. We also present experimental results showing that our automated approach can handle various probabilistic programs in the literature.

Modal logics and behavioral equivalences play an important role in the specification and verification of concurrent systems. In this paper, we first present a new notion of bisimulation for nondeterministic fuzzy transition systems, which is distribution based and coarser than state-based bisimulation appeared in the literature. Then, we define a distribution-based bisimilarity metric as the least fixed point of a suitable monotonic function on a complete lattice, which is a behavioral distance and is a more robust way of formalizing behavioral similarity between states than bisimulations. We also propose an on-the-fly algorithm for computing the bisimilarity metric. Moreover, we present a fuzzy modal logic and provide a sound and complete characterization of the bisimilarity metric. Interestingly, this characterization holds for a class of fuzzy modal logics. In addition, we show the nonexpansiveness of a typical parallel composition operator with respect to the bisimilarity metric, which makes compositional verification possible.

We investigate a notion of probabilistic program equivalence under linear contexts. We show that both a statebased and a distribution-based bisimilarity are sound coinductive proof techniques for reasoning about higher-order probabilistic programs, but only the distribution-based one is complete for linear contextual equivalence. The completeness proof is novel and directly constructs linear contexts from transitions, rather than the traditional approach of characterizing bisimilarities as testing equivalences.

In the ubiquitous presence of linear resources in quantum computation, program equivalence in linear contexts, where programs are used or executed once, is more important than in the classical setting. We introduce a linear contextual equivalence and two notions of bisimilarity, a state-based and a distribution-based, as proof techniques for reasoning about higher-order quantum programs. Both notions of bisimilarity are sound with respect to the linear contextual equivalence, but only the distribution-based one turns out to be complete. The completeness proof relies on a characterisation of the bisimilarity as a testing equivalence.

With the previous notions of bisimulation presented in the literature, to check if two quantum processes are bisimilar, we have to instantiate their free quantum variables with arbitrary quantum states, and verify the bisimilarity of the resulting configurations. This makes checking bisimilarity infeasible from an algorithmic point of view, because quantum states constitute a continuum. In this article, we introduce a symbolic operational semantics for quantum processes directly at the quantum operation level, which allows us to describe the bisimulation between quantum processes without resorting to quantum states. We show that the symbolic bisimulation defined here is equivalent to the open bisimulation for quantum processes in previous work, when strong bisimulations are considered. An algorithm for checking symbolic ground bisimilarity is presented. We also give a modal characterisation for quantum bisimilarity based on an extension of Hennessy-Milner logic to quantum processes.

Abstract We consider two characterisations of the may and must testing preorders for a probabilistic extension of the finite π -calculus: one based on notions of probabilistic weak simulations, and the other on a probabilistic extension of a fragment of Milner–Parrow–Walker modal logic for the π -calculus. We base our notions of simulations on similar concepts used in previous work for probabilistic CSP. However, unlike the case with CSP (or other non-value-passing calculi), there are several possible definitions of simulation for the probabilistic π -calculus, which arise from different ways of scoping the name quantification. We show that in order to capture the testing preorders, one needs to use the “earliest” simulation relation (in analogy to the notion of early (bi)simulation in the non-probabilistic case). The key ideas in both characterisations are the notion of a “characteristic formula” of a probabilistic process, and the notion of a “characteristic test” for a formula. As in an earlier work on testing equivalence for the π -calculus by Boreale and De Nicola, we extend the language of the π -calculus with a mismatch operator, without which the formulation of a characteristic test will not be possible.

The population protocol model [2] has emerged as an elegant computation paradigm for describing mobile ad hoc networks, consisting of a number of mobile nodes that interact with each other to carry out a computation. The interactions of nodes are subject to a fairness constraint. One essential property of population protocols is that all nodes must eventually converge to the correct output value (or configuration). In this paper, we aim to automatically verify self-stabilizing population protocols for leader election and token circulation in the Spin model checker [8]. We report our verification results and discuss the issue of modeling strong fairness constraints in spin.

In 1992 Wang & Larsen extended the may- and must preorders of De Nicola and Hennessy to processes featuring probabilistic as well as nondeterministic choice. They concluded with two problems that have remained open throughout the years, namely to find complete axiomatisations and alternative characterisations for these preorders. This paper solves both problems for finite processes with silent moves. It characterises the may preorder in terms of simulation, and the must preorder in terms of failure simulation. It also gives a characterisation of both preorders using a modal logic. Finally it axiomatises both preorders over a probabilistic version of CSP.

In 1992 Wang & Larsen extended the may- and must preorders of De Nicola and Hennessy to processes featuring probabilistic as well as nondeterministic choice. They concluded with two problems that have remained open throughout the years, namely to find complete axiomatisations and alternative characterisations for these preorders. This paper solves both problems for finite processes with silent moves. It characterises the may preorder in terms of simulation, and the must preorder in terms of failure simulation. It also gives a characterisation of both preorders using a modal logic. Finally it axiomatises both preorders over a probabilistic version of CSP.