Model-Checking Linear-Time Properties of Quantum Systems

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

zbMATH Keywords

invariantslivenesssafetymodel checkingquantum automatapersistence propertiesquantum engineering systems

Mathematics Subject Classification ID

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

• PRISM

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