@inproceedings{2e327815f341480d85a227a61d951fbd,
title = "Verifying Quantum Communication Protocols with Ground Bisimulation",
abstract = "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.",
keywords = "Bisimulation, Quantum communication protocols, Quantum process algebra, Verification",
author = "Xudong Qin and Yuxin Deng and Wenjie Du",
note = "Publisher Copyright: {\textcopyright} 2020, The Author(s).; 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020 ; Conference date: 25-04-2020 Through 30-04-2020",
year = "2020",
doi = "10.1007/978-3-030-45237-7\_2",
language = "英语",
isbn = "9783030452360",
series = "Lecture Notes in Computer Science",
publisher = "Springer Science and Business Media Deutschland GmbH",
pages = "21--38",
editor = "Armin Biere and David Parker",
booktitle = "Tools and Algorithms for the Construction and Analysis of Systems- 26th International Conference, TACAS 2020, held as part of the European Joint Conferenceson Theory and Practice of Software, ETAPS 2020, Proceedings",
address = "德国",
}