Conformance test sequences for communicationprotocols specified by finite state machines (FSM)often use unique input/output (UIO) sequences todetect state transition transfer faults. Since a UIOsequence may not exist for every state of an FSM, inthe previous research, we extended UIO sequence tointroduce a new concept called narrow input/output(NIO) sequence. The general computation of NIOsequences may lead to state explosion when an FSM isvery large. In this paper, we present an approach tofind NIO sequences using symbolic model checking.Constructing a Kripke structure and a computationtree logic (CTL) formula for such a purpose isdescribed in detail. We also illustrate the methodusing a model checker SMV.