Model-checking linear-time properties of quantum systems

Publication Type:
Journal Article
ACM Transactions on Computational Logic, 2014, 15 (3)
Issue Date:
Filename Description Size
Thumbnail2014 Model-Checking Linear-Time Properties of Quantum Systems.pdfPublished Version359.19 kB
Adobe PDF
Full metadata record
© 2014 ACM. 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, an automata-based model-checking technique is generalized for the verification of safety properties recognizable by reversible automata and ω?properties recognizable by reversible Büchi automata.
Please use this identifier to cite or link to this item: