几种确定型量子程序的可达和终止验证

Reachability and termination verification of some deterministic quantum programs

讨论了单量子比特空间中,比特翻转、相位翻转、去极化、幅值阻尼和相位阻尼等量子信道作为特殊的非确定型量子程序—确定型量子程序,从计算基态运行时程序的可达集合和它们终止及发散的情况。研究表明:这些量子信道从计算基态运行时,有的量子程序的终止和发散与刻画量子信道的参数有紧密的联系,而有的量子程序的终止和发散与刻画量子信道的参数没有联系。

In the single qubit system, the reachable set, the termination and the diverging conditions of deterministic quantum programs, which are a special kind of nondeterministic quantum programs, are investigated. They are described by bit flip channel, phase flip channel, depolarizing channel, amplitude damping channel and phase damping channel starting in computation basis states. The investigation shows that the termination and the diverging conditions of some quantum programs described by quantum channels starting in computation basis states relate closely with the parameters represented by quantum channels, while others do not.