aqora

Formal Verification of Measurement-Based Quantum Computation in Maude

Ryuichi Nagoshi, Tsubasa Takagi

Lecture notes in computer scienceJan 1, 20261 citation

Equivalence Checking of Quantum Circuits Based on Dirac Notation in Maude

Canh Minh Do, Kazuhiro Ogata

Lecture notes in computer scienceJan 1, 20243 citations

A Logic for Formal Verification of Quantum Programs

Yoshihiko Kakutani

Lecture notes in computer scienceJan 1, 200953 citations

Symbolic model checking quantum circuits in Maude

Canh Minh Do, Kazuhiro Ogata

This article presents a symbolic approach to model checking quantum circuits using a set of laws from quantum mechanics and basic matrix operations with Dirac notation. We use Maude, a high-level specification/programming language based on rewriting logic, to implement our symbolic approach. As case studies, we use the approach to formally specify several quantum communication protocols in the early work of quantum communication and formally verify their correctness: Superdense Coding, Quantum Teleportation, Quantum Secret Sharing, Entanglement Swapping, Quantum Gate Teleportation, Two Mirror-image Teleportation, and Quantum Network Coding. We demonstrate that our approach/implementation can be a first step toward a general framework to formally specify and verify quantum circuits in Maude. The proposed way to formally specify a quantum circuit makes it possible to describe the quantum circuit in Maude such that the formal specification can be regarded as a series of quantum gate/measurement applications. Once a quantum circuit has been formally specified in the proposed way together with an initial state and a desired property expressed in linear temporal logic (LTL), the proposed model checking technique utilizes a built-in Maude LTL model checker to automatically conduct formal verification that the quantum circuit enjoys the property starting from the initial state.This article presents a symbolic approach to model checking quantum circuits using a set of laws from quantum mechanics and basic matrix operations with Dirac notation. We use Maude, a high-level specification/programming language based on rewriting logic, to implement our symbolic approach. As case studies, we use the approach to formally specify several quantum communication protocols in the early work of quantum communication and formally verify their correctness: Superdense Coding, Quantum Teleportation, Quantum Secret Sharing, Entanglement Swapping, Quantum Gate Teleportation, Two Mirror-image Teleportation, and Quantum Network Coding. We demonstrate that our approach/implementation can be a first step toward a general framework to formally specify and verify quantum circuits in Maude. The proposed way to formally specify a quantum circuit makes it possible to describe the quantum circuit in Maude such that the formal specification can be regarded as a series of quantum gate/measurement applications. Once a quantum circuit has been formally specified in the proposed way together with an initial state and a desired property expressed in linear temporal logic (LTL), the proposed model checking technique utilizes a built-in Maude LTL model checker to automatically conduct formal verification that the quantum circuit enjoys the property starting from the initial state.

PeerJ Computer ScienceJun 20, 202412 citations

Verification of Quantum Circuits

Robert Wille, Lukas Burgholzer

Springer eBooksJan 1, 20225 citations

Formalizing the Semantics of a Classical-Quantum Imperative Language in Maude

Yingge Lu, Bangjie Zhu

Recent advancements in quantum computing have exhibited substantial promise across domains such as formal verification and quantum communication. However, formal verification of hybrid quantum-classical programs remains challenging due to the complex interactions between classical control logic and quantum operations. In this paper, we propose an executable operational semantics for the Classical-Quantum Imperative Language (QIMP), implemented using the Maude system. Our framework employs rewrite rules to precisely capture classical-quantum interactions, particularly the probabilistic branching induced by quantum measurements. Experimental validation using representative algorithms, such as Quantum Teleportation and the BB84 protocol, demonstrates the capability of our semantics to accurately simulate quantum behaviors including state evolution, collapse, and classical state updates, highlighting its applicability and scalability in formal verification tasks.Recent advancements in quantum computing have exhibited substantial promise across domains such as formal verification and quantum communication. However, formal verification of hybrid quantum-classical programs remains challenging due to the complex interactions between classical control logic and quantum operations. In this paper, we propose an executable operational semantics for the Classical-Quantum Imperative Language (QIMP), implemented using the Maude system. Our framework employs rewrite rules to precisely capture classical-quantum interactions, particularly the probabilistic branching induced by quantum measurements. Experimental validation using representative algorithms, such as Quantum Teleportation and the BB84 protocol, demonstrates the capability of our semantics to accurately simulate quantum behaviors including state evolution, collapse, and classical state updates, highlighting its applicability and scalability in formal verification tasks.

International Symposium on Computer Applications and Information Systems (ISCAIS)Mar 21, 20250 citations

Formal Verification of Quantum Arithmetic Circuits in Maude

Related papers

Formal Verification of Quantum Arithmetic Circuits in Maude

Related papers