|
Abstract
|
We introduce a novel notion of quantum Markov chain, specially suited to model quantum programs and quantum cryptographic protocols, in which quantum effects are entirely encoded into super-operators labelling transitions, leaving the location information (nodes) being classical. Then we define a quantum extension of probabilistic computation tree logic (PCTL) and develop a model-checking algorithm for quantum Markov chains.
|
