Model-checking linear-time properties of quantum systems
From MaRDI portal
Abstract: We define a formal framework for reasoning about linear-time properties of quantum systems in which quantum automata are employed in the modeling of systems and certain closed subspaces of state (Hilbert) spaces are used as the atomic propositions about the behavior of systems. We provide an algorithm for verifying invariants of quantum automata. Then automata-based model-checking technique is generalized for the verification of safety properties recognizable by reversible automata and omega-properties recognizable by reversible Buechi automata.
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
- Model checking -regular properties for quantum Markov chains
- On relation between linear temporal logic and quantum finite automata
- Temporal logics for reasoning about quantum systems
Cites work
- scientific article; zbMATH DE number 1579275 (Why is no real title available?)
- scientific article; zbMATH DE number 5708042 (Why is no real title available?)
- scientific article; zbMATH DE number 52331 (Why is no real title available?)
- scientific article; zbMATH DE number 1512853 (Why is no real title available?)
- scientific article; zbMATH DE number 1866308 (Why is no real title available?)
- scientific article; zbMATH DE number 5585443 (Why is no real title available?)
- An Algebraic Language for Distributed Quantum Computing
- An algebra of quantum processes
- Bisimulation for quantum processes
- Communicating quantum processes
- Defining liveness
- Local unitary equivalence of multipartite pure states
- Model checking of safety properties
- Probabilistic bisimulations for quantum processes
- Probabilistic model checking of complex biological pathways
- Proving the Correctness of Multiprocess Programs
- QUANTUM COMPUTATION TREE LOGIC — MODEL CHECKING AND COMPLETE CALCULUS
- Quantum cryptography: public key distribution and coin tossing
- Reachability and termination analysis of concurrent quantum programs
- Reasoning about infinite computations
- Relations among quantum processes: bisimilarity and congruence
- Specification and verification of quantum protocols
- 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
- The logic of quantum mechanics
- Types and typechecking for Communicating Quantum Processes
- Universal Quantum Simulators
- Weakly complete axiomatization of exogenous quantum propositional logic
Cited in
(14)- Measuring the constrained reachability in quantum Markov chains
- Quantum Markov chains: description of hybrid systems, decidability of equivalence, and model checking linear-time properties
- Equivalence checking of quantum finite-state machines
- Model Checking for Verification of Quantum Circuits
- An automated deductive verification framework for circuit-building quantum programs
- Model checking -regular properties for quantum Markov chains
- Model checking quantum systems. Principles and algorithms
- Model checking QCTL plus on quantum Markov chains
- Quantum temporal logic and reachability problems of matrix semigroups
- Model checking computation tree logic over finite lattices
- Model checking reversible systems: forwardly
- On relation between linear temporal logic and quantum finite automata
- Techniques for Formal Modelling and Analysis of Quantum Systems
- Toward automatic verification of quantum programs
This page was built for publication: Model-checking linear-time properties of quantum systems
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2946731)
