Model-checking quantum Markov chains: towards verification techniques for quantum cryptographic systems

Funding: 2013: $110,000
2014: $110,000
2015: $110,000

Project Member(s): Feng, Y., Ying, M.

Funding or Partner Organisation: Australian Research Council (ARC Discovery Projects)
McGill University
Technical University of Denmark

Start year: 2013

Summary: Human intuition is poorly adapted to the quantum world so design and implementation errors will occur in complex quantum cryptographic systems. This highly innovative project adapts model-checking, a dominant technique for verification of many industrial-strength systems, to the quantum setting by providing: different Markov models to describe quantum cryptographic protocols and quantum communication systems; formal logic to specify quantum system behaviours; algorithms and tools to automatically check properties of quantum systems. The breakthrough science employed will strengthen Australia's international standing in quantum computing research and provide frontier technology to industry and governments nationally and internationally.

Publications:

Zhou, L, Ying, S, Yu, N & Ying, M 2018, 'Quantum Coupling and Strassen Theorem.', CoRR, vol. abs/1803.10393.

Fu, C, Turrini, A, Huang, X, Song, L, Feng, Y & Zhang, L 1970, 'Model Checking Probabilistic Epistemic Logic for Probabilistic Multiagent Systems', Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, Twenty-Seventh International Joint Conference on Artificial Intelligence {IJCAI-18}, International Joint Conferences on Artificial Intelligence Organization, Stockholm, Sweden, pp. 4757-4763.
View/Download from: Publisher's site

Ying, M 2016, Foundations of Quantum Programming, Morgan Kaufmann Publishers.
View/Download from: Publisher's site

Su, G, Chen, T, Feng, Y, Rosenblum, DS & Thiagarajan, PS 1970, 'An Iterative Decision-Making Scheme for Markov Decision Processes and Its Application to Self-adaptive Systems', Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Fundamental Approaches to Software Engineering, Springer Berlin Heidelberg, Eindhoven, The Netherlands, pp. 269-286.
View/Download from: Publisher's site

Liu, T, Li, Y, Wang, S, Ying, M & Zhan, N 2016, 'A Theorem Prover for Quantum Hoare Logic and Its Applications'.

Feng, Y & Zhang, L 2015, 'A nearly optimal upper bound for the self-stabilization time in Herman’s algorithm', Distributed Computing, vol. 28, no. 4, pp. 233-244.
View/Download from: Publisher's site

Yu, N & Ying, M 2015, 'Optimal simulation of Deutsch gates and the Fredkin gate', PHYSICAL REVIEW A, vol. 91, no. 3.
View/Download from: Publisher's site

Feng, Y & Ying, M 1970, 'Toward automatic verification of quantum cryptographic protocols', Leibniz International Proceedings in Informatics, LIPIcs, International Conference on Concurrency Theory, Springer, Spain, pp. 441-455.
View/Download from: Publisher's site

Feng, Y & Ying, M 1970, 'Toward Automatic Verification of Quantum Cryptographic Protocols.', CONCUR, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp. 441-455.

Song, L, Feng, Y & Zhang, L 1970, 'Planning for stochastic games with Co-safe objectives', IJCAI International Joint Conference on Artificial Intelligence, International Joint Conference on Artificial Intelligence, AAAI, Buenos Aires, pp. 1682-1688.

Chen, W, Cao, Y, Wang, H & Feng, Y 2014, 'Minimum guesswork discrimination between quantum states', Computation, vol. 15, no. 9-10, pp. 9-758.

Feng, Y, Deng, Y & Ying, M 2014, 'Symbolic Bisimulation for Quantum Processes.', ACM Trans. Comput. Log., vol. 15, pp. 14:1-14:1.
View/Download from: Publisher's site

Li, Y & Ying, M 2014, 'Debugging quantum processes using monitoring measurements', PHYSICAL REVIEW A, vol. 89, no. 4.
View/Download from: Publisher's site

Ying, M, Li, Y, Yu, N & Feng, Y 2014, 'Model-Checking Linear-Time Properties of Quantum Systems', ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, vol. 15, no. 3.
View/Download from: Publisher's site

Ying, M 2014, 'Quantum Recursion and Second Quantisation'.

Feng, Y, Yu, N & Ying, M 2013, 'Model checking quantum Markov chains', JOURNAL OF COMPUTER AND SYSTEM SCIENCES, vol. 79, no. 7, pp. 1181-1198.
View/Download from: Publisher's site

Yu, N, Duan, R & Ying, M 2013, 'Five two-qubit gates are necessary for implementing the Toffoli gate', PHYSICAL REVIEW A, vol. 88, no. 1.
View/Download from: Publisher's site

Feng, Y & Zhang, L 1970, 'When Equivalence and Bisimulation Join Forces in Probabilistic Automata', Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Int. Symp. on Formal Methods, Springer International Publishing, National University of Singapore, pp. 247-262.
View/Download from: Publisher's site

Feng, Y, Yu, N & Ying, M 1970, 'Reachability Analysis of Recursive Quantum Markov Chains', MATHEMATICAL FOUNDATIONS OF COMPUTER SCIENCE 2013, International Symposium on Mathematical Foundations of Computer Science, Springer, IST Austria, pp. 385-396.
View/Download from: Publisher's site

Ying, M, Li, Y, Yu, N & Feng, Y 2011, 'Model-Checking Linear-Time Properties of Quantum Systems'.

Ying, M 1970, 'Foundations of Quantum Programming (Extended Abstract)', PROGRAMMING LANGUAGES AND SYSTEMS, Programming Languages and Systems, Springer-Verlag, Shanghai, China, pp. 16-20.
View/Download from: Publisher's site

Ying, M 2009, 'Hoare Logic for Quantum Programs'.

Keywords: Quantum Markov chains,Model checking quantum communication protocols,Quantum temporal logic

FOR Codes: Computational Logic and Formal Languages, Expanding Knowledge in the Information and Computing Sciences, Computation Theory and Mathematics not elsewhere classified, Information and Communication Services not elsewhere classified, Theory of computation not elsewhere classified, Other information and communication services not elsewhere classified

Acknowledgement of Country

UTS acknowledges the Gadigal people of the Eora Nation, the Boorooberongal people of the Dharug Nation, the Bidiagal people and the Gamaygal people, upon whose ancestral lands our university stands. We would also like to pay respect to the Elders both past and present, acknowledging them as the traditional custodians of knowledge for these lands.