随着量子计算、量子信息以及量子物理技术不断进展,形式化验证量子系统的重要性已经日益凸显.由于物理环境的干扰和系统复杂性,在设计和实现量子系统的时候不可避免的会出现缺陷和错误,因此保证量子系统的正确性、安全性和可靠性就至关重要了.而形式化验证是解决这些问题的关键技术,已经被应用于验证量子通信的安全性和量子程序的正确性.不管是量子模拟计算还是量子并行计算,原理上都是利用量子相干性.然而,真实的量子系统具有开放性,并不是一个孤立系统.事实上,它会与外部环境发生相互耦合,造成量子相干性很难得到保持,从而出现量子相干性的衰减.这就是所谓的消相干.因此,相比封闭量子系统来说,更有必要对开放量子系统的形式化验证做一定的研究.形式化验证包括三种类型:等价性检测、模型检测和定理证明.其中,模型检测是目前较为成功的一种形式化验证方法,在学术界和工业界都得到广泛关注和应用.由于量子系统与经典系统存在根本性差异,这就意味着经典模型检测技术不能直接推广到量子系统中,所以开放量子系统的模型检测是一项富有挑战性的工作.本论文主要围绕建立一个开放量子系统的逻辑语言、量子迁移系统线性时间属性的检测、量子马尔可夫链的检测和广义量子Loop程序终止的验证等几个方面进行研究.文章的具体工作有以下几个方面:(1)开放量子系统的量子逻辑研究:从语构和语义角度构建一套适合于刻画开放量子系统的逻辑,称为量子算子逻辑.作为公理化系统,证明量子算子逻辑具有可靠性和完备性.作为可满足性系统,讨论量子算子逻辑的可满足性问题.研究表明:对于量子算子逻辑公式的可满足性,存在有限模型结构.给定一个模型结构,提出量子算子逻辑的公式可满足的检测算法.作为量子算子逻辑的应用,逻辑刻画了贝尔态的纠缠性以及推理BB84协议的安全性.该内容见第三章.(2)开放量子迁移系统的模型检测:基于量子算子逻辑,定义开放量子迁移系统,用于描述量子系统的演化.由于量子系统具有无穷多个量子态,这不利于提出有效搜索算法,为了避免这样的问题,引入一个有穷抽象量子状态的概念.针对开放量子迁移系统,提出量子线性时间属性,包括量子安全性、量子不变性、量子活性和量子持续性等.分别针对量子不变性和量子安全性给出检测算法,重点提出基于自动机的量子正则安全性的检测技术.作为应用,验证开放量子行走的目标顶点的可达性.该内容见第四章.(3)量子马尔可夫链的模型检测:基于量子算子逻辑,引入一类新型量子马尔可夫链,定义量子线性时间属性,并分析量子马尔可夫链的可达性.分别针对测量一次、测量多次情形,提出基于自动机的量子正则安全性的检测技术.该内容见第五章.(4)广义量子Loop程序终止验证:利用量子马尔可夫链对广义量子Loop程序进行建模.通过引入以一定概率在第n步终止和可终止两种定义,解决现有终止定义在表达力方面存在的问题.分析终止问题的归约和终状态的可达性,提出程序终止的验证方法.针对单量子比特系统、多量子比特系统、复合量子系统、嵌套量子系统,给出广义量子Loop程序终止的概率和终状态的显式计算表达式.最后,证明广义量子Loop程序终止的充分必要条件.该内容见第六章。