Model checking -regular properties for quantum Markov chains

DOI10.4230/LIPICS.CONCUR.2017.35zbMATH Open1442.68106OpenAlexW2758925351MaRDI QIDQ5111649FDOQ5111649

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

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

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)

Cites Work

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

Cited In (7)

• 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
• An algebraic method to fidelity-based model checking over quantum Markov chains
• Model checking QCTL plus on quantum Markov chains
• Title not available (Why is that?)

Uses Software

• iscasMc
• QPMC

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)