Model checking quantum Markov chains

Publication Type:
Journal Article
Journal of Computer and System Sciences, 2013, 79 (7), pp. 1181 - 1198
Issue Date:
Filename Description Size
Thumbnail2012005090OK.pdf357.34 kB
Adobe PDF
Full metadata record
Although security of quantum cryptography is provable based on principles of quantum mechanics, it can be compromised by flaws in the design of quantum protocols. So, it is indispensable to develop techniques for verifying and debugging quantum cryptographic systems. Model-checking has proved to be effective in the verification of classical cryptographic protocols, but an essential difficulty arises when it is applied to quantum systems: the state space of a quantum system is always a continuum even when its dimension is finite. To overcome this difficulty, we introduce a novel notion of quantum Markov chain, especially suited for modelling quantum cryptographic protocols, in which quantum effects are encoded as 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. © 2013 Elsevier Inc. All rights reserved.
Please use this identifier to cite or link to this item: