两类量子游走组成的非确定型量子程序的终止验证

Verification of Termination for Nondeterministic Quantum Programs Constituted by Two Kinds of Quantum Walks

首先给出了C3和C4空间中由量子游走组成的非确定型量子程序的概念,其次讨论了它们从初态运行时在不同的测量算子下的可达集合、终止集合和发散集合。研究表明:非确定型量子程序的终止、发散和可达集合、发散集合与选取的测量算子有密切的关系。程序在不同测量算子作用下从同一个初态运行时可能终止,也可能发散;并且,同一个初态的可达集合中终态和发散态共存。

Firstly,the model of nondeterministic quantum programs constituted by quantum walks was proposed in C3 and C4.Secondly,the sets of reachable states,terminating states and diverging states of nondeterministic quantum programs starting in initial states under different measurement operators were discussed.It shows that the termination,diverging,the sets of reachable states and diverging states of nondeterministic quantum programs depend closely on the selection of measurement operators.The nondeterministic quantum programs starting in common initial states under different measurement operators is possible to terminate or diverge and the terminating states and diverging states of nondeterministic quantum programs coexist in the sets of reachable states starting in common initial states.