Model-Checking Linear-Time Properties of Quantum Systems

2010/12/31 by Mingsheng Ying, Yangjia Li, Ying, Mingsheng +5
Computer Science · #FOS: Physical sciences #Formal Methods in Verification #Quantum Computing Algorithms and Architecture #Quantum Information and Cryptography #Quantum Physics (quant-ph)

paper · pdf · doi:10.48550/arxiv.1101.0303

openalex publication_date 2010/12/31 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

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.

Citations

• Measurement-based quantum computation on cluster states

Related

• Model Checking Applied to Quantum Physics
• Measurement-based Verification of Quantum Markov Chains
• Model Checking Quantum Systems --- A Survey
• Quantum Markov chains: description of hybrid systems, decidability of equivalence, and model checking linear-time properties
• Model Checking for Verification of Quantum Circuits