Jingyi Mei

TACAS Conference 2026 Conference Paper

Equivalence Checking of Quantum Circuits via Path-Sum and Weighted Model Counting

• Wei-Jia Huang
• Christophe Chareton
• Yu-Fang Chen
• Kai-Min Chung
• Min-Hsiu Hsieh
• Alfons Laarman
• Jingyi Mei

Highlights Conference 2025 Conference Abstract

Quantum Circuit Compilation with sharp-SAT

• Jingyi Mei

TCS Journal 2022 Journal Article

An algebraic method to fidelity-based model checking over quantum Markov chains

• Ming Xu
• Jianling Fu
• Jingyi Mei
• Yuxin Deng

Fidelity is one of the most widely used quantities in quantum information that measures the distance of two quantum states through a noisy channel, a kind of quantum operations. In this paper, we consider the model of quantum Markov chain (QMC), in which transitions are weighted by super-operators to characterize quantum operations and the initial quantum state is left parametric. A quantum analogy of probabilistic computation tree logic, called QCTL, is introduced to take into account fidelity, instead of probability measure, over QMC. The key to the model checking problem lies in computing the fidelity of the super-operator valued measure specified by a path formula in QCTL. It is minimized over all initial quantum states, which is intended for analyzing the system performance in the worst case. We achieve it by a reduction to quantifier elimination in the existential theory of the reals. The method is absolutely exact, so that model checking QCTL formulas against QMCs is proved to be decidable in exponential time.

TCS Journal 2022 Journal Article

Model checking QCTL plus on quantum Markov chains

• Ming Xu
• Jianling Fu
• Jingyi Mei
• Yuxin Deng

Verifying temporal properties of quantum systems, including quantum Markov chains (QMCs), has attracted an increasing interest in the last decade. Typically, the properties are specified by quantum computation tree logic (QCTL), in which reachability analysis plays a central role. However, safety as the dual problem is known little. Motivated by this, we propose a more expressive logic — QCTL+ (QCTL plus), which extends QCTL by allowing the conjunction in path formulas and the negation in the top level of path formulas. The former can be adopted to express conditional events, and the latter can express safety. To deal with conjunction, we present a product construction of classical states in the QMC and the tri-valued truths of atomic path formulas; to deal with negation, we develop an algebraic approach to compute the safety of the bottom strongly connected component subspaces with respect to a super-operator under some necessary and sufficient convergence conditions. Thereby we conditionally decide QCTL+ formulas over QMCs; without the convergence conditions the safety problem still remains open. The complexity of our method is provided in terms of the size of both the input QMC and the QCTL+ formula.