# A Survey on Dynamic Corrective Control of Asynchronous Sequential Machines
## 2 Mathematical Formulation of Corrective Control
### Modeling of ASMs  
ASMs in corrective control have one of two types of dynamics: input/state machines in which the current state is given as the output, and input/output machines in which the output different from the state is provided. The modeling formalism for input/state ASMs is addressed in [16; 27; 28], and that for input/output ASMs in [29; 30; 31]; see also [32; 33] for general theory on switching and finite automata.  
An input/state ASM \(\Sigma\) is described by a quadruple  
\[\Sigma=(A,X,\bar{x},f),\]  
where \(A\) is the input set, \(X\) is the state set with \(|X|=n\), \(\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\). The behavior of \(\Sigma\) is characterized by the distinction between stable and transient states. If \(f(x,v)=x\), \((x,v)\in X\times A\) is a stable pair; if \(f(x,v)\
eq x\), \((x,v)\) is a transient one. In the absence of a synchronizing clock, \(\Sigma\) stays at a stable state \(x^{0}\in X\) indefinitely as long as the current input remains unchanged. If the input changes to another value \(a\in A\) such that \((x^{0},a)\) is transient, \(\Sigma\) engages in a chain of transient transitions  
\[x^{1}:=f(x^{0},a),x^{2}:=f(x^{1},a),\ldots, \tag{1}\]  
where \(a\) remains fixed. If \(\Sigma\) does not possess infinite cycles, \(\Sigma\) reaches the next stable state \(x^{k}\) such that  
\[x^{k}:=f(x^{k-1},a)=f(x^{k},a),\ 1\leqslant k\leqslant n-1. \tag{2}\]  
As transient transitions of ASMs are very fast, intermediate transient states \(x^{1},\ldots,x^{k-1}\) are almost imperceptible. Thus one often omits them and describes the chain of transient transitions only in terms of stable states. The stable recursion function \(s:X\times A\to X\)[28], plays the role of the latter compression. For a valid pair \((x,v)\in X\times A\),  
\[s(x,v):=x^{\prime}\]  
where \(x^{\prime}\) is the next stable state of \((x,v)\). The chain of transient transitions represented by \(s\) is termed a stable transition. The domain of \(s\) is often extended to \(X\times A^{+}\) as  
\[s(x,v_{1}v_{2}\cdots v_{k}):=s(s(x,v_{1}),v_{2}\cdots v_{k}),\ v_{1}v_{2} \cdots v_{k}\in A^{+}.\]  
When \(\Sigma\) has the form of an input/output ASM, it is represented by a six-tuple  
\[\Sigma=(A,Y,X,\bar{x},f,h),\]  
where \(Y\) is the output set and \(h:X\to Y\) is the output function.  
When \(\Sigma\) undertakes a stable transition, it generates a burst, or fast outburst of output characters. If \(\Sigma\) is an input/state ASM, it gives a state burst. If \(\Sigma\) is an input/output ASM, an output burst is generated instead. Since repeating characters are not noticeable in the dynamics of ASMs, they must be interpreted as a single one in the burst. Let \(\beta(x,v)\in X^{+}\cup Y^{+}\) be the burst \(\Sigma\) generates when it engages in a stable transition from \((x,v)\). In view of (1) and (2), \(\beta(x^{0},a)\) is written as\[\beta(x^{0},a):=\begin{cases}x^{0}x^{1}\cdots x^{k}&\text{input/state ASM}\\ \gamma(h(x^{0})h(x^{1})\cdots h(x^{k}))&\text{input/output ASM}\end{cases}\]  
where \(\gamma:Y^{+}\to Y^{+}\) is the mapping that replaces repeating characters by one. Note that the burst formulation of input/state ASMs needs not involve \(\gamma\) since no repeating states appear in them.