| [1] |
B. Alpern and F. Schneider. 1985. Defining liveness. Information Processing Letters 21, 181–185. · Zbl 0575.68030 · doi:10.1016/0020-0190(85)90056-0 |
| [2] |
C. Baier and J.-P. Katoen. 2008. Principles of Model Checking. MIT Press, Cambridge, Massachusetts. · Zbl 1179.68076 |
| [3] |
P. Baltazar, R. Chadha, P. Mateus, and A. Sernadas. 2007. Towards model-checking quantum security protocols. In: P. Dini et al. (eds.), Proceedings of the 1st International Conference on Quantum, Nano, and Micro Technologies (ICQNM’07). IEEE Press, 14. |
| [4] |
P. Baltazar, R. Chadha, and P. Mateus. 2008. Quantum computation tree logic - model checking and complete calculus. International Journal of Quantum Information 6, 219–236. · Zbl 1151.81305 · doi:10.1142/S0219749908003530 |
| [5] |
C. H. Bennett and G. Brassard. 1984. Quantum cryptography: Public key distribution and coin tossing. In: Proceedings of International Conference on Computers, Systems and Signal Processing. 175–179. · Zbl 1306.81030 |
| [6] |
G. Birkhoff and J. von Neumann. 1936. The logic of quantum mechanics. Annals of Mathematics 37, 823–843. · Zbl 0015.14603 · doi:10.2307/1968621 |
| [7] |
H.-P. Breuer and F. Petruccione. 2002. The Theory of Open Quantum Systems. Oxford University Press, Oxford. · Zbl 1053.81001 |
| [8] |
T. Brun. 2002. A simple model of qantum trajectories. American Journal of Physics 70, 719–737. · doi:10.1119/1.1475328 |
| [9] |
G. Bruns and J. Harding. 2000. Algebraic aspects of orthomodular lattices. In: B. Coecke, D. Moore and A. Wilce (eds.), Current Research in Operational Quantum Logic: Algebras, Categories, Languages, Kluwer, Dordrecht, 37–65. · Zbl 0955.06003 · doi:10.1007/978-94-017-1201-9_2 |
| [10] |
J. I. Cirac and P. Zoller. 2012. Goals and opportunities in quantum simulation. Nature Physics 8, 264–266. · doi:10.1038/nphys2275 |
| [11] |
T. Davidson. 2011. Formal Verification Techniques Using Quantum Process Calculus, PhD thesis, University of Warwick. |
| [12] |
T. Davidson, S. J. Gay, H. Mlnarik, R. Nagarajan, and N. Papanikolaou. 2012. Model checking for communicating quantum processes. International Journal of Unconventional Computing 8, 73–98. |
| [13] |
T. Davidson, S. J. Gay, R. Nagarajan, and I. V. Puthoor. 2012. Analysis of a quantum error correcting code using quantum process calculus. In: Proceedings of the 8th International Workshop on Quantum Physics and Logic (QPL’11), Electronic Proceedings in Theoretical Computer Science 95, 67–80. |
| [14] |
J. P. Dowling and G. J. Milburn. 2003. Quantum technology: The second quantum revolution. Philosophical Transactions of the Royal Society London A 361, 1655–1674. · doi:10.1098/rsta.2003.1227 |
| [15] |
Y. Feng, R. Y. Duan, Z. F. Ji, and M. S. Ying. 2007. Probabilistic bisimulations for quantum processes. Information and Computation 205, 1608–1639. · Zbl 1130.68079 · doi:10.1016/j.ic.2007.08.001 |
| [16] |
Y. Feng, R. Y. Duan, and M. S. Ying. 2011. Bisimulations for quantum processes. In: Proceedings of the 38th ACM Symposium on Principles of Programming Languages (POPL’11). 523–534. · Zbl 1284.68425 |
| [17] |
Y. Feng, R. Y. Duan, and M. S. Ying. 2012. Bisimulations for quantum processes. ACM Transactions on Programming Languages and Systems 34, art. 17. · Zbl 1130.68079 · doi:10.1145/2400676.2400680 |
| [18] |
S. J. Gay and R. Nagarajan. 2005. Communicating quantum processes. In: Proceedings of the 32nd ACM Symposium on Principles of Programming Languages (POPL’05). 145–157. · Zbl 1369.68207 |
| [19] |
S. J. Gay and R. Nagarajan. 2006. Types and typechecking for communicating quantum processes. Mathematical Structures in Computer Science 16, 375–406. · Zbl 1122.68059 · doi:10.1017/S0960129506005263 |
| [20] |
S. J. Gay, R. Nagarajan, and N. Papanikolaou. 2005. Probabilistic model-checking of quantum protocols arXiv:quant-ph/0504007. |
| [21] |
S. J. Gay, R. Nagarajan, and N. Panaikolaou. 2008. QMC: A model checker for quantum systems. In: Proceedings of the 20th International Conference on Automated Verification (CAV’08), Lecture Notes in Computer Science 5123, Springer. 543–547. |
| [22] |
S. J. Gay, R. Nagarajan, and N. Panaikolaou. 2010. Specification and verification of quantum protocols. In: I. Mackie and S. Gay (eds.), Semantic Techniques in Quantum Computation, Cambridge University Press, 414–472. · Zbl 1196.68135 |
| [23] |
J. Heath, M. Kwiatkowska, G. Norman, D. Parker, and O. Tymchyshyn. 2006. Probabilistic model checking of complex biological pathways. In: C. Priami (ed.) Proceedings of CMSB, Lecture Notes in Computer Science 4210, Springer. 32–47. · Zbl 1133.68043 |
| [24] |
D. Gottesman. 1997. Stablizer Codes and Quantum Error Correction, Ph.D. thesis, California Institute of Technology. |
| [25] |
R. B. Griffiths. 1996. Consistent histories and quantum reasoning. Physical Review A 54, 2759–2774. · doi:10.1103/PhysRevA.54.2759 |
| [26] |
P. Jorrand and M. Lalire. 2004. Toward a quantum process algebra. In: Proceedings of the 1st ACM Conference on Computing Frontiers (CF’04). 111–119. |
| [27] |
B. Kraus. 2010. Local unitary equivalence of multipartite pure states. Physical Review Letters 104, art. no. 020504. · Zbl 1255.81048 · doi:10.1103/PhysRevLett.104.020504 |
| [28] |
K. Kraus. 1983. States, Effects, and Operations: Fundamental Notions of Quantum Theory. Lecture Notes in Physics 190, Springer. · Zbl 0545.46049 |
| [29] |
O. Kupferman and M. Y. Vardi. 2001. Model checking of safety properties. Formal Methods in System Design 19, 291–314. · Zbl 0995.68061 · doi:10.1023/A:1011254632723 |
| [30] |
A. Kondacs and J. Watrous. 1997. On the power of quantum finite state automata. In: Proceedings of the 38th Symposium on Foundation of Computer Science (FOCS’97). 66–75. |
| [31] |
M. Kwiatkowska, G. Norman, and P. Parker. 2004. Probabilistic symbolic model-checking with PRISM: A hybrid approach. International Journal on Software Tools for Technology Transfer 6, 128–142. · doi:10.1007/s10009-004-0140-2 |
| [32] |
M. Lalire. 2006. Relations among quantum processes: Bisimilarity and congruence. Mathematical Structures in Computer Science 16, 407–428. · Zbl 1122.68060 · doi:10.1017/S096012950600524X |
| [33] |
L. Lamport. 1977. Proving the correctness of multiprocess programs. IEEE Transactions on Software Engineering 3, 125–143. · Zbl 0349.68006 · doi:10.1109/TSE.1977.229904 |
| [34] |
Y. J. Li, N. K. Yu, and M. S. Ying. Termination of nondeterministic quantum programs. Short presentation of LICSÕ12 (For full paper, see arXiv: 1201.0891). |
| [35] |
S. Lloyd. 1996. Universal quantum simulators. Science 273, 1073–1078. · Zbl 1226.81059 · doi:10.1126/science.273.5278.1073 |
| [36] |
Z. Manna and A. Pnueli. 1995. The Temporal Logic of Reactive and Concurrent Systems: Safety, Springer. · Zbl 0753.68003 · doi:10.1007/978-1-4612-4222-2 |
| [37] |
P. Mateus and A. Sernadas. 2006. Weakly complete axiomatisation of exogenous quantum propositional logic. Information and Computation 204, 771–794. · Zbl 1116.03021 · doi:10.1016/j.ic.2006.02.001 |
| [38] |
R. Nagarajan and S. J. Gay. 2002. Formal verification of quantum protocols. arXiv: quant-ph/0203086. |
| [39] |
M. A. Nielsen and I. L. Chuang. 2000. Quantum Computation and Quantum Information, Cambridge University Press. · Zbl 1049.81015 |
| [40] |
N. K. Papanikolaou. 2008. Model Checking Quantum Protocols, PhD Thesis, Department of Computer Science, University of Warwick. |
| [41] |
J.-E. Pin. 1987. On the languages recognised by finite reversible automata. In: Proceedings of the 14th International Colloquium on Automata, Languages and Programming (ICALP’87). Lecture Notes in Computer Science 267, Springer, 237–249. |
| [42] |
J.-E. Pin. 2001. On reversible automata. In: Proceedings of the First Latin American Theoretical Informatics Symposium (LATIN’92), Lecture Notes in Computer Science 583, Springer. 401–416. |
| [43] |
R. Raussendorf, D. E. Browne, and H. J. Briegel. 2003. Measurement-based quantum computation with cluster states. Physical Review A 68, art. No. 022312. · doi:10.1103/PhysRevA.68.022312 |
| [44] |
M. Y. Vardi and P. Wolper. 1994. Reasoning about infinite computations. Information and Computation 115, 1–37. · Zbl 0827.03009 · doi:10.1006/inco.1994.1092 |
| [45] |
G. M. Wang and M. S. Ying. 2008. Perfect many-to-one teleportation with stabilizer states. Physical Review A 77, art. No. 032324. · doi:10.1103/PhysRevA.77.032324 |
| [46] |
G. M. Wang and M. S. Ying. 2008. Deterministic distributed dense coding with stabilizer states. Physical Review A 77, art. No. 032306. · doi:10.1103/PhysRevA.77.032306 |
| [47] |
M. S. Ying. 2007. Quantum logic and automata theory. In: D. Gabbay, D. Lehmann, and K. Engesser (eds.), Handbook of Quantum Logic and Quantum Structures, Elsevier, Amsterdam, 619–754. · doi:10.1016/B978-044452870-4/50037-6 |
| [48] |
M. S. Ying and Y. Feng. 2009. An algebraic language for distributed quantum computing. IEEE Transactions on Computers 58, 728–743. · Zbl 1367.81039 · doi:10.1109/TC.2009.13 |
| [49] |
M. S. Ying, Y. Feng, R. Y. Duan, and Z. F. Ji. 2009. An algebra of quantum processes. ACM Transactions on Computational Logic 10, art. No. 19. · Zbl 1351.68187 · doi:10.1145/1507244.1507249 |
| [50] |
M. S. Ying, R. Y. Duan, Y. Feng, and Z. F. Ji. 2010. Predicate transformer semantics of quantum programs. In: I. Mackie and S. Gay (eds.), Semantic Techniques in Quantum Computation, Cambridge University Press, 311–360. · Zbl 1196.68123 |
| [51] |
M. S. Ying, N. K. Yu, Y. Feng, and R. Y. Duan. 2013. Verification of quantum programs. Science of Computer Programming 78, 679–1700. · doi:10.1016/j.scico.2013.03.016 |
| [52] |
N. K. Yu and M. S. Ying. 2012. Reachability and termination analysis of concurrent quantum programs. In: Proceedings of the 23rd International Conference on Concurrency Theory (CONCUR 2012). Lecture Notes in Computer Science 7454, Springer. 69–83. · Zbl 1364.68145 |
