Reachability and Termination Analysis of Concurrent Quantum Programs

Publisher:
Sringer-Verlag
Publication Type:
Journal Article
Citation:
Lecture Notes in Computer Science, 2012, 7454 pp. 69 - 83
Issue Date:
2012-01
Full metadata record
Files in This Item:
Filename Description Size
Thumbnail2012001822OK.pdf270.06 kB
Adobe PDF
We introduce a Markov chain model of concurrent quantum programs. This model is a quantum generalization of Hart, Sharir and Pnuelis 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.
Please use this identifier to cite or link to this item: