Reachability and Termination Analysis of Concurrent Quantum Programs

2012/06/09 by Nengkun Yu, Mingsheng Ying, Yu, Nengkun +1 · 4 citations
Computer Science · Physics and Astronomy · #FOS: Computer and information sciences #FOS: Physical sciences #Logic in Computer Science (cs.LO) #Quantum Computing Algorithms and Architecture #Quantum Information and Cryptography #Quantum Mechanics and Applications #Quantum Physics (quant-ph)

paper · pdf · doi:10.48550/arxiv.1206.1935

openalex publication_date 2012/06/09 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

Abstract

We introduce a Markov chain model of concurrent quantum programs. This model is a quantum generalization of Hart, Sharir and Pnueli's probabilistic concurrent programs. Some characterizations of the reachable space, uniformly repeatedly reachable space and termination of a concurrent quantum program are derived by the analysis of their mathematical structures. Based on these characterizations, algorithms for computing the reachable space and uniformly repeatedly reachable space and for deciding the termination are given.

Citations

• QMC: A Model Checker for Quantum Systems

Cited by

• QReach: A Reachability Analysis Tool for Quantum Markov Chains
• (Un)decidable Problems about Reachability of Quantum Systems
• Decomposition of Quantum Markov Chains and Its Applications
• Model Checking Applied to Quantum Physics

Related

• Termination of Nondeterministic Quantum Programs
• Reachability Analysis of Quantum Markov Decision Processes
• Algorithmic Analysis of Termination Problems for Nondeterministic Quantum Programs
• Quantum Temporal Logic
• Reachability Probabilities of Quantum Markov Chains