Model checking -regular properties for quantum Markov chains

DOI10.4230/LIPICS.CONCUR.2017.35MaRDI QIDQ5111649zbMATH OpenOpenAlexFDO

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

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)

Recommendations

• Quantum Markov chains: description of hybrid systems, decidability of equivalence, and model checking linear-time properties
• Model checking QCTL plus on quantum Markov chains
• Reachability Probabilities of Quantum Markov Chains
• Computer Aided Verification
• Model-checking linear-time properties of quantum systems

Cites work

• scientific article; zbMATH DE number 1579275 (Why is no real title available?)
• scientific article; zbMATH DE number 3990873 (Why is no real title available?)
• scientific article; zbMATH DE number 1142314 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• Communication via one- and two-particle operators on Einstein-Podolsky-Rosen states
• Computer Aided Verification
• Equivalence checking of quantum protocols
• From Nondeterministic B\"uchi and Streett Automata to Deterministic Parity Automata
• Functional and Logic Programming
• Model checking quantum Markov chains
• Model-checking linear-time properties of quantum systems
• Quantitative verification of implantable cardiac pacemakers over hybrid heart models
• Quantum Markov chains
• Quantum Markov chains: description of hybrid systems, decidability of equivalence, and model checking linear-time properties
• Quantum cryptography using any two nonorthogonal states
• Quantum cryptography: public key distribution and coin tossing
• Reachability Probabilities of Quantum Markov Chains
• Specification and verification of quantum protocols
• The complexity of probabilistic verification
• The structures of state space concerning quantum dynamical semigroups
• Tighter Bounds for the Determinisation of Büchi Automata

Cited in

(8)

• Model checking quantum Markov chains
• 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 linear-time properties of quantum systems
• Decomposition of quantum Markov chains and its applications
• An algebraic method to fidelity-based model checking over quantum Markov chains
• Model checking QCTL plus on quantum Markov chains
• scientific article; zbMATH DE number 7730615 (Why is no real title available?)

Describes a project that uses

Uses Software

• QPMC
• iscasMc

This page was built for publication: Model checking \(\omega\)-regular properties for quantum Markov chains

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5111649)