Model Checking Omega-regular Properties for Quantum Markov Chains

DOI10.4230/LIPIcs.CONCUR.2017.35zbMath1442.68106OpenAlexW2758925351MaRDI QIDQ5111649

Shenggang Ying, Andrea Turrini, Ernst Moritz Hahn, Yuan Feng

Publication date: 27 May 2020

Full work available at URL: https://opus.lib.uts.edu.au/bitstream/10453/127383/1/LIPIcs-CONCUR-2017-35.pdf

zbMATH Keywords

model checkingquantum Markov chains\(\omega\)-regular propertiesbottom strongly connected component

Mathematics Subject Classification ID

Quantum computation (81P68) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

Model checking QCTL plus on quantum Markov chains ⋮ Measuring the constrained reachability in quantum Markov chains ⋮ An algebraic method to fidelity-based model checking over quantum Markov chains

Uses Software

• iscasMc
• QPMC

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Model checking quantum Markov chains
• Quantum cryptography: public key distribution and coin tossing
• Quantum Markov chains: description of hybrid systems, decidability of equivalence, and model checking linear-time properties
• Quantitative verification of implantable cardiac pacemakers over hybrid heart models
• Reachability Probabilities of Quantum Markov Chains
• THE STRUCTURES OF STATE SPACE CONCERNING QUANTUM DYNAMICAL SEMIGROUPS
• Model-Checking Linear-Time Properties of Quantum Systems
• Tighter Bounds for the Determinisation of Büchi Automata
• The complexity of probabilistic verification
• Communication via one- and two-particle operators on Einstein-Podolsky-Rosen states
• Quantum cryptography using any two nonorthogonal states
• Functional and Logic Programming
• Computer Aided Verification
• Equivalence Checking of Quantum Protocols
• From Nondeterministic B\"uchi and Streett Automata to Deterministic Parity Automata
• Quantum Markov chains