Equational Reasoning About Quantum Protocols View Full Text


Ontology type: schema:Chapter      Open Access: True


Chapter Info

DATE

2015

AUTHORS

Simon J. Gay , Ittoop V. Puthoor

ABSTRACT

Communicating Quantum Processes (CQP) is a quantum process calculus that applies formal techniques from classical computer science to concurrent and communicating systems that combine quantum and classical computation. By employing the theory of behavioural equivalence between processes, it is possible to verify the correctness of a system in CQP. The equational theory of CQP helps us to analyse quantum systems by reducing the need to explicitly construct bisimulation relations. We add three new equational axioms to the existing equational theory of CQP, which helps us to analyse various quantum protocols by proving that the implementation and specification are equivalent. We summarise the necessary theory and demonstrate its application in the analysis of quantum secret sharing. Also, we illustrate the approach by verifying other interesting and important practical quantum protocols such as superdense coding, quantum error correction and remote CNOT. More... »

PAGES

155-170

References to SciGraph publications

  • 2014. Verification of Concurrent Quantum Protocols by Equivalence Checking in TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS
  • 2008. QMC: A Model Checker for Quantum Systems in COMPUTER AIDED VERIFICATION
  • 2013. Quantum Process Calculus for Linear Optical Quantum Computing in REVERSIBLE COMPUTATION
  • Book

    TITLE

    Reversible Computation

    ISBN

    978-3-319-20859-6
    978-3-319-20860-2

    Author Affiliations

    Identifiers

    URI

    http://scigraph.springernature.com/pub.10.1007/978-3-319-20860-2_10

    DOI

    http://dx.doi.org/10.1007/978-3-319-20860-2_10

    DIMENSIONS

    https://app.dimensions.ai/details/publication/pub.1001319818


    Indexing Status Check whether this publication has been indexed by Scopus and Web Of Science using the SN Indexing Status Tool
    Incoming Citations Browse incoming citations for this publication using opencitations.net

    JSON-LD is the canonical representation for SciGraph data.

    TIP: You can open this SciGraph record using an external JSON-LD service: JSON-LD Playground Google SDTT

    [
      {
        "@context": "https://springernature.github.io/scigraph/jsonld/sgcontext.json", 
        "about": [
          {
            "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/0802", 
            "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
            "name": "Computation Theory and Mathematics", 
            "type": "DefinedTerm"
          }, 
          {
            "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/08", 
            "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
            "name": "Information and Computing Sciences", 
            "type": "DefinedTerm"
          }
        ], 
        "author": [
          {
            "affiliation": {
              "alternateName": "University of Glasgow", 
              "id": "https://www.grid.ac/institutes/grid.8756.c", 
              "name": [
                "School of Computing Science, University of Glasgow"
              ], 
              "type": "Organization"
            }, 
            "familyName": "Gay", 
            "givenName": "Simon J.", 
            "id": "sg:person.07715733373.69", 
            "sameAs": [
              "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07715733373.69"
            ], 
            "type": "Person"
          }, 
          {
            "affiliation": {
              "alternateName": "University of Glasgow", 
              "id": "https://www.grid.ac/institutes/grid.8756.c", 
              "name": [
                "School of Computing Science, University of Glasgow", 
                "School of Physics and Astronomy, University of Glasgow"
              ], 
              "type": "Organization"
            }, 
            "familyName": "Puthoor", 
            "givenName": "Ittoop V.", 
            "id": "sg:person.012254764731.04", 
            "sameAs": [
              "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.012254764731.04"
            ], 
            "type": "Person"
          }
        ], 
        "citation": [
          {
            "id": "https://doi.org/10.1017/s0960129506005263", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1006707584"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1017/s0960129506005263", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1006707584"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1017/s0960129506005263", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1006707584"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-540-70545-1_51", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1018395138", 
              "https://doi.org/10.1007/978-3-540-70545-1_51"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1103/physreva.62.052316", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1018836240"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1103/physreva.62.052316", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1018836240"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1006/inco.1994.1093", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1027267686"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1145/382780.382781", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1028992479"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1016/j.entcs.2008.11.023", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1030888247"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-642-38986-3_19", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1030904470", 
              "https://doi.org/10.1007/978-3-642-38986-3_19"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1103/physreva.59.1829", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1037692613"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1103/physreva.59.1829", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1037692613"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1145/1040305.1040318", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1042468482"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-642-54862-8_42", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1051353652", 
              "https://doi.org/10.1007/978-3-642-54862-8_42"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.4204/eptcs.160.10", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1072355187"
            ], 
            "type": "CreativeWork"
          }
        ], 
        "datePublished": "2015", 
        "datePublishedReg": "2015-01-01", 
        "description": "Communicating Quantum Processes (CQP) is a quantum process calculus that applies formal techniques from classical computer science to concurrent and communicating systems that combine quantum and classical computation. By employing the theory of behavioural equivalence between processes, it is possible to verify the correctness of a system in CQP. The equational theory of CQP helps us to analyse quantum systems by reducing the need to explicitly construct bisimulation relations. We add three new equational axioms to the existing equational theory of CQP, which helps us to analyse various quantum protocols by proving that the implementation and specification are equivalent. We summarise the necessary theory and demonstrate its application in the analysis of quantum secret sharing. Also, we illustrate the approach by verifying other interesting and important practical quantum protocols such as superdense coding, quantum error correction and remote CNOT.", 
        "editor": [
          {
            "familyName": "Krivine", 
            "givenName": "Jean", 
            "type": "Person"
          }, 
          {
            "familyName": "Stefani", 
            "givenName": "Jean-Bernard", 
            "type": "Person"
          }
        ], 
        "genre": "chapter", 
        "id": "sg:pub.10.1007/978-3-319-20860-2_10", 
        "inLanguage": [
          "en"
        ], 
        "isAccessibleForFree": true, 
        "isPartOf": {
          "isbn": [
            "978-3-319-20859-6", 
            "978-3-319-20860-2"
          ], 
          "name": "Reversible Computation", 
          "type": "Book"
        }, 
        "name": "Equational Reasoning About Quantum Protocols", 
        "pagination": "155-170", 
        "productId": [
          {
            "name": "doi", 
            "type": "PropertyValue", 
            "value": [
              "10.1007/978-3-319-20860-2_10"
            ]
          }, 
          {
            "name": "readcube_id", 
            "type": "PropertyValue", 
            "value": [
              "06496b684a1f5c71a50613836ce80bf96f3d118a804031a2853006d10488966e"
            ]
          }, 
          {
            "name": "dimensions_id", 
            "type": "PropertyValue", 
            "value": [
              "pub.1001319818"
            ]
          }
        ], 
        "publisher": {
          "location": "Cham", 
          "name": "Springer International Publishing", 
          "type": "Organisation"
        }, 
        "sameAs": [
          "https://doi.org/10.1007/978-3-319-20860-2_10", 
          "https://app.dimensions.ai/details/publication/pub.1001319818"
        ], 
        "sdDataset": "chapters", 
        "sdDatePublished": "2019-04-15T22:52", 
        "sdLicense": "https://scigraph.springernature.com/explorer/license/", 
        "sdPublisher": {
          "name": "Springer Nature - SN SciGraph project", 
          "type": "Organization"
        }, 
        "sdSource": "s3://com-uberresearch-data-dimensions-target-20181106-alternative/cleanup/v134/2549eaecd7973599484d7c17b260dba0a4ecb94b/merge/v9/a6c9fde33151104705d4d7ff012ea9563521a3ce/jats-lookup/v90/0000000001_0000000264/records_8695_00000243.jsonl", 
        "type": "Chapter", 
        "url": "http://link.springer.com/10.1007/978-3-319-20860-2_10"
      }
    ]
     

    Download the RDF metadata as:  json-ld nt turtle xml License info

    HOW TO GET THIS DATA PROGRAMMATICALLY:

    JSON-LD is a popular format for linked data which is fully compatible with JSON.

    curl -H 'Accept: application/ld+json' 'https://scigraph.springernature.com/pub.10.1007/978-3-319-20860-2_10'

    N-Triples is a line-based linked data format ideal for batch operations.

    curl -H 'Accept: application/n-triples' 'https://scigraph.springernature.com/pub.10.1007/978-3-319-20860-2_10'

    Turtle is a human-readable linked data format.

    curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-319-20860-2_10'

    RDF/XML is a standard XML format for linked data.

    curl -H 'Accept: application/rdf+xml' 'https://scigraph.springernature.com/pub.10.1007/978-3-319-20860-2_10'


     

    This table displays all metadata directly associated to this object as RDF triples.

    114 TRIPLES      23 PREDICATES      38 URIs      20 LITERALS      8 BLANK NODES

    Subject Predicate Object
    1 sg:pub.10.1007/978-3-319-20860-2_10 schema:about anzsrc-for:08
    2 anzsrc-for:0802
    3 schema:author Nb18b7a67cc624ebea5339b54d047b7fe
    4 schema:citation sg:pub.10.1007/978-3-540-70545-1_51
    5 sg:pub.10.1007/978-3-642-38986-3_19
    6 sg:pub.10.1007/978-3-642-54862-8_42
    7 https://doi.org/10.1006/inco.1994.1093
    8 https://doi.org/10.1016/j.entcs.2008.11.023
    9 https://doi.org/10.1017/s0960129506005263
    10 https://doi.org/10.1103/physreva.59.1829
    11 https://doi.org/10.1103/physreva.62.052316
    12 https://doi.org/10.1145/1040305.1040318
    13 https://doi.org/10.1145/382780.382781
    14 https://doi.org/10.4204/eptcs.160.10
    15 schema:datePublished 2015
    16 schema:datePublishedReg 2015-01-01
    17 schema:description Communicating Quantum Processes (CQP) is a quantum process calculus that applies formal techniques from classical computer science to concurrent and communicating systems that combine quantum and classical computation. By employing the theory of behavioural equivalence between processes, it is possible to verify the correctness of a system in CQP. The equational theory of CQP helps us to analyse quantum systems by reducing the need to explicitly construct bisimulation relations. We add three new equational axioms to the existing equational theory of CQP, which helps us to analyse various quantum protocols by proving that the implementation and specification are equivalent. We summarise the necessary theory and demonstrate its application in the analysis of quantum secret sharing. Also, we illustrate the approach by verifying other interesting and important practical quantum protocols such as superdense coding, quantum error correction and remote CNOT.
    18 schema:editor Nec39c5852c664c6981101bf2ca8eb999
    19 schema:genre chapter
    20 schema:inLanguage en
    21 schema:isAccessibleForFree true
    22 schema:isPartOf N4095fa2118db4ffba56d83c1df692b9c
    23 schema:name Equational Reasoning About Quantum Protocols
    24 schema:pagination 155-170
    25 schema:productId N6e2d4aab8ad1499a84103c98cff6b60e
    26 N9a52c00d611442639a2785c011e34e58
    27 Nb26c200c624c4c54b3fb5eb4ff11bd69
    28 schema:publisher Nea6b62b965e4439e9d88f39a8338120f
    29 schema:sameAs https://app.dimensions.ai/details/publication/pub.1001319818
    30 https://doi.org/10.1007/978-3-319-20860-2_10
    31 schema:sdDatePublished 2019-04-15T22:52
    32 schema:sdLicense https://scigraph.springernature.com/explorer/license/
    33 schema:sdPublisher N56c8a2ed85f4401bae5b49c59ff2c6b8
    34 schema:url http://link.springer.com/10.1007/978-3-319-20860-2_10
    35 sgo:license sg:explorer/license/
    36 sgo:sdDataset chapters
    37 rdf:type schema:Chapter
    38 N302cbeeb9daf434c907bdcafbb43f087 schema:familyName Stefani
    39 schema:givenName Jean-Bernard
    40 rdf:type schema:Person
    41 N34eef9afcd954b0784ad4205f0bf0af4 rdf:first sg:person.012254764731.04
    42 rdf:rest rdf:nil
    43 N4095fa2118db4ffba56d83c1df692b9c schema:isbn 978-3-319-20859-6
    44 978-3-319-20860-2
    45 schema:name Reversible Computation
    46 rdf:type schema:Book
    47 N47393ced8ab24798846d59cad3151bea schema:familyName Krivine
    48 schema:givenName Jean
    49 rdf:type schema:Person
    50 N56c8a2ed85f4401bae5b49c59ff2c6b8 schema:name Springer Nature - SN SciGraph project
    51 rdf:type schema:Organization
    52 N6e2d4aab8ad1499a84103c98cff6b60e schema:name doi
    53 schema:value 10.1007/978-3-319-20860-2_10
    54 rdf:type schema:PropertyValue
    55 N9a52c00d611442639a2785c011e34e58 schema:name dimensions_id
    56 schema:value pub.1001319818
    57 rdf:type schema:PropertyValue
    58 Nb18b7a67cc624ebea5339b54d047b7fe rdf:first sg:person.07715733373.69
    59 rdf:rest N34eef9afcd954b0784ad4205f0bf0af4
    60 Nb26c200c624c4c54b3fb5eb4ff11bd69 schema:name readcube_id
    61 schema:value 06496b684a1f5c71a50613836ce80bf96f3d118a804031a2853006d10488966e
    62 rdf:type schema:PropertyValue
    63 Nb3570464ced34042a5086b0677548fbf rdf:first N302cbeeb9daf434c907bdcafbb43f087
    64 rdf:rest rdf:nil
    65 Nea6b62b965e4439e9d88f39a8338120f schema:location Cham
    66 schema:name Springer International Publishing
    67 rdf:type schema:Organisation
    68 Nec39c5852c664c6981101bf2ca8eb999 rdf:first N47393ced8ab24798846d59cad3151bea
    69 rdf:rest Nb3570464ced34042a5086b0677548fbf
    70 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
    71 schema:name Information and Computing Sciences
    72 rdf:type schema:DefinedTerm
    73 anzsrc-for:0802 schema:inDefinedTermSet anzsrc-for:
    74 schema:name Computation Theory and Mathematics
    75 rdf:type schema:DefinedTerm
    76 sg:person.012254764731.04 schema:affiliation https://www.grid.ac/institutes/grid.8756.c
    77 schema:familyName Puthoor
    78 schema:givenName Ittoop V.
    79 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.012254764731.04
    80 rdf:type schema:Person
    81 sg:person.07715733373.69 schema:affiliation https://www.grid.ac/institutes/grid.8756.c
    82 schema:familyName Gay
    83 schema:givenName Simon J.
    84 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07715733373.69
    85 rdf:type schema:Person
    86 sg:pub.10.1007/978-3-540-70545-1_51 schema:sameAs https://app.dimensions.ai/details/publication/pub.1018395138
    87 https://doi.org/10.1007/978-3-540-70545-1_51
    88 rdf:type schema:CreativeWork
    89 sg:pub.10.1007/978-3-642-38986-3_19 schema:sameAs https://app.dimensions.ai/details/publication/pub.1030904470
    90 https://doi.org/10.1007/978-3-642-38986-3_19
    91 rdf:type schema:CreativeWork
    92 sg:pub.10.1007/978-3-642-54862-8_42 schema:sameAs https://app.dimensions.ai/details/publication/pub.1051353652
    93 https://doi.org/10.1007/978-3-642-54862-8_42
    94 rdf:type schema:CreativeWork
    95 https://doi.org/10.1006/inco.1994.1093 schema:sameAs https://app.dimensions.ai/details/publication/pub.1027267686
    96 rdf:type schema:CreativeWork
    97 https://doi.org/10.1016/j.entcs.2008.11.023 schema:sameAs https://app.dimensions.ai/details/publication/pub.1030888247
    98 rdf:type schema:CreativeWork
    99 https://doi.org/10.1017/s0960129506005263 schema:sameAs https://app.dimensions.ai/details/publication/pub.1006707584
    100 rdf:type schema:CreativeWork
    101 https://doi.org/10.1103/physreva.59.1829 schema:sameAs https://app.dimensions.ai/details/publication/pub.1037692613
    102 rdf:type schema:CreativeWork
    103 https://doi.org/10.1103/physreva.62.052316 schema:sameAs https://app.dimensions.ai/details/publication/pub.1018836240
    104 rdf:type schema:CreativeWork
    105 https://doi.org/10.1145/1040305.1040318 schema:sameAs https://app.dimensions.ai/details/publication/pub.1042468482
    106 rdf:type schema:CreativeWork
    107 https://doi.org/10.1145/382780.382781 schema:sameAs https://app.dimensions.ai/details/publication/pub.1028992479
    108 rdf:type schema:CreativeWork
    109 https://doi.org/10.4204/eptcs.160.10 schema:sameAs https://app.dimensions.ai/details/publication/pub.1072355187
    110 rdf:type schema:CreativeWork
    111 https://www.grid.ac/institutes/grid.8756.c schema:alternateName University of Glasgow
    112 schema:name School of Computing Science, University of Glasgow
    113 School of Physics and Astronomy, University of Glasgow
    114 rdf:type schema:Organization
     




    Preview window. Press ESC to close (or click here)


    ...