Skip to content Skip to navigation
University of Warwick
  • Study
  • |
  • Research
  • |
  • Business
  • |
  • Alumni
  • |
  • News
  • |
  • About

University of Warwick
Publications service & WRAP

Highlight your research

  • WRAP
    • Home
    • Search WRAP
    • Browse by Warwick Author
    • Browse WRAP by Year
    • Browse WRAP by Subject
    • Browse WRAP by Department
    • Browse WRAP by Funder
    • Browse Theses by Department
  • Publications Service
    • Home
    • Search Publications Service
    • Browse by Warwick Author
    • Browse Publications service by Year
    • Browse Publications service by Subject
    • Browse Publications service by Department
    • Browse Publications service by Funder
  • Help & Advice
University of Warwick

The Library

  • Login
  • Admin

Verification of concurrent quantum protocols by equivalence checking

Tools
- Tools
+ Tools

Ardeshir-Larijani, Ebrahim, Gay, Simon J. and Nagarajan, Rajagopal (2014) Verification of concurrent quantum protocols by equivalence checking. In: Ábrahám, Erika and Havelund, Klaus, (eds.) Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, Volume 8413 . Springer Berlin Heidelberg, pp. 500-514. ISBN 9783642548611

Research output not available from this repository.

Request-a-Copy directly from author or use local Library Get it For Me service.

Official URL: http://dx.doi.org/10.1007/978-3-642-54862-8_42

Request Changes to record.

Abstract

We present a tool which uses a concurrent language for describing quantum systems, and performs verification by checking equivalence between specification and implementation. In general, simulation of quantum systems using current computing technology is infeasible. We restrict ourselves to the stabilizer formalism, in which there are efficient simulation algorithms. In particular, we consider concurrent quantum protocols that behave functionally in the sense of computing a deterministic input-output relation for all interleavings of the concurrent system. Crucially, these input-output relations can be abstracted by superoperators, enabling us to take advantage of linearity. This allows us to analyse the behaviour of protocols with arbitrary input, by simulating their operation on a finite basis set consisting of stabilizer states. Despite the limitations of the stabilizer formalism and also the range of protocols that can be analysed using this approach, we have applied our equivalence checking tool to specify and verify interesting and practical quantum protocols from teleportation to secret sharing.

Item Type: Book Item
Divisions: Faculty of Science, Engineering and Medicine > Science > Computer Science
Series Name: Lecture Notes in Computer Science
Publisher: Springer Berlin Heidelberg
ISBN: 9783642548611
ISSN: 0302-9743
Book Title: Tools and Algorithms for the Construction and Analysis of Systems
Editor: Ábrahám, Erika and Havelund, Klaus
Official Date: 2014
Dates:
DateEvent
2014Published
Volume: Volume 8413
Page Range: pp. 500-514
DOI: 10.1007/978-3-642-54862-8_42
Status: Peer Reviewed
Publication Status: Published
Access rights to Published version: Restricted or Subscription Access
Conference Paper Type: Paper
Title of Event: Joint Conferences on Theory and Practice of Software, ETAPS 2014,
Type of Event: Conference
Location of Event: Grenoble, France,
Date(s) of Event: 5-13 Apr 2014

Request changes or add full text files to a record

Repository staff actions (login required)

View Item View Item
twitter

Email us: wrap@warwick.ac.uk
Contact Details
About Us