Model Checking Quantum Markov Chains

Paper information (2013, Journal of Computer and System Sciences 79:1181–1198; preprint: 2012) — Yuan Feng, Nengkun Yu, and Mingsheng Ying. arXiv:1205.2187

Work

The paper develops a model-checking framework for verifying and debugging quantum cryptographic protocols. Because even a finite-dimensional quantum system has a continuous state space, the authors encode quantum effects in superoperators labeling transitions while keeping locations classical, forming a quantum Markov chain. They then define a quantum extension of probabilistic computation tree logic (quantum PCTL) and give a model-checking algorithm.

Contributions

• A quantum Markov-chain model suited to quantum protocols.
• Superoperator-labeled transitions that avoid direct enumeration of continuous quantum states.
• Quantum PCTL for expressing probabilistic and temporal properties.
• A model-checking method for protocol verification and debugging.

Limits

Results depend on the finite-dimensional state space, transition superoperators, logic expressiveness, and numerical-decision assumptions. Classical locations do not automatically capture every hardware-noise detail, and arbitrary quantum programs or protocols may not admit an efficient model. A model proof does not replace implementation testing, cryptographic auditing, or hardware certification.

Connections

The paper extends the model-checking direction in Verification Methods and Tools to quantum systems. It complements the process-behavior comparison of Bisimulation for Quantum Processes: this work checks logical properties, while bisimulation compares process behavior. Compared with Floyd–Hoare Logic for Quantum Programs, it centers transition systems and temporal logic rather than program-assertion rules.

Original paper

Yuan Feng, Nengkun Yu, and Mingsheng Ying, Model Checking Quantum Markov Chains, Journal of Computer and System Sciences 79, 1181–1198 (2013). arXiv:1205.2187