International Symposium on Computer Applications and Information Systems (ISCAIS)

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

Yingge Lu, Bangjie Zhu

Published Mar 21, 2025• 0 citations

Abstract

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.

DOI: 10.1109/iscait64916.2025.11010455

Related papers

Symbolic Model Checking Quantum Circuits in Maude

Canh Minh Do, Kazuhiro Ogata

This paper presents a symbolic approach to model checking quantum circuits by 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 a case study, we use the approach to formally specify and verify the correctness of the quantum teleportation protocol, which is an important quantum communication protocol in the early work of quantum communications.Moreover, our implementation can be used as a general framework to formally specify and verify quantum circuits in Maude in an effortless way, where only an initial quantum state and a sequence of actions describing how a quantum circuit works in a simple way are required.

Proceedings/Proceedings of the ... International Conference on Software Engineering and Knowledge EngineeringJul 1, 20237 citations

Modeling non-deterministic quantum programs for model checking

Kierner, Kaleb

Quantum programming introduces both probabilistic and non-deterministic behavior, making formal verification a challenging task. This work develops a framework for modeling non-deterministic quantum programs using Markov Decision Processes (MDPs). Each program configuration is represented as a combination of the remaining program and its quantum state, while transitions capture both quantum evolution and non-deterministic branching. We define operational semantics for quantum programs in terms of MDPs and prove their equivalence to established denotational semantics. This equivalence ensures consistency between high-level mathematical descriptions and executable models. The approach enables the application of model-checking techniques, originally designed for classical probabilistic systems, to quantum programs. Our results show that MDPs provide a foundation for verifying properties of non-deterministic quantum programs.

Jan 1, 20250 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.

PeerJ Computer ScienceJun 20, 202412 citations

Formal Specification and Model Checking of the BB84 Protocol in Maude (S)

Canh Minh Do, Kazuhiro Ogata

The BB84 protocol is the first quantum key distribution (QKD) protocol, allowing two parties (typically referred to as Alice and Bob) to securely share a cryptographic key by leveraging the principles of quantum mechanics.Given its importance in cryptography, simulating the protocol is essential for understanding its behavior, while formally verifying that it enjoys certain desired properties is equally crucial.This paper presents a formal specification of the BB84 protocol in Maude, a specification and programming language based on rewriting logic.The formal specification is executable in Maude with several formal analysis methods for simulation and analysis.We use the built-in Maude LTL model checker to analyze some qualitative properties of the protocol.Our analysis confirms that (1) if Alice and Bob choose the same basis and there is no eavesdropper, their bits will match; and (2) if Alice and Bob choose the same basis but do not share the same bit, the presence of an eavesdropper will be detected.

Proceedings/Proceedings of the ... International Conference on Software Engineering and Knowledge EngineeringSep 29, 20250 citations

Temporal Logic Formalization for Quantum State Verification

Jincheng Zhang

This paper introduces Q-Temporal, a novel temporal logic formalism designed specifically for the rigorous verification of quantum state evolution. Traditional methods for quantum state verification struggle to adequately represent the complexities introduced by measurement, decoherence, and the inherent probabilistic nature of quantum mechanics. Q-Temporal addresses these limitations through a branching temporal logic structure incorporating operators that explicitly model quantum operations and their corresponding measurement outcomes. The system enables the formal specification of quantum state trajectories and facilitates automated verification against theoretical predictions. This approach provides a more precise and efficient framework for ensuring the correctness of quantum algorithms and quantum systems, offering a significant improvement over existing verification techniques. The core contribution lies in the ability to capture the temporal dependencies within quantum systems with greater fidelity, ultimately leading to more robust and reliable quantum computation.

Sep 7, 20260 citations

Temporal Logic for Quantum State Evolution

Jincheng Zhang

This paper introduces a novel approach to quantum state evolution by leveraging temporal logic formalisms. The core idea is to directly represent and reason about quantum state transitions, incorporating the inherent uncertainties of non-deterministic branching and measurement outcomes. We propose a new temporal logic variant, Temporal Probabilistic Logic (TPL), where quantum state transitions are defined as logical rules and measurement collapses are modeled as probabilistic branches within the temporal reasoning process. This purely logical framework contrasts with traditional numerical simulation methods used in quantum control theory, offering potential advantages in automated proof of correctness, algorithm design, and optimization. TPL allows for the formal specification of quantum protocols and the verification of their behavior without relying on computationally intensive simulations. The paper outlines the key components of TPL, including its syntax, semantics, and operational rules, and explores its application to a simplified quantum algorithm. The presented framework provides a foundation for developing a more robust and verifiable approach to quantum computation.

Sep 1, 20260 citations