# State-Bust Feedback Control for Fault Recovery of Input/State Asynchronous Sequential Machines
## 2 Preliminaries  
For a finite set \(D\), \(|D|\) is the cardinality of \(D\), and \(D^{+}\) is the set of non-empty strings made of characters in \(D\). For \(p,q\in D^{+}\), \(|p|\in\mathbb{N}\) is the length of \(p\), \(p\) is a _strict prefix_ of \(q\) if \(q=pr\) with \(r\in D^{+}\). \(sp(q)\subset D^{+}\) denotes the set of all strict prefixes of \(q\). We also denote \(N_{0}:=\{0,1,\ldots,n\}\) for some \(n\in\mathbb{N}\). Table 1 summarizes the notations used in this paper. ASMs are classified as input/state machines in which the current state is given as the output, and input/output ones that generate the output different from the state. In this study, we focus our concern on input/state ASMs. An input/state ASM \(\Sigma\) is modeled by a quadruple as follows:  
\[\Sigma=(A,X,\bar{x},f),\]  
where \(A\) is the input set, \(X=\{x_{1},\ldots,x_{n}\}\) with \(|X|=n\) is the state set, \(\bar{x}\in X\) is the initial state, and \(f:X\times A\to X\) is the state transition function partially defined on \(X\times A\). \(A\) is divided into \(A=A_{n}\dot{\cup}A_{d}\) where \(A_{n}\) and \(A_{d}\) are the set of normal and adversarial inputs, respectively. \((x,v)\in X\times A\) is valid if \(f(x,v)\) is defined. A valid pair \((x,v)\) is stable if \(f(x,v)=x\), and transient if \(f(x,v)\
eq x\). Let  
\[U(x) :=\{v\in A|f(x,v)=x\}\text{ and}\] \[T(x) :=\{v\in A|f(x,v)\
eq x\}\]  
denote the set of inputs that make stable and transient pairs with \(x\), respectively. Owing to the absence of a synchronizing clock, \(\Sigma\) responds only to the input change. It rests in a stable pair \((x^{0},a^{\prime})\) with \(a^{\prime}\in U(x^{0})\) indefinitely as long as \(a^{\prime}\) remains fixed. If \(a^{\prime}\) changes to another value \(a\in T(x^{0})\), \(\Sigma\) engages in a chain of transient transitions as follows:  
\[f(x^{0},a)=x^{1},f(x^{1},a)=x^{2},\ldots, \tag{1}\]  
while \(a\) remains fixed. Provided that \(\Sigma\) possesses no infinite cycles, \(\Sigma\) reaches the next stable state as follows:  
\[f(x^{k},a)=f(x^{k-1},a)=x^{k} \tag{2}\]  
after \(k\) steps, where \(1\leq k\leq n-1\). As transient states are traversed instantaneously, it is convenient to describe this chain of transitions only in terms of stable states, omitting instantaneous transient transitions. To this end, the stable recursion function \(s\)[1,9] is defined on every valid pair as follows:  
\[s:X\times A\to X,\;s(x,v):=x^{\prime},\] \begin{table}
\begin{tabular}{c c} \hline \hline
**Symbol** & **Definition** \\ \hline \(\Sigma\), \(\Sigma^{\prime}\) & Input/state ASM \\ \(C\) & Static corrective controller \\ \(G\) & Diagnoser \\ \(A\) & Input set \\ \(A_{n}\), \(A_{d}\subset A\) & Normal and adversarial input set \\ \(X\) & State set \\ \(U(x)\subset A\) & Set of inputs making stable pairs with \(x\in X\) \\ \(T(x)\subset A\) & Set of inputs making transient pairs with \(x\in X\) \\ \(f\) & State transition function of \(\Sigma\) \\ \(s\), \(s^{\prime}\) & Stable recursion function of \(\Sigma\) and \(\Sigma^{\prime}\) \\ \(\alpha(x,u)\in X^{+}\) & State burst with respect to \(x\in X\) and \(u\in A\) \\ \(z_{f},z_{l}\in X\) & First and last element of state burst \(z\in X^{+}\) \\ \(W(x)\subset A_{d}\) & Set of adversarial inputs that occur at \(x\in X\) \\ \(\Gamma(x)\subset X\) & Set of states reached as a result of \(W(x)\) \\ \hline \hline \end{tabular}
\end{table} 
Table 1: Nomenclature. where \(x^{\prime}\) is the next stable state of \((x,v)\). If \((x,v)\) is a stable pair, \(s(x,v):=x\). The chain of transient transitions characterized by \(s\) is termed a _stable transition_.