Model checking quantum Markov chains

DOI10.1016/j.jcss.2013.04.002zbMath1311.68086arXiv1205.2187MaRDI 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 checking; quantum protocols; quantum Markov chains

Mathematics Subject Classification ID

94A60: Cryptography

68Q60: Specification and verification (program logics, model checking, etc.)

81S25: Quantum stochastic calculus

81P94: Quantum cryptography (quantum-theoretic aspects)

Related Items

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

Uses Software

• QPL

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• 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