Skip to content
/ DQL Public

Dynamic Quantum Logic to Verify Quantum Protocols in Maude

Notifications You must be signed in to change notification settings

canhminhdo/DQL

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

62 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

Automated Quantum Protocol Verification Based on Dynamic Quantum Logic

This repository presents a support tool developed in Maude to verify sequential quantum protocols and concurrent quantum protocols using Basic Dynamic Quantum Logic (BDQL) and Concurrent Dynamic Quantum Logic (CDQL).

Dependencies

  • Maude is a programming/specification language based on rewriting logic. How to download and install Maude can be found here.

How to install

  • Clone the source code to your computer and go to the source code directory.

  • Feed a Maude file that is the formal specification of a protocol being verified into Maude.

For example, we can type the following command in CLI in order to verify the correctness of the quantum teleportation protocol:

maude examples/teleport.maude

Note that for verifying sequential quantum protocols using BDQL, all necessary files are in the outermost folder. Meanwhile, verifying concurrent quantum protocols using CDQL, all necessary files are in the CDQL folder.

  • For testing, go to the test folder and run the ./tester file in CLI.

Case Studies

We successfully verified the correctness of some quantum protocols with the support tool as follows:

  • Superdense Coding
  • Quantum Teleportation
  • Quantum Secret Sharing
  • Entanglement Swapping
  • Quantum Gate Teleportation
  • Quantum Network Coding
  • ...

Publication

About

Dynamic Quantum Logic to Verify Quantum Protocols in Maude

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages