Model checking quantum Markov chains

DOI10.1016/j.jcss.2013.04.002zbMath1311.68086arXiv1205.2187OpenAlexW2963787308MaRDI QIDQ394340

Yuan Feng, Nengkun Yu, Ming Sheng Ying

Publication date: 27 January 2014

Published in: Journal of Computer and System Sciences (Search for Journal in Brave)

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

zbMATH Keywords

model checkingquantum protocolsquantum Markov chains

Mathematics Subject Classification ID

Cryptography (94A60) Specification and verification (program logics, model checking, etc.) (68Q60) Quantum stochastic calculus (81S25) Quantum cryptography (quantum-theoretic aspects) (81P94)

Related Items

Model checking QCTL plus on quantum Markov chains, Measuring the constrained reachability in quantum Markov chains, Open Quantum Random Walks and Quantum Markov chains on Trees I: Phase transitions, Reachability analysis of quantum Markov decision processes, A Lambda Calculus for Density Matrices with Classical and Probabilistic Controls, Towards Quantum Programs Verification: From Quipper Circuits to QPMC, On quotients of formal power series, On stopping rules for tree-indexed quantum Markov chains, Recurrence of a class of quantum Markov chains on trees, Open quantum random walks and quantum Markov chains on trees. II: The recurrence, Model checking computation tree logic over finite lattices, Mirrors and memory in quantum automata, Tree-homogeneous quantum Markov chains, Deriving the correctness of quantum protocols in the probabilistic logic for quantum programs, Exponential decay of matrix Φ-entropies on Markov semigroups with applications to dynamical evolutions of quantum ensembles, Unnamed Item, Temporal normal form for Linear Temporal Logic formulae1, Toward automatic verification of quantum programs, Quantum Markov chains: description of hybrid systems, decidability of equivalence, and model checking linear-time properties, Symbolic Bisimulation for Quantum Processes, Techniques for Formal Modelling and Analysis of Quantum Systems, Quantum Markov chains on comb graphs: Ising model, Model Checking Omega-regular Properties for Quantum Markov Chains, An algebraic method to fidelity-based model checking over quantum Markov chains

Uses Software

• QPL

Cites Work

• 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
• Nonrelativistic quantum mechanics as a noncommutative Markov process
• A logic for reasoning about time and reliability
• Exact Quantum Algorithms for the Leader Election Problem
• Stochastic Model Checking
• QUANTUM COMPUTATION TREE LOGIC — MODEL CHECKING AND COMPLETE CALCULUS
• 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
• Towards a quantum programming language
• Quantum Markov chains
• Subgroups of NEC groups
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item