Model-checking linear-time properties of quantum systems
- Publication Type:
- Journal Article
- ACM Transactions on Computational Logic, 2014, 15 (3)
- Issue Date:
|2014 Model-Checking Linear-Time Properties of Quantum Systems.pdf||Published Version||359.19 kB|
Copyright Clearance Process
- Recently Added
- In Progress
- Closed Access
This item is closed access and not available.
© 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: