Phys.org December 19, 2024
It is crucial to verify quantum protocols before they can be trusted in safety and security-critical applications. Researchers in Japan proposed Basic Dynamic Quantum Logic (BDQL) to formalize and verify sequential models of quantum protocols with a support tool developed in Maude. As BDQL does not support concurrency in its formalization they introduced Concurrent Dynamic Quantum Logic (CDQL) to formalize and verify concurrent models of quantum protocols. They extended the syntax of BDQL to CDQL and made a transformation from CDQL to BDQL without interrupting the semantics of BDQL. They made new support tools in Maude making rewriting strategy and verification process faster. Several quantum communication protocols were successfully formalized and verified in BDQL/CDQL, demonstrating the effectiveness of their automated approach and tool in verifying quantum protocols… read more. Open Access TECHNICAL ARTICLE
The development of CDQL is an extension of basic dynamic quantum logic to handle concurrency in quantum protocols. Credit: ACM Transactions on Software Engineering and Methodology, 12 December 2024