On Preset Homing and Synchronizing Sequences for Observable Input/Output Automata

The paper is devoted to the problem of deriving synchronizing and homing experiments for nondeterministic Input/Output automata; corresponding input sequences are widely used in testing (non-initialized) discrete event systems. In active testing, there is an opportunity to set a system under test into a known initial state; in passive testing, a known current state allows to reduce the number of properties to be checked. In the paper, we note that such experiments for Input/Output automata are different from so-called gedanken experiments with classical Finite State Machines; the existence check conditions of such experiments are established for a predefined discipline of applying inputs and a method for its derivation is proposed when such an experiment exists. The obtained results allow to reduce the problem of deriving synchronizing and homing experiments for Input/Output automata to the well developed problem of deriving such experiments for appropriate classes of Finite State Machines.

Automated summary

This paper focuses on deriving synchronizing and homing experiments for nondeterministic Input/Output automata. The authors establish the existence check conditions and propose a method for deriving such experiments. This reduces the problem to the well developed problem of deriving experiments for appropriate classes of Finite State Machines.