量子信息系统的动态逻辑研究

量子程序语言的充分发展推动了程序检验的逻辑基础的发展,但目前关于量子程序的动态逻辑研究刚刚起步。当前的动态逻辑理论并不能充分展现真实量子系统中许多一般的量子特性，进而不能反映量子信息的实际动态演化情况。本项目主要研究量子信息的动态逻辑理论，主要研究内容包括：（1）借鉴模态逻辑、动态逻辑、量子逻辑、量子计算的思想，利用形式化方法，建立反映基于测量的量子计算模型的信息流的动态逻辑。（2）讨论他们和已有的基于线路模型的量子动态逻辑的区别和联系，进而建立一般量子信息系统的动态逻辑。（3）分析和比较与传统von Neumann 量子逻辑和unsharp量子逻辑的关系。本项目的研究不仅从逻辑的角度重现各种量子行为、刻画和反映量子信息系统中的复杂问题，而且能够为将来量子程序的验证提供逻辑基础，同时也会促进传统量子逻辑的发展。

本项目实现了项目计划规定的要求，同时增加了量子随机行走、量子通信协议两个方面的内容。.我们以基于量子测量的量子计算模型和量子随机行走为基本模型，研究了量子信息系统的动态演化规律；同时系统地研究了基于unsharp量子逻辑的量子计算理论。具体地，.(1)我们以格序QMV代数和扩张的格序effect代数作为主要的unsharp量子结构，以此为基础系统地建立了基于unsharp 量子逻辑的计算理论。主要包括：基于unsharp 量子逻辑的有穷自动机和下推自动机理论，基于unsharp 量子逻辑的图灵机和线性有界自动机理论。通过深入系统的研究，我们发现了这些unsharp量子自动机的一系列不寻常的性质；由于Von Neumann量子逻辑不适用于构造开放系统量子逻辑的Chomsky计算体系，我们研究了非von Neumann量子逻辑及其泛代数模型QMV，同时还给出了QMV代数的通过幂等元的分解定理；.(2)One way 量子计算是基于测量的量子计算的主要模式，为了研究基于测量的量子信息系统的动态规律，我们构造了费米子one-way量子计算模型。由于实验上one-way模型都建立在玻色子或自旋系统上，这也造成大规模的实现聚合态的困难。随着费米子研究在实验上取得的可喜进展及在一些计算任务上的指数加速，我们给出了费米子one-way量子计算模型的构造，给出了其信息流的演化框架，证明了费米子聚合态具有通用计算能力。并且我们仅通过测量就给出了具有通用性的费米子聚合态的构造；.(3)量子随机行走在量子算法的设计中有着重要的作用，它也能实现通用计算。它有许多与经典随机行走不同的性质。由于退想干和耗散的影响，实际中我们常碰到的是开量子随机行走。为了研究量子信息系统的动态演化规律，我们研究了带吸收边界的开量子随机行走。考察了它的动态演化规律，运用路径积分的方法计算了它的最终吸收概率和粒子被吸收前所走的平均步数。我们发现当时间趋于无穷大时，开量子随机行走表现出了类似经典随机行走的性质，这显然是酉量子随机行走所不具有的。