Symbolic bisimulation for quantum processes
From MaRDI portal
Abstract: With the previous notions of bisimulation presented in literature, to check if two quantum processes are bisimilar, we have to instantiate the free quantum variables of them with arbitrary quantum states, and verify the bisimilarity of resultant configurations. This makes checking bisimilarity infeasible from an algorithmic point of view because quantum states constitute a continuum. In this paper, we introduce a symbolic operational semantics for quantum processes directly at the quantum operation level, which allows us to describe the bisimulation between quantum processes without resorting to quantum states. We show that the symbolic bisimulation defined here is equivalent to the open bisimulation for quantum processes in the previous work, when strong bisimulations are considered. An algorithm for checking symbolic ground bisimilarity is presented. We also give a modal logical characterisation for quantum bisimilarity based on an extension of Hennessy-Milner logic to quantum processes.
Recommendations
Cites work
- A theory of bisimulation for the -calculus
- A theory of communicating processes with value passing
- An algebra of quantum processes
- Bisimulation for quantum processes
- Communicating quantum processes
- Communication via one- and two-particle operators on Einstein-Podolsky-Rosen states
- scientific article; zbMATH DE number 1579275 (Why is no real title available?)
- scientific article; zbMATH DE number 42752 (Why is no real title available?)
- scientific article; zbMATH DE number 177817 (Why is no real title available?)
- Model checking quantum Markov chains
- Open bisimulation for quantum processes
- Probabilistic bisimulations for quantum processes
- Quantum cryptography: public key distribution and coin tossing
- Relations among quantum processes: bisimilarity and congruence
- Semi-automated verification of security proofs of quantum cryptographic protocols
- Specification and verification of quantum protocols
- States, effects, and operations. Fundamental notions of quantum theory. Lectures in mathematical physics at the University of Texas at Austin. Ed. by A. Böhm, J. D. Dollard and W. H. Wootters
- Symbolic bisimulations
- Symbolic model checking: \(10^{20}\) states and beyond
- Teleporting an unknown quantum state via dual classical and Einstein-Podolsky-Rosen channels
Cited in
(12)- SMT-based generation of symbolic automata
- On well-founded and recursive coalgebras
- Verifying quantum communication protocols with ground bisimulation
- Correctness checking of a quantum protocol for reliable communications via feedback
- Compositional equivalences based on open pNets
- Open bisimulation for quantum processes
- An algebra of quantum processes
- Observational equivalence using schedulers for quantum processes
- Bisimulations for probabilistic and quantum processes (invited paper)
- Branching bisimulation semantics for quantum processes
- Effect semantics for quantum process calculi
- The way we were: structural operational semantics research in perspective
This page was built for publication: Symbolic bisimulation for quantum processes
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5169970)
