Model Checking Quantum Systems --- A Survey <s> III. MODEL CHECKING QUANTUM AUTOMATA <s> In this paper, we introduce 1-way and 2-way quantum finite state automata (1qfa's and 2qfa's), which are the quantum analogues of deterministic, nondeterministic and probabilistic 1-way and 2-way finite state automata. We prove the following facts regarding 2qfa's. 1. For any /spl epsiv/>0, there is a 2qfa M which recognizes the non-regular language L={a/sup m/b/sup m/|m/spl ges/1} with (one-sided) error bounded by E, and which halts in linear time. Specifically, M accepts any string in L with probability 1 and rejects any string not in L with probability at least 1-/spl epsiv/. 2. For every regular language L, there is a reversible (and hence quantum) 2-way finite state automaton which recognizes L and which runs in linear time. In fact, it is possible to define 2qfar's which recognize the non-context-free language {a/sup m/b/sup m/c/sup m/|m/spl ges/1}, based on the same technique used for 1. Consequently, the class of languages recognized by linear time, bounded error 2qfa's properly includes the regular languages. Since it is known that 2-way deterministic, nondeterministic and polynomial expected time, bounded error probabilistic finite automata can recognize only regular languages, it follows that 2qfa's are strictly more powerful than these "classical" models. In the case of 1-way automata, the situation is reversed. We prove that the class of languages recognizable by bounded error 1qfa's is properly contained in the class of regular languages. <s> BIB001 </s> Model Checking Quantum Systems --- A Survey <s> III. MODEL CHECKING QUANTUM AUTOMATA <s> To study quantum computation, it might be helpful to generalize structures from language and automata theory to the quantum case. To that end, we propose quantum versions of finite-state and push-down automata, and regular and context-free grammars. We find analogs of several classical theorems, including pumping lemmas, closure properties, rational and algebraic generating functions, and Greibach normal form. We also show that there are quantum context-free languages that are not context-free. <s> BIB002 </s> Model Checking Quantum Systems --- A Survey <s> III. MODEL CHECKING QUANTUM AUTOMATA <s> 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. <s> BIB003 </s> Model Checking Quantum Systems --- A Survey <s> III. MODEL CHECKING QUANTUM AUTOMATA <s> We study the reachability problem of a quantum system modeled by a quantum automaton, namely, a set of processes each of which is formalized as a quantum unitary transformation. The reachable sets are chosen to be boolean combinations of (closed) subspaces of the state Hilbert space of the quantum system. Four different reachability properties are considered: eventually reachable, globally reachable, ultimately forever reachable, and infinitely often reachable. The main result of this paper is that all of the four reachability properties are undecidable in general; however, the last three become decidable if the reachable sets are boolean combinations without negation. <s> BIB004
A research line pursued by the authors and their collaborators is to develop model-checking techniques that can be used not only for quantum communication protocols but also for general quantum systems, including physical systems and quantum programs. Quantum automata were adopted in BIB003 , BIB004 as the model of the systems: Definition 3.1 (Quantum automata BIB001 , BIB002 ): A quantum automaton is a 4-tuple A = (H, Act , {U α : α ∈ Act}, H 0 ), where: 1) H is a finite-dimensional Hilbert space, called the state space; 2) Act is a finite set of action names; 3) for each action name α ∈ Act, U α is a unitary operator on H; 4) H 0 ⊆ H is the subspace of initial states. A quantum automaton behaves as follows: it starts from some initial state in H 0 , and at each step it performs a unitary transformation U α for some α ∈ Act. An algorithm for checking certain linear-time properties (e.g. invariants and safety properties) was proposed in BIB003 , where following Birkhoff-von Neumann quantum logic  , closed subspaces of the state Hilbert space are used as the atomic propositions about the state of system, and the checked linear-time properties are defined as infinite sequences of sets of atomic propositions. Furthermore, decidability or undecidability of several reachability problems (namely, eventually reachable, globally reachable, ultimately forever reachable, and infinitely often reachable) for quantum automata were established in BIB004 .