基于格半群的有限状态自动机的同态

本文研究了格值有限状态自动机(LFSA)的同态和强同态及其性质.利用强同态概念,在格值有限状态自动机的状态集上建立了一种等价关系,得到了格值有限状态自动机的商自动机,证明了商自动机与强同态像自动机同构.     

几类非确定型量子程序的终止验证

程序验证是保证程序正确性的关键技术.由于经典世界和量子世界的本质不同,经典程序验证的技术和工具不能直接应用到量子系统.而量子程序设计语言是描述量子系统的一种新的形式化模型,量子程序的验证问题就显得更为迫切和必要.本文首先讨论了量子通讯中常用的比特翻转、相位翻转、去极化、幅值阻尼、相位阻尼等信道作为特殊的非确定型量子程序从计算基态开始运行时的可达集合和终止集合等程序验证问题.其次,把上述五种量子程序两两组合组成非确定型量子程序,根据这五种量子程序的可达集合之相似点,最终合并成三种非确定型量子程序,重点讨论了这三种非确定型量子程序从计算基态开始运行时的终止和发散等程序验证问题.研究表明：这三种非确定型量子程序从计算基态0开始运行时都是终止的;而从计算基态1开始运行时：比特翻转信道和去极化信道组成的非确定型量子程序的终止和发散与分别刻画它们的两个参数有关;比特翻转信道和相位翻转信道组成的非确定型量子程序的终止和发散只与刻画比特翻转信道的参数有关;幅值阻尼信道和相位阻尼信道组成的非确定型量子程序是发散的,其发散条件与刻画量子信道的两个参数都没有关系.本文的结果可以为量子信息安全中量子通讯协议的验证提供理论和技术支持.     

量子马尔可夫链安全性模型检测

本文定义了量子线性时间属性,包括量子安全性,量子不变性,讨论了它们的关系和性质。结合测量一次、测量多次的单向量子有穷自动机,构建了两类乘积量子马尔可夫链,提出了基于自动机技术的量子正则安全性检测方法。通过验证乘积量子马尔可夫链的可达终状态来判断量子正则安全性的可满足性,并给出了可满足性的概率计算公式。作为应用,分析了广义量子loop程序,将程序终止归结为验证量子正则安全性的可满足性。     

广义量子Loop程序的若干性质

本文首先就广义量子loop程序(简记为GQLoop)的主体由比特翻转、去极化、幅值阻尼、相位阻尼等信道描述时,对它的终止(几乎终止)问题进行了研究.其次,讨论了两类GQLoop程序相互嵌套时loop程序的终止(几乎终止)的问题.研究表明:以量子运算的嵌套为主体的GQLoop程序终止(几乎终止)的条件依赖于刻画量子信道的参数.最后,当开放量子系统与其环境在酉运算下做为loop程序的主体时,讨论了在酉运算后去掉环境时的主系统上量子程序的执行过程.     

格值正则语言的性质

给出了格值正则文法与格值正则语言的定义.从文法的角度来研究语言的性质,讨论了格植正则语言关于正则运算的封闭性及其条件.