Deriving adaptive checking sequence for nondeterministic Finite State Machines

The derivation of checking sequences for Finite State Machines (FSMs) has a long history. There are many papers devoted to deriving a checking sequence that can distinguish a complete deterministic specification FSM from any non-equivalent FSM with the same number of states. To the best of our knowledge, for nondeterministic FSMs, the topic appeared only recently; the authors started with preset checking sequences for FSMs where the initial state is still known but the reset is very expensive. In this paper, a technique is proposed for deriving an adaptive checking sequence for a complete nondeterministic finite state machine with respect to the reduction relation. The main contribution of the paper is the use of a (adaptive) distinguishing test case instead of a separating sequence. Such a test case is usually shorter that a separating sequence (when it exists) and can exist when there is no separating sequence. We also discuss the possibilities of using adaptive transfer sequences instead of deterministic transfer sequences that also allows to extend the set of FSMs for which the strategy can be used and reduce the length of a checking sequence. The application of a proposed strategy to partial possibly nondeterministic FSMs is briefly discussed.