Reachability and termination analysis of concurrent quantum programs

DOI10.1007/978-3-642-32940-1_7MaRDI QIDQ2914364zbMATH OpenOpenAlexFDO

Authors Nengkun Yu, Mingsheng Ying

Publication date 25 September 2012

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1206.1935

zbMATH Keywords

concurrent programsquantum computationreachabilitytermination

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Quantum computation (81P68)

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.

Recommendations

• Reachability analysis of recursive quantum Markov chains
• Reachability analysis of quantum Markov decision processes
• Termination of nondeterministic quantum programs
• Reachability Probabilities of Quantum Markov Chains
• Exogenous quantum Markov chains and reachability analysis

Cited in

(13)

• Reachability analysis of quantum Markov decision processes
• Decomposition of quantum Markov chains and its applications
• Termination of nondeterministic quantum programs
• Reachability analysis of recursive quantum Markov chains
• Model-checking linear-time properties of quantum systems
• Exogenous quantum Markov chains and reachability analysis
• Quantaloids for concurrency
• Model Checking for Verification of Quantum Circuits
• Quantum temporal logic and reachability problems of matrix semigroups
• Toward automatic verification of quantum programs
• Classical-quantum state quantum Markov chains and finiteness
• Measuring the constrained reachability in quantum Markov chains
• Quantum loop programs

This page was built for publication: Reachability and termination analysis of concurrent quantum programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2914364)