Model checking quantum protocols
Papanikolaou, Nikolaos K., 1982- (2009) Model checking quantum protocols. PhD thesis, University of Warwick.
WRAP_THESIS_Papanikolaou_2009.pdf - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
Official URL: http://webcat.warwick.ac.uk/record=b2283088~S9
This thesis describes model checking techniques for protocols arising in quantum information theory and quantum cryptography. We discuss the theory and implementation of a practical model checker, QMC, for quantum protocols. In our framework, we assume that the quantum operations performed in a protocol are restricted to those within the stabilizer formalism; while this particular set of operations is not universal for quantum computation, it allows us to develop models of several useful protocols as well as of systems involving both classical and quantum information processing. We detail the syntax, semantics and type system of QMC’s modelling language, the logic QCTL which is used for verification, and the verification algorithms that have been implemented in the tool. We demonstrate our techniques with applications to a number of case studies.
|Item Type:||Thesis or Dissertation (PhD)|
|Subjects:||Q Science > QA Mathematics > QA76 Electronic computers. Computer science. Computer software|
|Library of Congress Subject Headings (LCSH):||Information theory -- Research, Cryptography, Quantum computers, Data encryption (Computer science)|
|Institution:||University of Warwick|
|Theses Department:||Department of Computer Science|
|Supervisor(s)/Advisor:||Nagarajan, R. (Rajagopal)|
|Sponsors:||University of Warwick. Dept. of Computer Science ; Engineering and Physical Sciences Research Council (Great Britain) (EPSRC) (GR/S34090/01, EP/E006833/2, GR/S86037/01) ; Sixth Framework Programme (European Commission) (SFP) ; Fundação para a Ciência ea Tecnologia (FCT) (POCI/MAT/55796/2004) ; Conselho de Reitores das Universidades Portuguesas (CRUP)|
|Format of File:|
|Extent:||168 leaves : ill.|
Actions (login required)