Model-Checking Linear-Time Properties of Quantum Systems
Mingsheng Ying, Yangjia Li, Nengkun Yu, Yuan Feng
TL;DR
This paper introduces a formal framework for verifying linear-time properties of quantum systems using quantum automata and automata-based model checking techniques, including algorithms for invariant verification and safety property analysis.
Contribution
It presents a novel formal framework and algorithms for model checking linear-time properties of quantum systems using quantum automata and reversible automata.
Findings
Algorithm for verifying invariants of quantum automata.
Automata-based model checking extended to quantum systems.
Verification of safety and omega-properties in quantum models.
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsQuantum Computing Algorithms and Architecture · Formal Methods in Verification · Quantum Information and Cryptography