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 (24)

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

• 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

This page was built for publication: Model checking quantum Markov chains