Bisimulation for quantum processes

DOI10.1145/1926385.1926446MaRDI QIDQ5408571zbMATH OpenOpenAlexWikidataFDO

Authors Yuan Feng, Runyao Duan, Mingsheng Ying

Publication date 10 April 2014

Published in Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1007.2584

zbMATH Keywords

bisimulationcongruencequantum communicationquantum computingquantum process algebra

Mathematics Subject Classification ID

Quantum algorithms and complexity in the theory of computing (68Q12) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Quantum cryptography (quantum-theoretic aspects) (81P94)

Abstract: In this paper we introduce a novel notion of probabilistic bisimulation for quantum processes and prove that it is congruent with respect to various process algebra combinators including parallel composition even when both classical and quantum communications are present. We also establish some basic algebraic laws for this bisimulation. In particular, we prove uniqueness of the solutions to recursive equations of quantum processes, which provides a powerful proof technique for verifying complex quantum protocols.

Recommendations

• Toward automatic verification of quantum cryptographic protocols
• Verifying quantum communication protocols with ground bisimulation
• Probabilistic bisimulations for quantum processes
• Model checking quantum Markov chains
• Open bisimulation for quantum processes

Cited in

(23)

• Quantum process algebra with priorities
• 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
• Model-checking linear-time properties of quantum systems
• Semi-automated verification of security proofs of quantum cryptographic protocols
• Techniques for Formal Modelling and Analysis of Quantum Systems
• Bisimulations for probabilistic and quantum processes (invited paper)
• Formalization \textit{of} quantum protocols using Coq
• A Lambda Calculus for Density Matrices with Classical and Probabilistic Controls
• Symbolic bisimulation for quantum processes
• Toward automatic verification of quantum cryptographic protocols
• Relations among quantum processes: bisimilarity and congruence
• Branching bisimulation semantics for quantum processes
• Explainability is a game for probabilistic bisimilarity distances

This page was built for publication: Bisimulation for quantum processes

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5408571)