Verifying quantum communication protocols with ground bisimulation. (English) Zbl 1473.68115
Biere, Armin (ed.) et al., Tools and algorithms for the construction and analysis of systems. 26th international conference, TACAS 2020, held as part of the European joint conferences on theory and practice of software, ETAPS 2020, Dublin, Ireland, April 25–30, 2020. Proceedings. Part II. Cham: Springer. Lect. Notes Comput. Sci. 12079, 21-38 (2020).
Summary: One important application of quantum process algebras is to formally verify quantum communication protocols. With a suitable notion of behavioural equivalence and a decision method, one can determine if an implementation of a protocol is consistent with its specification. Ground bisimulation is a convenient behavioural equivalence for quantum processes because of its associated coinduction proof technique. We exploit this technique to design and implement two on-the-fly algorithms for the strong and weak versions of ground bisimulation to check if two given processes in quantum CCS are equivalent. We then develop a tool that can verify interesting quantum protocols such as the BB84 quantum key distribution scheme.
For the entire collection see [Zbl 1471.68010].
For the entire collection see [Zbl 1471.68010].
MSC:
| 68Q85 | Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) |
| 68Q12 | Quantum algorithms and complexity in the theory of computing |
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 81P68 | Quantum computation |
References:
| [1] | Ying, M.: Foundations of Quantum Programming · Zbl 1541.68005 |
| [2] | Ying, M., Feng, Y., Duan, R., Ji, Z.: An algebra of quantum processes. ACMTransactions on Computational Logic 10(3), 1-36 (2009) · Zbl 1351.68187 |
| [3] | Turrini, A., Hermanns, H.: Polynomial time decision algorithms for probabilistic automata. Information and Computation 244, 134-171 (2015) · Zbl 1329.68168 · doi:10.1016/j.ic.2015.07.004 |
| [4] | Shor, P., Preskill, J.: Simple proof of security of the BB84 quantum key distribution protocol. Physical Review Letters 85(2), 441-444 (2000) · doi:10.1103/PhysRevLett.85.441 |
| [5] | Selinger, P.: Towards a quantum programming language. Mathematical Structures in Computer Science 14(4), 527-586 (2004) · Zbl 1085.68014 · doi:10.1017/S0960129504004256 |
| [6] | Sangiorgi, D.: A theory of bisimulation for the pi-calculus. Acta Informatica 33(1), 69-97 (1996) · Zbl 0835.68072 · doi:10.1007/s002360050036 |
| [7] | Milner, R.: Communication and Concurrency. Prentice-Hall (1989) · Zbl 0683.68008 |
| [8] | Liu, T., Li, Y., Wang, S., Ying, M., Zhan, N.: A theorem prover for quantum hoare logic and its applications. CoRR abs/1601.03835 (2016) |
| [9] | Lalire, M.: Relations among quantum processes: Bisimilarity and congruence. Mathematical Structures in Computer Science 16(3), 407-428 (2006) · Zbl 1122.68060 · doi:10.1017/S096012950600524X |
| [10] | Kubota, T., Kakutani, Y., Kato, G., Kawano, Y., Sakurada, H.: Semi-automated verification of security proofs of quantum cryptographic protocols. Journal of Symbolic Computation 73, 192-220 (2016) · Zbl 1336.68164 · doi:10.1016/j.jsc.2015.05.001 |
| [11] | Kissinger, A.: Pictures of Processes: Automated Graph Rewriting for Monoidal Categories and Applications to Quantum Computing. Ph.D. thesis, University of Oxford (2011) |
| [12] | Jorrand, P., Lalire, M.: Toward a quantum process algebra. In: Proceedings of the 1st Conference on Computing Frontiers. pp. 111-119. ACM (2004) |
| [13] | Hennessy, M., Lin, H.: Symbolic bisimulations. Theoretical Computer Science 138(2), 353-389 (1995) · Zbl 0874.68187 · doi:10.1016/0304-3975(94)00172-F |
| [14] | Gay, Simon J., Nagarajan, Rajagopal, Papanikolaou, Nikolaos: QMC: A Model Checker for Quantum Systems. In: Gupta, Aarti, Malik, Sharad (eds.) CAV 2008. LNCS, vol. 5123, pp. 543-547. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-70545-1_51 · doi:10.1007/978-3-540-70545-1_51 |
| [15] | Gay, S.J., Nagarajan, R.: Communicating quantum processes. In: Palsberg, J., Abadi, M. (eds.) Proceedings of the 32Nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. pp. 145-157 (2005) · Zbl 1369.68207 |
| [16] | Fernandez, J.C., Mounier, L.: Verifying bisimulations “on the fly”. In: Proceedings of the 3rd International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols. pp. 95-110. North-Holland (1990) |
| [17] | Feng, Yuan, Hahn, Ernst Moritz, Turrini, Andrea, Zhang, Lijun: QPMC: A Model Checker for Quantum Programs and Protocols. In: Bjørner, Nikolaj, de Boer, Frank (eds.) FM 2015. LNCS, vol. 9109, pp. 265-272. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-19249-9_17 · doi:10.1007/978-3-319-19249-9_17 |
| [18] | Feng, Y., Duan, R., Ying, M.: Bisimulation for quantum processes. In: Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. pp. 523-534. ACM (2011) · Zbl 1284.68425 |
| [19] | Feng, Y., Deng, Y., Ying, M.: Symbolic bisimulation for quantum processes. ACM Transactions on Computational Logic 15(2), 1-32 (2014) · Zbl 1291.68237 · doi:10.1145/2579818 |
| [20] | Feng, Y., Duan, R., Ji, Z., Ying, M.: Probabilistic bisimulations for quantum processes. Information and Computation 205(11), 1608-1639 (2007) · Zbl 1130.68079 · doi:10.1016/j.ic.2007.08.001 |
| [21] | Deng, Yuxin, Feng, Yuan: Open Bisimulation for Quantum Processes. In: Baeten, Jos C.M., Ball, Tom, de Boer, Frank S. (eds.) TCS 2012. LNCS, vol. 7604, pp. 119-133. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-33475-7_9 · Zbl 1362.68210 · doi:10.1007/978-3-642-33475-7_9 |
| [22] | Deng, Y., Du, W.: A local algorithm for checking probabilistic bisimilarity. In: Proceedings of the 4th International Conference on Frontier of Computer Science and Technology. pp. 401-407. IEEE Computer Society (2009) |
| [23] | Davidson, T.A.S.: Formal Verification Techniques using Quantum Process Calculus. Ph.D. thesis, University of Warwick (2011) |
| [24] | Bennett, C.H., Brassard, G.: Quantum cryptography: Public-key distribution and coin tossing. In: Proceedings of the IEEE International Conference on Computer, Systems and Signal Processing. pp. 175-179 (1984) · Zbl 1306.81030 |
| [25] | Baier, C., Engelen, B., Majster-Cederbaum, M.E.: Deciding bisimilarity and similarity for probabilistic processes. Journal of Computer and System Sciences 60(1), 187-231 (2000) · Zbl 1073.68690 · doi:10.1006/jcss.1999.1683 |
| [26] | Ardeshir-Larijani, E., Gay, S.J., Nagarajan, R.: Automated equivalence checking of concurrent quantum systems. ACM Transactions on Computational Logic 19(4), 28:1-28:32 (2018) · Zbl 1407.68276 |
| [27] | Aaronson, S., Gottesman, D.: Improved simulation of stabilizer circuits.Physical Review A 70(052328) (2004) |
| [28] | Abramsky, S., Coecke, B.: A categorical semantics of quantum protocols. In: Proceedings of the 19th IEEE Symposium on Logic in Computer Science. pp. 415-425. IEEE Computer Society (2004) |
| [29] | Deng, Y.: Semantics of Probabilistic Processes: An Operational Approach.Springer (2015) |
| [30] | Qin, X., Deng, Y., Du, W.: QBisim (2020), https://github.com/MartianQXD/QBisim |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
