This paper develops a model of quantum behavior that is intended to support the abstract yet accurate design and functional verification of quantum communication protocols. The work is motivated by the need for conceptual tools for the development of quantum-communication systems that are usable by non-specialists in quantum physics while also correctly capturing at a useful abstraction the underlying quantum phenomena. Our approach involves defining a quantum abstract machine (QAM) whose operations correspond to well-known quantum circuits; these operations, however, are given direct abstract semantics in a style similar to that of Berry's and Boudol's Chemical Abstract Machine. This paper defines the QAM's semantics and shows via examples how it may be used to model and reason about existing quantum communication protocols.

翻译：本文提出了一种量子行为模型，旨在支持量子通信协议的抽象化精确设计及功能验证。这项研究的动因在于，需要开发概念性工具以构建量子通信系统，这些工具需兼具两个特性：使非量子物理专业背景的用户能够使用，同时能在有效的抽象层面准确捕捉底层量子现象。我们的方法是通过定义一种量子抽象机（QAM），其操作对应于经典量子电路；但这些操作采用类似Berry与Boudol的化学抽象机风格，被赋予直接的抽象语义。本文界定了QAM的语义体系，并通过实例演示如何利用该模型对现有量子通信协议进行建模与推理分析。