Initial-State Observability of Mealy-Based Finite-State Machine With Nondeterministic Output Functions

In mobile systems or the failure detection applications, the output for some input event is state-dependent and nondeterministic after intermittent sensor failures or measurement uncertainties, which does not hold under the conventional observability hypothesis. In this article, such cases can be modeled by a Mealy-based finite-state machine (FSM) with nondeterministic output functions, and we investigate the ``initial-state'' observability by use of matrix semitensor product (matrix-STP). First, to characterize the nondeterministic output functions, a virtual state set consisting of state-event pairs is introduced to obtain an augmented FSM. By resorting to the matrix-STP, the algebraic expression of augmented FSM is proposed. Subsequently, based on the newly constructed model, the initial-state observability can be verified by checking the distinguishability of state trajectories of the augmented FSM. Meanwhile, the necessary and sufficient condition for such initial-state observability is derived from a discriminant matrix consisting of polynomial elements. Finally, numerical examples show the validity of the proposed method. The current results are further conducive to explore the critical safety of cyber-physical systems in many real-world systems.