Seminário de Computação e Informação Quântica 

07/06/2005, 15:00 — 16:00 — Sala P4.35, Pavilhão de Matemática
Simon Gay, U Glasgow

Probabilistic model-checking of quantum protocols

Quantum cryptographic systems are likely to become technologically important in the near future, and it is important to be confident of their correctness. Although several quantum protocols have been mathematically proved correct, we argue that further steps of verification are necessary in order to be confident of the correctness of a complete system, which is likely to combine both quantum and classical communication and computation. We have begun to apply formal modelling and verification techniques, which have been successful in the analysis of classical communication and cryptographic systems, to quantum systems; initially we have focussed on model-checking techniques, and in particular the probabilistic model-checking tool PRISM. This seminar will outline the challenges involved in formal verification of quantum systems, and report some initial results. This is joint work with Nick Papanikolaou and Raja Nagarajan of the University of Warwick, and is certainly work in progress.