分野別セミナー

Abstract: While constructing practical quantum computers by big companies remains a challenge, the application of quantum communication and cryptography has made remarkable progress. As a result, it is crucial to verify quantum protocols before they can be trusted in safety and security-critical applications. Dynamic Quantum Logic (DQL), a
quantum counterpart of Dynamic Logic, has been proposed to handle quantum effects, such as superposition,
entanglement, and measurement, in order to verify quantum protocols with manual proofs. However, DQL lacks an
automated approach to quantum protocol verification and a parallel operator to handle concurrency in quantum
protocols. This talk presents recent developments in automated quantum protocol verification based on Concurrent
Dynamic Quantum Logic (CDQL), an extension of DQL for handling the concurrent behaviors of participants in
quantum protocols. Additionally, this talk shows how to effectively handle large interleavings from concurrency in
CDQL with a support tool developed in Maude, a specification and programming language based on rewriting logic.