Visit ShanghaiTech University | 中文 | How to find us
HOME > News and Events > Events
Model checking quantum Markov chains
Date: 2017/7/11             Browse: 570

Speaker:   Prof. Yuan Feng

Time:         July 11, 10:30am-11:30am

Location:  Room 1A-200  , SIST Building

Inviter:    Prof. Fu Song


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.


Yuan Feng is an ARC future fellow and professor at the Centre for Quantum Software and Information (CQSI), University of Technology Sydney (UTS), Australia. He received his BS and PhD degrees from the Department of Applied Mathematics and the Department of Computer Science and Technology, Tsinghua University, in 1999 and 2004, respectively. Before joining UTS in 2009, he was an Associate Professor at Tsinghua University. Prof Feng's research interests include the theory of quantum programming, quantum information and quantum computation, and probabilistic systems. He has published more than 60 research papers in computer science journals like ACM TOPLAS, ACM TOCL, IEEE TIT, IEEE TSE, IEEE TC, I&C, and JCSS; physics journals like PRL, PRA, and QIC; and conferences like POPL, ICSE, CONCUR, CSF, MFCS, FM, IJCAI, UAI, and AAMAS.


                                                                                                                                                                                                                                      SIST-Seminar 17034