  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.
