Model checking quantum Markov chains
From MaRDI portal
Publication:394340
DOI10.1016/J.JCSS.2013.04.002zbMATH Open1311.68086arXiv1205.2187OpenAlexW2963787308MaRDI QIDQ394340FDOQ394340
Authors: Yuan Feng, Nengkun Yu, Mingsheng Ying 
Publication date: 27 January 2014
Published in: Journal of Computer and System Sciences (Search for Journal in Brave)
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.
Full work available at URL: https://arxiv.org/abs/1205.2187
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
Cryptography (94A60) Specification and verification (program logics, model checking, etc.) (68Q60) Quantum cryptography (quantum-theoretic aspects) (81P94) Quantum stochastic calculus (81S25)
Cites Work
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Communication via one- and two-particle operators on Einstein-Podolsky-Rosen states
- Teleporting an unknown quantum state via dual classical and Einstein-Podolsky-Rosen channels
- Title not available (Why is that?)
- Towards a quantum programming language
- Title not available (Why is that?)
- 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
- A logic for reasoning about time and reliability
- Nonrelativistic quantum mechanics as a noncommutative Markov process
- Exact Quantum Algorithms for the Leader Election Problem
- Stochastic model checking
- QUANTUM COMPUTATION TREE LOGIC — MODEL CHECKING AND COMPLETE CALCULUS
- Quantum Markov chains
- Subgroups of NEC groups
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
- Toward automatic verification of quantum cryptographic protocols
- Specification and verification of quantum protocols
- Mirrors and memory in quantum automata
- Deriving the correctness of quantum protocols in the probabilistic logic for quantum programs
- Reachability analysis of quantum Markov decision processes
- 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
- Open quantum random walks and quantum Markov chains on trees. II: The recurrence
- Semi-automated verification of security proofs of quantum cryptographic protocols
- Symbolic bisimulation for quantum processes
- A Theory of Cartesian Arrays (with Applications in Quantum Circuit Verification)
- On stopping rules for tree-indexed quantum Markov chains
- Bisimulation for quantum processes
- Recurrence of a class of quantum Markov chains on trees
- 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
- Title not available (Why is that?)
Uses Software
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)
