Model checking quantum Markov chains
From MaRDI portal
Abstract: Although the security of quantum cryptography is provable based on the principles of quantum mechanics, it can be compromised by the flaws in the design of quantum protocols and the noise in their physical implementations. So, it is indispensable to develop techniques of verifying and debugging quantum cryptographic systems. Model-checking has proved to be effective in the verification of classical cryptographic protocols, but an essential difficulty arises when it is applied to quantum systems: the state space of a quantum system is always a continuum even when its dimension is finite. To overcome this difficulty, we introduce a novel notion of quantum Markov chain, specially suited to model quantum cryptographic protocols, in which quantum effects are entirely encoded into super-operators labelling transitions, leaving the location information (nodes) being classical. Then we define a quantum extension of probabilistic computation tree logic (PCTL) and develop a model-checking algorithm for quantum Markov chains.
Recommendations
- scientific article; zbMATH DE number 7730615
- Model checking QCTL plus on quantum Markov chains
- Model checking \(\omega\)-regular properties for quantum Markov chains
- An algebraic method to fidelity-based model checking over quantum Markov chains
- Quantum Markov chains: description of hybrid systems, decidability of equivalence, and model checking linear-time properties
- Exogenous quantum Markov chains and reachability analysis
- Reachability analysis of recursive quantum Markov chains
- Quantum Markov chains
- Model checking quantum systems. Principles and algorithms
- Reachability analysis of quantum Markov decision processes
Cites work
- scientific article; zbMATH DE number 1579275 (Why is no real title available?)
- scientific article; zbMATH DE number 47926 (Why is no real title available?)
- scientific article; zbMATH DE number 3576139 (Why is no real title available?)
- scientific article; zbMATH DE number 1142326 (Why is no real title available?)
- scientific article; zbMATH DE number 1866308 (Why is no real title available?)
- scientific article; zbMATH DE number 5585443 (Why is no real title available?)
- scientific article; zbMATH DE number 3109251 (Why is no real title available?)
- A logic for reasoning about time and reliability
- Communication via one- and two-particle operators on Einstein-Podolsky-Rosen states
- Exact Quantum Algorithms for the Leader Election Problem
- Nonrelativistic quantum mechanics as a noncommutative Markov process
- QUANTUM COMPUTATION TREE LOGIC — MODEL CHECKING AND COMPLETE CALCULUS
- Quantum Markov chains
- 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
- Stochastic model checking
- Subgroups of NEC groups
- Teleporting an unknown quantum state via dual classical and Einstein-Podolsky-Rosen channels
- Towards a quantum programming language
Cited in
(38)- Measuring the constrained reachability in quantum Markov chains
- Quantum Markov chains: description of hybrid systems, decidability of equivalence, and model checking linear-time properties
- Model Checking for Verification of Quantum Circuits
- Formalization \textit{of} quantum protocols using Coq
- Specification and verification of quantum protocols
- Toward automatic verification of quantum cryptographic protocols
- Deriving the correctness of quantum protocols in the probabilistic logic for quantum programs
- Reachability analysis of quantum Markov decision processes
- Mirrors and memory in quantum automata
- A Lambda Calculus for Density Matrices with Classical and Probabilistic Controls
- Model checking \(\omega\)-regular properties for quantum Markov chains
- Model checking quantum systems. Principles and algorithms
- An algebraic method to fidelity-based model checking over quantum Markov chains
- Model checking QCTL plus on quantum Markov chains
- Temporal normal form for linear temporal logic formulae
- Quantum Markov chains on comb graphs: Ising model
- Verification of quantum protocols with a probabilistic model-checker
- Tree-homogeneous quantum Markov chains
- Model checking computation tree logic over finite lattices
- A narrative review on quantum finance theory
- Exponential decay of matrix Φ-entropies on Markov semigroups with applications to dynamical evolutions of quantum ensembles
- Semi-automated verification of security proofs of quantum cryptographic protocols
- Open quantum random walks and quantum Markov chains on trees. II: The recurrence
- Symbolic bisimulation for quantum processes
- A Theory of Cartesian Arrays (with Applications in Quantum Circuit Verification)
- Recurrence of a class of quantum Markov chains on trees
- On stopping rules for tree-indexed quantum Markov chains
- Bisimulation for quantum processes
- On quotients of formal power series
- An overview of quantum software engineering in Latin America
- Towards quantum programs verification: from Quipper circuits to QPMC
- Testing quantum circuits and detecting insecure encryption
- Techniques for Formal Modelling and Analysis of Quantum Systems
- Open quantum random walks and quantum Markov chains on trees. I: Phase transitions
- Security analysis of semi-quantum cryptography protocols by model checking
- Toward automatic verification of quantum programs
- The modeling library of eavesdropping methods in quantum cryptography protocols by model checking
- scientific article; zbMATH DE number 7730615 (Why is no real title available?)
This page was built for publication: Model checking quantum Markov chains
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q394340)
