Modeling non-deterministic quantum programs for model checking

RWTH Publications (RWTH Aachen)

Abstract

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.

Authors 0

1. Author list not loaded yet.