Communicating quantum processes
From MaRDI portal
Publication:5276142
Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Quantum computation (81P68) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)
Abstract: We define a language CQP (Communicating Quantum Processes) for modelling systems which combine quantum and classical communication and computation. CQP combines the communication primitives of the pi-calculus with primitives for measurement and transformation of quantum state; in particular, quantum bits (qubits) can be transmitted from process to process along communication channels. CQP has a static type system which classifies channels, distinguishes between quantum and classical data, and controls the use of quantum state. We formally define the syntax, operational semantics and type system of CQP, prove that the semantics preserves typing, and prove that typing guarantees that each qubit is owned by a unique process within a system. We illustrate CQP by defining models of several quantum communication systems, and outline our plans for using CQP as the foundation for formal analysis and verification of combined quantum and classical systems.
Recommendations
Cited in
(30)- Branching bisimulation semantics for quantum processes
- Analysis of a quantum error correcting code using quantum process calculus
- Types and typechecking for Communicating Quantum Processes
- Interaction in Quantum Communication
- Formalization \textit{of} quantum protocols using Coq
- Model-checking linear-time properties of quantum systems
- Probabilistic bisimulations for quantum processes
- An axiomatization for quantum processes to unifying quantum and classical computing
- Entanglement in quantum process algebra
- Formal verification for KMB09 protocol
- Probabilistic process algebra to unifying quantum and classical computing in closed systems
- Verifying quantum communication protocols with ground bisimulation
- Distributed measurement-based quantum computation
- A process algebra for reasoning about quantum security
- Encodability criteria for quantum based systems
- Termination of nondeterministic quantum programs
- Distributed quantum programming
- Equational reasoning about quantum protocols
- On well-founded and recursive coalgebras
- Quantum patterns and types for entanglement and separability
- Describing and animating quantum protocols
- Simulating and compiling code for the sequential quantum random access machine
- Encodability criteria for quantum based systems
- Symbolic bisimulation for quantum processes
- Techniques for Formal Modelling and Analysis of Quantum Systems
- Bisimulations for probabilistic and quantum processes (invited paper)
- Quantum process algebra with priorities
- Quantum communication protocols as a benchmark for programmable quantum computers
- Classical knowledge for quantum cryptographic reasoning
- Quantum arrows in Haskell
This page was built for publication: Communicating quantum processes
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5276142)
