Communicating quantum processes
From MaRDI portal
Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Quantum computation (81P68)
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
(34)- Quantum process algebra with priorities
- Distributed quantum programming
- An axiomatization for quantum processes to unifying quantum and classical computing
- Probabilistic process algebra to unifying quantum and classical computing in closed systems
- Entanglement in quantum process algebra
- Formal verification for KMB09 protocol
- Encodability criteria for quantum based systems
- On well-founded and recursive coalgebras
- Verifying quantum communication protocols with ground bisimulation
- Termination of nondeterministic quantum programs
- Probabilistic bisimulations for quantum processes
- Equational reasoning about quantum protocols
- A process algebra for reasoning about quantum security
- Distributed measurement-based quantum computation
- Simulating and compiling code for the sequential quantum random access machine
- Quantum patterns and types for entanglement and separability
- Classical knowledge for quantum cryptographic reasoning
- Quantum arrows in Haskell
- Model-checking linear-time properties of quantum systems
- Interaction in Quantum Communication
- Techniques for Formal Modelling and Analysis of Quantum Systems
- Analysis of a quantum error correcting code using quantum process calculus
- Bisimulations for probabilistic and quantum processes (invited paper)
- Formalization \textit{of} quantum protocols using Coq
- Symbolic bisimulation for quantum processes
- Types and typechecking for Communicating Quantum Processes
- Branching bisimulation semantics for quantum processes
- Encodability criteria for quantum based systems
- Describing and animating quantum protocols
- Quantum communication protocols as a benchmark for programmable quantum computers
- Effect semantics for quantum process calculi
- Causal reversibility in nondeterministic process calculi extended with time or probabilities
- Reconciling quantum theory and process equivalence via physically admissible schedulers
- Programming with quantum communication
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)
