d abstract) Gaoyan Xie, Cheng Li, and Zhe Dang School of Electrical Engineering and Computer Science Washington State University Pullman, WA 99164, USA Abstract. In this paper, we introduce oracle (finite) automata that are finite/Buchi automata augmented with oracles in some classes of formal languages. We present some testability results for the emptiness problem of oracle automata associated with various classes of oracles. Moreover, we show that some important verification problems (such as reachability, safety, LTL model-checking, etc.) for oracle automata can be reduced to testing the emptiness of oracle automata. Our theory results on the testability of oracle automata can find applications in the verification of a system containing unspecified/partially specified components.