Model checking quantum Markov chains

作者：

Highlights：

• We propose a novel notion of quantum Markov chain (qMC).

• We define quantum computation tree logic, a quantum extension of PCTL and CTL.

• We design an efficient algorithm for verifying QCTL formulas against qMCs.

摘要

•We propose a novel notion of quantum Markov chain (qMC).•We define quantum computation tree logic, a quantum extension of PCTL and CTL.•We design an efficient algorithm for verifying QCTL formulas against qMCs.

论文关键词：Quantum Markov chains,Quantum protocols,Model checking

论文评审过程：Received 10 May 2012, Revised 28 November 2012, Accepted 22 April 2013, Available online 25 April 2013.

论文官网地址：https://doi.org/10.1016/j.jcss.2013.04.002