Model-Checking Linear-Time Properties of Quantum Systems
From MaRDI portal
Publication:2946731
DOI10.1145/2629680zbMath1354.68090arXiv1101.0303OpenAlexW1988413534MaRDI QIDQ2946731
Nengkun Yu, Yangjia Li, Yuan Feng, Ming Sheng Ying
Publication date: 17 September 2015
Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1101.0303
invariantslivenesssafetymodel checkingquantum automatapersistence propertiesquantum engineering systems
Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Quantum algorithms and complexity in the theory of computing (68Q12)
Related Items (6)
Measuring the constrained reachability in quantum Markov chains ⋮ Model checking computation tree logic over finite lattices ⋮ Equivalence checking of quantum finite-state machines ⋮ Toward automatic verification of quantum programs ⋮ An automated deductive verification framework for circuit-building quantum programs ⋮ Model Checking Omega-regular Properties for Quantum Markov Chains
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Quantum cryptography: public key distribution and coin tossing
- 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
- Defining liveness
- Reasoning about infinite computations
- Probabilistic bisimulations for quantum processes
- Probabilistic model checking of complex biological pathways
- Weakly complete axiomatization of exogenous quantum propositional logic
- The logic of quantum mechanics
- Reachability and Termination Analysis of Concurrent Quantum Programs
- An algebra of quantum processes
- Universal Quantum Simulators
- QUANTUM COMPUTATION TREE LOGIC — MODEL CHECKING AND COMPLETE CALCULUS
- Proving the Correctness of Multiprocess Programs
- Local Unitary Equivalence of Multipartite Pure States
- An Algebraic Language for Distributed Quantum Computing
- Communicating quantum processes
- Bisimulation for quantum processes
- Types and typechecking for Communicating Quantum Processes
- Relations among quantum processes: bisimilarity and congruence
- Model checking of safety properties
This page was built for publication: Model-Checking Linear-Time Properties of Quantum Systems