text:
\section{Introduction}

\IEEEPARstart{I}{n} this paper, we investigate the state estimation problem for supervisor synthesis in networked discrete event systems (DES).
This problem can be briefly stated as: estimate all the states of the controlled system (plant) online under communication delays and losses, given that all the future control decisions are unknowable.
The supervisory control problem in DES is to find a supervisor (feedback controller) such that the language generated by the controlled system  is equal to a given specification language (desired behaviors), i.e., the \textsl{supervisor existence problem}\cite{lafortune07book}.
This problem is first studied under full observations in \cite{ramadge1987supervisory}, and then under partial observations in \cite{lin88is}.
After that, the supervisory control problem has been widely investigated in different directions, such as, robust supervisory control \cite{lin93tac}, decentralized supervisory control \cite{lin88isb,rudie92tac},  quantitative supervisory control \cite{ji21tac}, and online supervisory control \cite{heymann94deds}, etc.
However, in many applications, the specification language cannot be achieved exactly.
In such situations, one would like to synthesize a supervisor such that the language generated by the controlled system always consists in the specification language \cite{1990Formulas,heymann94deds,1996Centralized,2002Effective,2015Relative}, which is known as the \textsl{supervisor synthesis problem}.
This problem is one of the core problems in supervisory control and  has been well studied by Yin and Lafortune in \cite{yin16tac1,yin16tac2,yin17tac,yin18tac} over the past few years.
The effective implementation of approaches concerning the \textsl{supervisor synthesis problem} relies on online state estimation of the controlled system.

Nowadays, technological advancements of networks have enabled us to connect the supervisor and the plant via  a shared communication network.
Such a networked structure provides more flexible and agile ways for controlling DES.
For example, it allows the supervisor to be an edge computing node, which can share the computing resource with other edge computing nodes.
Recently, the \textsl{supervisor existence problem}  \cite{lin2014control,shu17tac2,zhao17tcns, rashidinejad18wodes,zhu19cdc,alves20tac} and \textsl{supervisor synthesis problem} \cite{liu21tac, wang15cdc, shu15tac, hou20tac,shu17tac1} in the context of networked DES have draw much attention in the literature.
Especially, when it comes to the  \textsl{supervisor synthesis problem},  communication delays and losses existing in the networks pose significant challenges on realizing accurate state estimation.
Most of the current works realize state estimation based on the open-loop system without using the information of control actions executed by the actuator \cite{wang15cdc, shu15tac,shu17tac1,2019State, hou20tac,lin20tcns,yue20csl,zhou21tase}.
The state estimates in  \cite{wang15cdc, shu15tac,shu17tac1,2019State, hou20tac,lin20tcns,yue20csl,zhou21tase} are conservative in the sense that they may contain states of which the controlled system is not in, when they are used for supervisor synthesis.
One exception is the work of \cite{liu21tac}, where the authors proposed a novel online state estimation algorithm  by taking  the information of control decisions history into consideration.
Nevertheless, this approach considers only control delays.
How to estimate states of a controlled system online under communication delays and losses remains open.
This is the primary motivation of this paper.

As in \cite{lin2014control,zhu19cdc,liu21tac}, this paper assumes that  i)  both the control channel and the observation channel satisfy first-in-first-out (FIFO);
ii) the observation delays and the control delays are upper bounded by $N_o$ and $N_c$ event occurrences (observable or not), respectively;
iii) the numbers of consecutive observation losses  and  consecutive control losses are no larger than $N_{l,o}$ and $N_{l,c}$, respectively.
This paper answers the following two questions.

1) How do we specify the language generated by the controlled system under communication delays and losses?
In this paper, we represent the networked supervisor as an automaton.
To solve the first problem, we construct a networked control model whose states record: (i)
the state that the plant is in, (ii) the state that the networked supervisor is in, (iii) the sequence of observable events has occurred but still needs to be delivered to the supervisor, (iv) the number of consecutive observation losses, (v) the control action being in use,
(vi) the sequence of control actions has been issued but still delayed at the control channel, and (vii) the number of consecutive control losses.
To describe communication delays and losses, the states of the networked control model are updated when one of the following behaviors happens (represented as a special event occurrence): (a) a new event occurs, (b) a new observable event is communicated, (c) a new control action is executed, (d)  an observation loss occurs, and (e) a control loss occurs.
It is shown that the dynamics of the controlled system can be simply ``decoded''  from sequences generated by the networked control model.

2) How do we online estimate states of the controlled system subject to communication delays and losses?
To solve this problem, the states of the plant, the states of the observation channel, and the states of the control channel are tracked simultaneously, during the evolution of the controlled system.
Specifically, for tracking states of the observation channel, we introduce the notion of ``observation channel configuration'', which consists of two parts: (i) a sequence of event-integer pairs that is used to track the delayed observable event occurrences and the number of observation delays, and (ii) an integer that is used to track the number of consecutive observation losses.
On the other hand, for tracking states of the control channel, we introduce the notion of ``control channel configuration'', which consists of three parts: (a) an admissible control action that is taking effect, (b) a sequence of command-integer pairs that is used to track the delayed control actions and the number of control delays, and (c) an integer that is used to track the number of consecutive control losses.
By incorporating the control and observation channel configurations into states of the plant, we can obtain a triplet.
We call such a triplet as an augmented state (the plant state augments with the observation and control channel configurations).
An online approach is proposed for updating the augmented state estimates upon each new observation, which can be used to estimate states of the controlled system.

To solve the \textsl{supervisor synthesis problem} in non-networked DES, the authors in \cite{yin16tac1} proposed a game structure called \textsl{All Inclusive Controller} (AIC) that embeds all the safe supervisors.
Using techniques developed in this paper, we show that the AIS can be easily extended to its networked counterpart, called \textsl{All Inclusive Networked Controller} (AINC).
The AINS includes all the safe networked supervisors, and we can always select a maximally-permissive one from them.

The rest of this paper is organized as follows.
Section II
presents some preliminary concepts and the required assumptions in this paper. Section III specifies the language generated by the controlled system subject to communication delays and losses. An online procedure for estimating states of the controlled system is presented in Section IV. Section V shows the application of techniques developed in this paper. Section VI
concludes this paper.

\section{Preliminaries}
A DES is modeled by a deterministic finite-state automaton
$
G=(Q, \Sigma,\delta,\Gamma, q_{0}, Q_m),
$
where $Q$ is the finite set of states; $\Sigma$ is the finite set of events; $\delta: Q\times \Sigma \rightarrow Q$ is the transition function; $\Gamma: Q \rightarrow 2^{\Sigma}$ is the active events set; $q_{0}$ is the initial state; and $Q_m \subseteq Q$ is the set of marked states.
$\delta$ is extended to $Q \times \Sigma^{\ast}$ in the usual way.
``!'' means ``is defined''.
$\mathscr{L}(G)$ is the language generated by $G$.
$\Sigma$ is partitioned into the set of controllable events
$\Sigma_c$ and the set of uncontrollable events $\Sigma_{uc}$.
$\Sigma$ is also partitioned into the set of observable events
$\Sigma_{o}$ and the set of unobservable events $\Sigma_{uo}$.
The natural projection $P: \mathscr{L}(G) \rightarrow \Sigma_{o}^{\ast}$ is defined as $P(\varepsilon)=\varepsilon$ and, for all $s, s\sigma \in\mathscr{L}(G)$, $P(s\sigma)=P(s)\sigma$ if $\sigma \in \Sigma_{o}$, and  $P(s\sigma)=P(s)$ otherwise.
Given automata $G_{1}$ and $G_{2}$, we say $G_1$ is a sub-automaton of $G_2$, denoted by $G_1 \sqsubseteq G_2$, if $G_1$ and $G_2$ have the same initial state and $G_1$ is a subgraph of $G_2$.

Given a string $s$, let $\overline{\{s\}} = \{s': (\exists s'') s = s's''\}$ be the set of all prefixes of $s$.
The length of a string $s$ is denoted by $|s|$.
The prefix-closure of a language $L\subseteq \Sigma^{\ast}$ is denoted as $\overline{L}$. $L$ is prefix-closed if $L=\overline{L}$.
We only consider prefix-closed languages in this paper.
Therefore, we assume that $Q=Q_m$ and denote an automaton by $G=(Q, \Sigma,\delta, \Gamma, q_{0})$.
$\varepsilon$ denotes the empty string.
Given a $s=\sigma_1\sigma_2\cdots\sigma_k$, we write $s^i = \sigma_1 \cdots \sigma_i$ for $i = 1,\ldots,k$, and $s^0 = \varepsilon$.
$\mathbb{N}$ is the set of natural numbers.
Given $a,b\in \mathbb{N}$, let $[a,b]$ be the set of natural numbers between $a$ and $b$.
The cardinality of a set  $Z$ is denoted by $|Z|$.
Given a $n \in \mathbb{N}$, let $Z^{\le n}$ be the set of queues of elements in $Z$ with the length no larger than $n$.

\begin{figure}
	\begin{center}
		\includegraphics[width=8.8cm]{fig1.pdf}
		\caption{Supervisory control for networked DES with communcation delays and losses.}
		\label{Fig1}
	\end{center}
\end{figure}

{As depicted in Fig.\ref{Fig1}, we consider a networked DES in this paper, where communications from the plant to the supervisor for observation and from the supervisor to the plant for control are achieved over a network.}
Due to the network characteristics, communication delays and losses exist for both
control and observation. We make the following assumptions on the networked DES.
\begin{enumerate}
\item Both the control channel and the observation channel satisfy the FIFO property, i.e., the observable event occurrences are delievered to the supervisor in the same order as they were generated and the control actions are executed by the actuator of the plant in the same order as they were issued;
\item  The communication delays in the observation (regarded as observation delays) are nondeterministic, but upper bounded by $N_o$ events, i.e., before an occurred event is observed, the system can generate no more than $N_o$ event occurrences. The communication delays in the control (regarded as control delays) are also nondeterministic, but upper bounded by $N_c$ events, i.e., before an issued control action is executed, the system can generate no more than $N_c$ event occurrences;
\item  The consecutive losses of observable event occurrences are assumed to be no larger than $N_{l,o}$, i.e., before a new observable event is communicated (observed), there are at most $N_{l,o}$ consecutive observation losses, and the consecutive losses of control actions are assumed to be no larger than $N_{l,c}$, i.e., before a new control action is extcuted, there are at most $N_{l,c}$ consecutive control losses;
\item  The actuators always implement the most recently received action, and the intial control action can be executed without any delays and losses because it can be executed beforehand.
\end{enumerate}

\begin{remark}
In this paper, we assume that both the control channel and the observation channel satisfy FIFO, since it is often the case there is only one communication channel from the plant to the supervisor and from the supervisor to the actuator.
This is slightly different from \cite{lin2014control,shu15tac,shu17tac1,shu17tac2, liu21tac}, where FIFO is not required for the control channel, and \cite{ rashidinejad18wodes}, where FIFO is not required for the observation channel.
Besides, since the communication losses are usual small, we also assume that both the consecutive observation losses and the  consecutive control losses are  with upper bounds.
The same assumption can  be found in \cite{zhu19cdc}.
Meanwhile, the delays are measured by the number of event occurrences (observable or not).
When time needs to be considered explicitly as in \cite{ rashidinejad18wodes,alves20tac}, we can introduce a new event
to denote the passage of a unit of time in the system model.
Observation and control delays can then be measured
using the number of newly introduced events have occurred.
\end{remark}

The networked supervisor is defined as a pair $S=(A,\gamma)$ such that $A=(X,\Sigma_o,\zeta,x_0)$\footnote{Here, we assume that $X$ is a finite set because all the networked supervisors considered in this paper can always be represented by an automaton with finite state spaces.} is a deterministic automaton with $\mathcal{L}(A)=\Sigma_o^*$, and $\gamma: X \rightarrow 2^\Sigma$ is a function specifies the set of events to be enabled.
Specifically, for any $t \in \Sigma_o^*$, we denote $\gamma(\zeta(x_0,t))$ by the set of events to be enabled after observing $t$.
With a slight abuse of notation, we also write $\gamma(\zeta(x_0,t))=S(t)$.
Let $\Pi=\{\pi\in 2^{\Sigma}:\Sigma_{uc}\subseteq \pi\}$ be the set of all the admissible control actions.
Since we can not disable an uncontrollable event, $S(t)$ should be admissble, i.e., $S(t)\in \Pi$.

\begin{figure}
\centering \subfigure[$G$]{\label{Fig21}\includegraphics[width=4.0cm]{fig1a.pdf}}
\subfigure[$S=(A,\gamma)$]{\label{Fig22}\includegraphics[width=3.9cm]{fig1b.pdf}}
\caption{System $G$ and networked supervisor $S=(A,\gamma)$  in Example \ref{Ex1}.} \label{Fig2}
\end{figure}
\begin{example}\label{Ex1}
Consider system $G$ depicted in Fig.\ref{Fig21} with $\Sigma_c=\Sigma=\{\alpha,\beta,\lambda\}$ and  $\Sigma_o=\{\alpha,\beta\}$.
The networked supervisor $S=(A,\gamma)$ is depicted in  Fig.\ref{Fig22}.
The function $\gamma$ is specified by the set of events associated with each
state in Fig.\ref{Fig22}.
As we can see, when $S$ is in the initial state, we have $S(\varepsilon)=\gamma(p_1)=\{\alpha\}$.
Once $\alpha$ is observed, $S$ moves to state $p_2$ and we have $S(\alpha)=\gamma(p_2)=\{\beta,\lambda\}$.
For all $t \in \Sigma^*_o \setminus \{\varepsilon,\alpha\}$, we have $S(t)=\gamma(p_3)=\emptyset$.
\end{example}

Given two networked supervisors $S_1$ and $S_2$, we say $S_1$ is smaller than $S_2$, denoted by $S_1 \subseteq S_2$, if $S_1(t)\subseteq S_2(t)$ for all $t\in \Sigma_o^*$; we say $S_1$ is strictly smaller than $S_2$, denoted by $S_1 \subset S_2$, if $S_1 \subseteq S_2$ and  there exists $t \in \Sigma_o^*$ such that $S_1(t)\subset S_2(t)$.

\section{Networked control model}

To estimate states of a controlled system,  we need to first specify the languages that can be generated by the controlled system (subject to communication delays and losses).
This is a challenging task because for the networked supervisor,  the observation for an occurred string is not deterministic but varies with different observation delays and losses.
For the same observation, the control action being in use can also be different due to control delays and losses.
To overcome these difficulties, we next construct a networked control model that describes explicitly the communication delays and losses occurring in the observation channel and the control channel.
We show that the ``dynamics'' of the controlled system can be inferred from the constructed  model.

Before we formally construct the networked control model, we first define four special types of events to characterize behaviors of communication delays and losses. Let $N=N_c+N_o$.
\begin{enumerate}

\item To describe the loss of an observable event occurrence, define bijection $o:[1,N_o+1] \rightarrow \Sigma^o$ such that  $\Sigma^o=\{o(i):i\in [1,N_o+1]\}$, where $o(i)$ denotes the loss of the $i$th observable event in the observation channel;

\item To describe the loss of  a control action, define bijection $c:[1,N+1] \rightarrow \Sigma^c$ such that $\Sigma^{c}=\{c(i):i\in [1,N+1]\}$, where $c(i)$ denotes the loss of the $i$th control action in the control channel;

\item To keep track of what observable event has been communicated, define bijection $f:\Sigma_o \rightarrow \Sigma^f$ such that $\Sigma^f=\{f(\sigma):\sigma \in \Sigma_o\}$, where $f(\sigma)$ means the occurrence of $\sigma$ has been communicated;

\item To model which control decision is taken, define bijection $g:\Pi \rightarrow \Sigma^g$ such that $\Sigma^g=\{g(\pi): \pi \in \Pi\}$, where $g(\pi)$ denotes the control action $\pi$ has been executed.

\end{enumerate}
Note that  $\Sigma$, $\Sigma^o$, $\Sigma^c$, $\Sigma^f$, and $\Sigma^g$ are mutually disjoint.

Given a system $G$ and a networked supervisor $S=(A,\gamma)$  such that $A=(X,\Sigma_o,\zeta,x_0)$, we denote each state of the networked control model by a seven-tuple $\tilde{q}=(q,x,n,\phi,y,m,p) \in  Q \times (\Sigma_o \times [0,N_o])^{\le N_o+1}\times [0,N_{l,o}] \times \Pi \times (\Pi \times [0,N_c])^{\le N+1}  \times [0,N_{l,c}] \times X$, where (i) $q \in Q$ tracks the state that plant $G$ is in; (ii) $x$ is a sequence of pairs $(\sigma_1,n_1) \cdots (\sigma_k, n_k) \in (\Sigma_o \times [0,N_o])^{\le N_o+1}$ such that $\sigma_1\cdots\sigma_k \in \Sigma_o^*$ tracks a sequence of observable events have occurred but still needs to be communicated (delivered) to the supervisor, and the integer $n_i$ tracks the number of event occurrences while $\sigma_i$ is waiting to be communicated;
(iii) $n \in [0,N_{l,o}]$  counts the number of consecutive observation losses;
(iv) $\phi \in \Pi$ is the control action being in use;
(v) $y$ is a sequence of pairs $(\pi_1,m_1) \cdots (\pi_h,m_h) \in (\Pi \times [0,N_c])^{\le N+1}$ such that  $\pi_1 \cdots \pi_h \in \Pi^{\le N+1}$ tracks a sequence of admissible control actions have been issued but  not been executed due to control delays, and the integer $m_i$ tracks the number of event occurrences while the control action $\pi_i$ is delayed at the control channel;
(vi) $m \in [0,N_{l,c}]$  counts the number of consecutive control losses;
(vii) $p\in X$ tracks the state that networked supervisor $S$ is in.

\begin{remark}
Note that the lengths of $x$ and $y$ are both finite.
The reasons are as follows. Since the observation delays are assumed to be upper bounded by $N_o$, there could be $N_o$ additional event occurrences at most before an occurred observable event is communicated.
Thus, the number of events delayed at the observation channel is $N_o+1$ at most, and the length of $x$ is no larger than $N_o+1$.
On the other hand, due to control delays and observation delays, the control action being in use could be any one issued in the past $N=N_c+N_o$ steps.
When a new event occurs, at least one control action issued in the past $N+1$ steps is executed.
Therefore, the length of $y$ is no longer than $N+1$.
\end{remark}

Given a $x \in (\Sigma_o \times [0,N_o])^{\le N_o+1}$, if $x=(\sigma_1,n_1) \cdots (\sigma_k, n_k) \neq \varepsilon$, define $\textbf{NUM}(x)=n_1$ as the integer in the first pair of $x$, and if $x=\varepsilon$, define $\textbf{NUM}(x)=0$.
Since $\sigma_1$ is the first event queued at the observation channel, $\textbf{NUM}(x)$ records the maximum observation delays at the moment.
Also, for recording the observation delays after a new event occurrence, define $x^+=(\sigma_1,n_1+1) \cdots (\sigma_k,n_k+1)$ if $x=(\sigma_1,n_1) \cdots (\sigma_k, n_k) \neq \varepsilon$, and $x^+=\varepsilon$ if $x=\varepsilon$.
Similarly, for any $y \in (\Pi \times [0,N_c])^{\le N+1}$, if $y=(\pi_1,m_1) \cdots (\pi_h, m_h) \neq \varepsilon$, define $y^+=(\pi_1,m_1+1) \cdots (\pi_h, m_h+1)$ and $\textbf{NUM}(y)=m_1$, and if $y=\varepsilon$, define $y^+=\varepsilon$ and $\textbf{NUM}(y)=0$.

Formally, we construct $G_S=(\tilde{Q},\tilde{\Sigma}, \tilde{\delta}, \tilde{\Gamma}, \tilde{q}_{0})$, where $\tilde{Q} \subseteq  Q \times (\Sigma_o \times [0,N_o])^{\le N_o+1}\times [0,N_{l,o}] \times \Pi \times (\Pi \times [0,N_c])^{\le N+1}  \times [0,N_{l,c}] \times X$ is the state space; $\tilde{\Sigma}=\Sigma \cup \Sigma^o \cup\Sigma^c \cup \Sigma^f \cup \Sigma^g$ is the event set; $\tilde{q}_{0}=(q_0, \varepsilon, 0, S(\varepsilon), \varepsilon, 0, x_0)$ is the initial state; the transition function $\tilde{\delta}: \tilde{Q} \times \tilde{\Sigma} \rightarrow \tilde{Q}$ is defined as follows:

\begin{itemize}

  \item For all $\tilde{q}=(q,x,n,\phi,y,m,p)\in \tilde{Q}$ and all $\sigma \in \Sigma$,
\begin{eqnarray} \begin{array}{lllllll}\label{Eq1}
  \tilde{\delta}(\tilde{q}, \sigma)= \begin{cases}
    \tilde{q}' & \text{if}\ \delta(q,\sigma)! \wedge \sigma \in \phi \\
&\wedge  \textbf{NUM}(x)+1 \le N_o\\
& \wedge \textbf{NUM}(y)+1 \le N_c\\
    \mbox{undefined} & \mbox{otherwise,}
  \end{cases}
  \end{array}  \end{eqnarray}
with $\tilde{q}' =(q',x',n',\phi',y',m',p')$, where (i) $q'=\delta(q,\sigma)$, (ii) if $\sigma \in \Sigma_o$, $x'=x^+(\sigma,0)$, and if $\sigma \in \Sigma_{uo}$, $x'=x^+$, (iii) $n'=n$, (iv) $\phi'=\phi$, (v) $y'=y^+$, (vi) $m'=m$, and (vii)  $p'=p$.

  \item For all $\tilde{q}=(q,x,n,\phi,y,m,p)\in \tilde{Q}$ and all $o(i) \in \Sigma^o$,  if $x=\varepsilon$, $\tilde{\delta}(\tilde{q},o(i))$ is not defined, and if $x \neq \varepsilon$, we write $x=(\sigma_1,,n_1) \cdots (\sigma_k,n_k)$ for $\sigma_j \in \Sigma_o$ and $n_j \in [0,N_o]$, and then,
\begin{eqnarray} \begin{array}{lllllll}\label{Eq2}
  \tilde{\delta} (\tilde{q}, o(i))= \begin{cases}
    \tilde{q}' & \text{if}\ i \in [1,k] \wedge n+1 \le N_{l,o}\\
    \mbox{undefined} & \mbox{otherwise,}
  \end{cases}
  \end{array}  \end{eqnarray}
with $\tilde{q}' =(q',x',n',\phi',y',m',p')$, where  (i) $q'=q$, (ii) $$x'=(\sigma_1,n_1) \cdots (\sigma_{i-1},n_{i-1})(\sigma_{i+1},n_{i+1})\cdots (\sigma_k,n_k),$$
(iii) $n'=n+1$, (iv) $\phi'=\phi$, (v) $y'=y$,  (vi) $m'=m$, and (vii) $p'=p$.

\item For all $\tilde{q}=(q,x,n,\phi,y,m,p)\in \tilde{Q}$ and all $f(\sigma) \in \Sigma^f$, if $x=\varepsilon$, then $\tilde{\delta}(\tilde{q},f(\sigma))$ is not defined,
and if $x \neq \varepsilon$, we write $x=(\sigma_1,n_1) \cdots (\sigma_k,n_k)$ for $\sigma_j \in \Sigma_o$ and $n_j \le N_o$, and then,
\begin{eqnarray} \begin{array}{lllllll}\label{Eq4}
  \tilde{\delta} (\tilde{q}, f(\sigma))= \begin{cases}
    \tilde{q}' & \text{if}\ \sigma=\sigma_1\\
    \mbox{undefined} & \mbox{otherwise,}
  \end{cases}
  \end{array}  \end{eqnarray}
with $\tilde{q}' =(q',x',n',\phi',y',m',p')$, where  (i) $q'=q$, (ii) $x'=(\sigma_2,n_2) \cdots (\sigma_k,n_k)$, (iii) $n'=0$, (iv) $\phi'=\phi$, (v) $y'=y(\gamma(\zeta(p,\sigma)),0)$, (vi) $m'=m$, and (vii) $p'=\zeta(p,\sigma)$.

\item For all $\tilde{q}=(q,x,n,\phi,y,m,p)\in \tilde{Q}$ and all $c(i) \in \Sigma^c$, if $y=\varepsilon$, $\tilde{\delta}(\tilde{q},c(i))$ is not defined,
and if $y \neq \varepsilon$, we write $y=(\pi_1,m_1) \cdots (\pi_h,m_h)$ for $\pi_j \in \Pi$ and $m_j \le N_c$, and then,
\begin{eqnarray} \begin{array}{lllllll}\label{Eq3}
  \tilde{\delta}(\tilde{q}, c(i))= \begin{cases}
    \tilde{q}' & \text{if}\ i \in [1,h] \wedge m+1 \le N_{l,c}\\
    \mbox{undefined} & \mbox{otherwise,}
  \end{cases}
  \end{array}  \end{eqnarray}
with $\tilde{q}' =(q',x',n',\phi',y',m',p')$, where  (i) $q'=q$, (ii) $x'=x$, (iii) $n'=n$, (iv) $\phi'=\phi$,  (v) $$y'=(\pi_1,m_1) \cdots (\pi_{i-1},m_{i-1})(\pi_{i+1},m_{i+1})\cdots (\pi_h,m_h),$$  (vi) $m'=m+1$, and (vii) $p'=p$.

  \item For all $\tilde{q}=(q,x,n,\phi,y,m,p)\in \tilde{Q}$ and all $g(\pi) \in \Sigma^g$, if $y=\varepsilon$, $\tilde{\delta}(\tilde{q},g(\pi))$ is not defined,
and if $y \neq \varepsilon$, we write $y=(\pi_1,m_1) \cdots (\pi_h,m_h)$ for $\pi_j \in \Pi$ and $m_j \le N_c$, and then,
\begin{eqnarray} \begin{array}{lllllll}\label{Eq5}
  \tilde{\delta} (\tilde{q}, g(\pi))= \begin{cases}
    \tilde{q}' & \text{if}\ \pi=\pi_1\\
    \mbox{undefined} & \mbox{otherwise,}
  \end{cases}
  \end{array}  \end{eqnarray}
with $\tilde{q}' =(q',x',n',\phi',y',m',p')$, where  (i) $q'=q$, (ii) $x'=x$, (iii) $n'=n$, (iv) $\phi'=\pi$, (v) $y'=(\pi_2,m_2) \cdots (\pi_h,m_h)$, (vi) $m'=0$, and (vii) $p'=p$.

\end{itemize}

\begin{figure*}
	\begin{center}
		\includegraphics[width=18.4cm]{fig3.pdf}
		\caption{Networked control model $G_S$ in Example \ref{Ex2}}
		\label{Fig3}
	\end{center}
\end{figure*}

We interpret the construction of $G_S$ as follows.
In (\ref{Eq1}), $\sigma$ can occur at $\tilde{q}=(q,x,n,\phi,y,m,p)\in \tilde{Q}$ only if $\sigma$ is defined at $q$ in $G$, i.e., $\delta(q,\sigma)!$, the occurrence of $\sigma$ is allowed by the control action being in use, i.e., $\sigma \in \phi$, and the observation delays and control delays after the occurrence of $\sigma$ are no larger  than $N_o$ and $N_c$, respectively, i.e.,  {$\textbf{NUM}(x)+1 \le N_o  \wedge \textbf{NUM}(y)+1 \le N_c$}.
If $\sigma$ occurs at $\tilde{q}$,   since $q$ is used to track the state that the plant is in, we have $q'=\delta(q,\sigma)$.
After the occurrence of $\sigma$, the delays for control actions queued at the control channel should plus 1. Hence, $y'=y^+$ in (\ref{Eq1}).
Furthermore, if $\sigma$ occurs at $\tilde{q}$ and $\sigma$ is unobservable,  we know the sequence delayed at the observation channel still is $x$ but all the numbers in $x$ (if $x \neq \varepsilon$) should plus 1 for counting the observation delays.
As we can see,  we set $x=x^+$ if $\sigma \in \Sigma_{uo}$ in (\ref{Eq1}).
However, if $\sigma \in \Sigma_o$, by FIFO, $(\sigma,0)$ should be added to the end of $x$, as $x'=x^+(\sigma,0)$ if $\sigma \in \Sigma_{o}$ in (\ref{Eq1}).
For the rest components in $\tilde{q}$,  the state of the supervisor can be updated only when a new event is communicated, and the control action being in use can be updated only when a new control action is executed.
Therefore, $p$ and $\phi$ have no change after the occurrence of $\sigma$, i.e., $p'=p$ and $\phi'=\phi$.
Also, since there are no control and observation losses,  $n'=n$ and $m'=m$.

For any $\tilde{q}=(q,x,n,\phi,y,m,p)\in \tilde{Q}$, if $x=\varepsilon$, the observation channel is empty.
Thus, no observable events can get lost or be communicated.
As we can see, if $x=\varepsilon$, $o(i)\in \Sigma^o$ is not defined at $\tilde{q}$ in (\ref{Eq2}), and $f(\sigma) \in \Sigma^f$ is not defined at $\tilde{q}$ in (\ref{Eq4}).
Otherwise, if $x=(\sigma_1,n_1)\cdots(\sigma_k,n_k) \neq \varepsilon$,  by assumption, all the observable events queued at the observation channel may get lost if the consecutive observation losses are not larger than $N_{l,o}$ after the observation loss.
Therefore,  if $n+1 \le N_{l,o}$,  $o(i)$ is defined at $\tilde{q}$ for all $i\in [1,k]$  in (\ref{Eq2}).
When $o(i)$ occurs at $\tilde{q}$, we remove $(\sigma_i,n_i)$ from $x$ and update $n$ to $n+1$ for recording the observation loss.
On the other hand, since $x=(\sigma_1,n_1)\cdots(\sigma_k,n_k)$, by FIFO,  $f(\sigma)$ is defined at $\tilde{q}$ iff  $\sigma=\sigma_1$ as in (\ref{Eq4}).
When the occurrence of $\sigma_1$ is communicated, the remaining sequence to be communicated will be $\sigma_2 \cdots \sigma_k$, which is illustrated by  $x'=(\sigma_2,n_2)\cdots(\sigma_k,n_k)$ in (\ref{Eq4}).
Following the communication of $\sigma_1$, the state of the supervisor is updated to $\zeta(p,\sigma)$, and the supervisor
sends $\gamma(\zeta(p,\sigma))$ to the actuator of the plant, which are illustrated respectively by $p'=\zeta(p,\sigma)$ and $y'=y(\gamma(\zeta(p,\sigma)),0)$ in (\ref{Eq4}).
Furthermore, since $n$ is used to count the number of consecutive observation losses,  we reset $n$ to $0$ after a new event communication, as $n'=0$ in (\ref{Eq4}).

For any $\tilde{q}=(q,x,n,\phi,y,m,p)\in \tilde{Q}$, if $y=\varepsilon$, the control channel is empty, and no control actions can get lost or be executed.
Thus, if $y=\varepsilon$, $c(i) \in \Sigma^c$ is not defined at $\tilde{q}$ in (\ref{Eq3}), and $g(\pi) \in \Sigma^g$  is not defined at $\tilde{q}$ in (\ref{Eq5}).
Otherwise, if  $y=(\pi_1,m_1) \cdots (\pi_h,m_h) \neq \varepsilon$, by assumption, all the control actions queued at the control channel may get lost if the consecutive control losses are no larger than $N_{l,c}$ after the control loss.
Hence, if $m+1\le N_{l,c}$,  $c(i)$ is defined at $\tilde{q}$ for all $i\in [1,h]$ in (\ref{Eq3}).
When $c(i)$ occurs at $\tilde{q}$, we remove $(\pi_i,m_i)$ from $y$ and update $m$ to $m+1$  for recording the control loss.
On the other hand, since  $y=(\pi_1,m_1) \cdots (\pi_h,m_h) \neq \varepsilon$, by FIFO, $g(\pi)$ is defined at $\tilde{q}$ iff $\pi=\pi_1$.
When $g(\pi)$ occurs at $\tilde{q}$, the control action taking effect becomes $\pi$, and the control actions queued at the control channel are $\pi_2\cdots\pi_h$, which are illustrated respectively by  $\phi'=\pi$ and $y'=(\pi_2,m_2) \cdots (\pi_h,m_h)$ in (\ref{Eq5}).
Since $m$ is used to count the number of consecutive control losses, we reset $m$ to $0$ in (\ref{Eq5}) when a new control action is executed.

Example \ref{Ex2} further illustrates how to construct the networked control model $G_S$.
\begin{example}\label{Ex2}
Consider the system $G$ and the networked supervisor $S$ depicted, respectively, in Fig.\ref{Fig21} and  Fig.\ref{Fig22}.
Let $\Sigma_c=\Sigma$ and $\Sigma_o=\{\alpha,\beta\}$.
Also, let $N_c=N_o=N_{l,c}=N_{l,o}=1$.
The networked control model $G_S$ is constructed in Fig.\ref{Fig3}.

Let us take the initial state $\tilde{q}_0=(q_1,\varepsilon, 0,\{\alpha\},\varepsilon,0,p_1)$ for example.
We write $\phi=S(\varepsilon)=\{\alpha\}$ and $x=y=\varepsilon$.
Since the control channel is empty, no control actions can be executed or get lost.
Hence, all the events in $\Sigma^c$ and $\Sigma^g$ are not defined at $\tilde{q}_0$.
Similarly, since the observation channel is empty, all the events in $\Sigma^o$ and $\Sigma^f$ are also not defined at $\tilde{q}_0$.
By Fig.\ref{Fig21}, $\delta(q_1,\alpha)=q_2$.
Moreover, since $\alpha \in \Sigma_o$, $\alpha \in \phi$, $\textbf{NUM}(x)+1=1 \le N_c$, and $\textbf{NUM}(y)+1=1 \le N_o$, by (\ref{Eq1}), we have $\tilde{\delta}(\tilde{q}_0,\alpha)=\tilde{q}_1=(q_2,(\alpha,0),0,S(\varepsilon),\varepsilon,0,p_1)$.

Next, let us consider state $\tilde{q}_1=(q_2,(\alpha,0),0,\{\alpha\},\varepsilon,0,p_1)$.
We write $x'=(\alpha,0)$, $\phi'=\phi=\{\alpha\}$, and $n'=0$.
By Fig.\ref{Fig21}, we know $\delta(q_2,\beta)=q_4$ and  $\delta(q_2,\lambda)=q_3$.
However, since $\beta,\lambda \notin \phi'$, by (\ref{Eq1}), $\beta$ and $\lambda$ are not defined at $\tilde{q}_1$.
Moreover, since $x'=(\alpha,0)\neq \varepsilon$, by (\ref{Eq4}), $f(\alpha)$ is defined at $\tilde{q}_1$.
When $\sigma$ is communicated to the supervisor, $S$ moves to state $\zeta(p_1,\alpha)=p_2$, and a new control action $\gamma(p_2)=\{\beta,\lambda\}$ is issued.
By (\ref{Eq4}),  $\tilde{\delta}(\tilde{q}_1,f(\alpha))=(q_2,\varepsilon,0,\{\alpha\},(\{\beta,\lambda\},0),0,p_2)$.
Meanwhile, since $x'=(\alpha,0)\neq \varepsilon$ and $n'+1=1\le N_{l,o}$, by (\ref{Eq2}), $\tilde{\delta}(\tilde{q}_1,o(1))=(q_2,\varepsilon,1,\{\alpha\},\varepsilon, 0, p_1)$.
In this way, we can construct $G_S$.

\end{example}

Given a string $\mu \in \tilde{\Sigma}^*$, let $\psi(\mu)$ and $\psi^f(\mu)$ be the string obtained by removing all the events in $\tilde{\Sigma} \setminus \Sigma$ and $\tilde{\Sigma} \setminus \Sigma_f$  from $\mu$, respectively, without changing the order of the remaining events.
Define $f^{-1}$ as, for all $f(\sigma) \in \Sigma_f$, $f^{-1}(f(\sigma))=\sigma$.
We extend $\psi$, $\psi^f$, and $f^{-1}$ to a set of strings in the usual way.

\begin{example}\label{Ex3}
{Consider the networked control model $G_S$ depicted in Fig.\ref{Fig3}.
Take string $\mu=\alpha f(\alpha) c(1) \in \mathcal{L}(G_S)$ for example, which accounts for the case that the occurrence of $\alpha$ is communicated to the networked supervisor without any observation delays and losses, however, the control action issued after the communication of $\alpha$ gets lost.
By the definition of $\psi(\cdot)$, $\psi(\mu)=\alpha \in \mathcal{L}(G)$.
By the definitions of $\psi^f(\cdot)$ and $f^{-1}(\cdot)$, $\psi^f(\mu)=f(\alpha)$ and $f^{-1}(\psi^f(\mu))=\alpha$.
Clearly, $\psi(\mu)$ characterizes the string has occurred in $G$ under $S$, and  $f^{-1}(\psi^f(\mu))$ characterizes the string has been communicated after the occurrence of $\psi(\mu)$.}
\end{example}

Intuitively, 1) $\psi(\mathcal{L}(G_S))$  specifies all the languages that can be generated under  $S$, and 2) $f^{-1}(\psi^f(\mathcal{L}(G_S)))$ specifies all the behaviors that can be observed by the networked supervisor.
We formally prove them in the following proposition.

\begin{proposition}\label{Prop1}
Given a $\mu \in \mathcal{L}(G_S)$, let us write $\tilde{\delta}(\tilde{q}_0,\mu)=(q,x,n,\phi,y,m,p)$.
Then, we have (i) $q=\delta(q_0,\psi(\mu))$ and (ii) $p=\zeta(x_0,f^{-1}(\psi^f(\mu)))$.
\end{proposition}
\begin{proof}
The proof is by induction on the length of strings in $\mathcal{L}(G_S)$.
Since $\tilde{\delta}(\tilde{q}_0,\varepsilon)=(q_0,\varepsilon,0,S(\varepsilon),\varepsilon,0,x_0)$, $\delta(q_0,\varepsilon)=q_0$, and  $\zeta(x_0,\varepsilon)=x_0$, the base case is true.
The induction hypothesis is that for any $\mu \in \mathcal{L}(G_S)$ with $|\mu| \le n$, if we write $\tilde{\delta}(\tilde{q}_0,\mu)=(q,x,n,\phi,y,m,p)$, then $q=\delta(q_0,\psi(\mu))$ and  $p=\zeta(x_0,f^{-1}(\psi^f(\mu)))$.
We next prove the same is also true for $\mu e \in \mathcal{L}(G_S)$.
We write $\tilde{\delta}(\tilde{q}_0,\mu e)=(q',x',n',\phi',y',m',p')$.
By the definition of $\tilde{\Sigma}$,  $e \in \Sigma$, $e\in \Sigma^f$, or $e \in \tilde{\Sigma}\setminus (\Sigma \cup \Sigma^f)$.
We consider each of them separately as follows.

\emph{Case 1:} $e \in \Sigma$.
By (\ref{Eq1}), $q'=\delta(q,e)$ and $p'=p$.
Since $e \in \Sigma$, by definitions, we have $\psi(\mu e)=\psi(\mu)e$ and $f^{-1}(\psi^f(\mu e))=f^{-1}(\psi^f(\mu))$.
Moreover, since $q=\delta(q_0,\psi(\mu))$ and  $p=\zeta(x_0,f^{-1}(\psi^f(\mu)))$, we have $\delta(q_0,\psi(\mu e))=\delta(q,e)=q'$ and  $\zeta(x_0,f^{-1}(\psi^f(\mu e)))=\zeta(x_0,f^{-1}(\psi^f(\mu)))=p=p'$.

\emph{Case 2:} $e=f(\sigma) \in \Sigma^f$.
By (\ref{Eq4}), $q'=q$ and $p'=\zeta(p,\sigma)$.
Since $e \in \Sigma^f$, we have $\psi(\mu e)=\psi(\mu)$ and $f^{-1}(\psi^f(\mu e))=f^{-1}(\psi^f(\mu)) \sigma$.
Moreover, since $q=\delta(q_0,\psi(\mu))$ and  $p=\zeta(x_0,f^{-1}(\psi^f(\mu)))$, we have $\delta(q_0,\psi(\mu e))=\delta(q_0,\psi(\mu))=q=q'$ and  $\zeta(x_0,f^{-1}(\psi^f(\mu e)))=\zeta(x_0,f^{-1}(\psi^f(\mu))\sigma)=\zeta(p,\sigma)=p'$.

\emph{Case 3:} $e \in \tilde{\Sigma} \setminus (\Sigma \cup \Sigma^f)$.
By (\ref{Eq2}), (\ref{Eq3}), and (\ref{Eq5}), $q'=q$ and $p'=p$.
Since $e \in \tilde{\Sigma} \setminus (\Sigma \cup \Sigma^f)$,  $\psi(\mu e)=\psi(\mu)$ and $f^{-1}(\psi^f(\mu e))=f^{-1}(\psi^f(\mu))$.
Moreover, since $q=\delta(q_0,\psi(\mu))$ and  $p=\zeta(x_0,f^{-1}(\psi^f(\mu)))$, we have $\delta(q_0,\psi(\mu e))=\delta(q_0,\psi(\mu))=q=q'$ and  $\zeta(x_0,f^{-1}(\psi^f(\mu e)))=\zeta(x_0,f^{-1}(\psi^f(\mu)))=p=p'$.
\end{proof}

By Proposition \ref{Prop1}, the ``dynamics'' of the controlled system can be simply obtained by removing all the events in $\tilde{\Sigma}\setminus \Sigma$ from sequences generated by $G_S$.
This gives the following definition.

\begin{definition}\label{Def1}
Given a system $G$ and a networked supervisor $S=(X,\Sigma_o,\zeta,x_0)$, we construct $G_S$ as described above.
The languages generated by the controlled system under communication delays and losses, denoted by $\mathcal{L}(S/G)$, are defined as: $\mathcal{L}(S/G)=\psi(\mathcal{L}(G_S))$.
\end{definition}

\begin{proposition}\label{Prop}
Given two  $S_i=(X_i,\Sigma_o,\zeta_i,x_{0,i})$, $i \in \{1,2\}$,  we construct $G_{S_i}=(\tilde{Q}_i,\tilde{\Sigma},\tilde{\delta}_i,\tilde{\Gamma}_i,\tilde{q}_{0,i})$ as described above.
Then, if $S_1 \subseteq S_2$, $\mathcal{L}(S_1/G) \subseteq \mathcal{L}(S_2/G)$.
\end{proposition}
\begin{proof}
Please see Appendix A.
\end{proof}

Proposition \ref{Prop} tells us  that the more events a networked supervisor $S$ enables, the larger language $\mathcal{L}(S/G)$ the controlled system generates.
With above preparations, we next introduce the definition of networked state estimate (NSE) for a communicated string under $S$.
\begin{definition}\label{Def2}
Given a system $G$ and a networked supervisor $S$ defined over $\Sigma_o^*$, for any $t \in f^{-1}(\psi^f(\mathcal{L}(G_S)))$, define
\begin{align}\label{Eq6}
\mathcal{E}_S(t)=&\{q\in Q:(\exists \mu \in \mathcal{L}(G_S))\notag\\
&q=\delta(q_0,\psi(\mu))\wedge t=f^{-1}(\psi^f(\mu))\},
\end{align}
as the NSE of $t$ under $S$, which is the set of all the possible states that  plant $G$ can be in after observing $t$ (subject to communication delays and losses) under $S$.
\end{definition}

If $S$ is given beforehand, we can calculate $\mathcal{E}_S(t)$ by constructing an observer of $G_S$ with the set of observable events $\Sigma^f$ \cite{lafortune07book}.
However, when we solve the \textsl{supervisor synthesis problem}, $S$ is unknowable.
The state estimate should be calculated online right after each new observation without using future observations and controls  \cite{yin16tac1,yin16tac2,yin17tac,yin18tac}.
This is exactly the problem we want to solve in this paper.
The details will be discussed in the next section.

\section{Online networked state estimation}

{In this section, we discuss how to online estimate states of a controlled system under communication delays and losses.
This problem is very different from that in non-networked DES.
To determine which state the controlled system is in, we should not only track states of the plant, but also track control actions delayed at the control channel as well as observable event occurrences delayed at the observation channel.
Inspired by the work of \cite{liu21tac}, we  introduce the notions of \textsl{observation channel configuration} and \textsl{control channel configuration} as follows.}

\begin{definition}\label{DefI}
The {observation channel configuration} is defined as: $\theta_o=((\sigma_1,n_1)\cdots (\sigma_k,n_k), n),$
where $(\sigma_1,n_1)\cdots (\sigma_k,n_k)\in (\Sigma_o \times [0,N_o])^{\le N_o+1}$ is sequence of pairs such that $\sigma_1\cdots\sigma_k$ is a sequence of observable events currently delayed at the observation channel (in the same order as they were generated), and $n_i$ is the number of event occurrences since $\sigma_i$ has occurred, and $n\in [0,N_{l,o}]$ tracks the number of consecutive observation losses.
\end{definition}

We denote by $\Theta_o \subseteq (\Sigma_o \times [0,N_o])^{\le N_o+1} \times [0,N_{l,o}]$ the set of all the possible observation channel configurations.
By Definition \ref{DefI},  it can be verified that $\theta_o$ is updated when one the following three behaviors happens: (i) an event occurs, (ii) an observable event is communicated, (iii) an observable event gets lost.
To update $\theta_o$, we define three operations, denoted respectively by $\textbf{IN}^{obs}:\Theta_o \times \Sigma \rightarrow \Theta_o$, $\textbf{OUT}^{obs}:\Theta_o \rightarrow \Theta_o$, and $\textbf{LOSS}^{obs}:\Theta_o \times [1,N_o+1] \rightarrow \Theta_o$ as follows.
Given a $\theta_o=(x,n)\in \Theta_o$,
\begin{enumerate}
\item  if an event $\sigma  \in \Sigma$ occurs,  $x$ should be updated to $x^+$ at first  for counting the observation delays.
Furthermore, if $\sigma \in \Sigma_o$, by FIFO, we still need to add $(\sigma,0)$ to the end of $x^+$ for recording the new observable event occurrence.
Formally, for any $\theta_o=(x,n)\in \Theta_o$ and any  $\sigma \in \Sigma$, define $$\textbf{IN}^{obs}(\theta_o,\sigma)=(x',n'),$$ where  if $\sigma \in \Sigma_o$, $x'=x^+(\sigma,0)$ and $n'=n$, and  if $\sigma \in \Sigma_{uo}$, $x'=x^+$ and $n'=n$;

\item if a new  $\sigma \in \Sigma_o$ is communicated, by FIFO, $\sigma$ is the first event queued at the observation channel.
If we write $x=(\sigma_1,n_1)\cdots (\sigma_k,n_k)$, then $\sigma=\sigma_1$ and the remaining events delayed at the observation channel are $\sigma_2\cdots\sigma_k$.
Besides, since $n$ is used to track the number of consecusive observation losses, we need to reset $n$ to $0$ after a new event communication.
Therefore, for any $\theta_o=(x,n)\in \Theta_o$, if $x=(\sigma_1,n_1)\cdots (\sigma_k,n_k)\neq \varepsilon$, define $$\textbf{OUT}^{obs}(\theta_o)=(x',n'),$$ where $x'=(\sigma_2,n_2)\cdots (\sigma_k,n_k)$ and $n'=0$;

\item if the $i$th event in the observation channel gets lost, by definition, we should remove it from $x$.
Meanwhile, since a new observation loss occurs, the number of consecutive observation losses now is $n+1$.
Correspondingly, for any $\theta_o=(x,n) \in \Theta_o$ with $x=(\sigma_1,n_1)\cdots (\sigma_k,n_k) \neq \varepsilon$ and any $i \in [1,k]$, define $$\textbf{LOSS}^{obs}(\theta_o,i)=(x',n'),$$ where $x'=(\sigma_1,n_1)\cdots (\sigma_{i-1},n_{i-1}) (\sigma_{i+1},n_{i+1})\cdots(\sigma_k,n_k)$ and $n'=n+1$.
\end{enumerate}

\begin{definition}\label{DefII}
The control channel configuration is defined as: $\theta_c=(\phi, y=(\pi_1,m_1)\cdots (\pi_h,m_h), m),$
where ($\phi\in \Pi \cup \emptyset$)\footnote{Before the initial control action is executed, we have $\phi=\emptyset$.} is the control action being in use, $(\pi_1,m_1)\cdots (\pi_h,m_h)\in (\Pi \times [0,N_c])^{\le N+1}$ is a sequence of pairs such that $\pi_1\cdots\pi_h$ are control actions currently queued at the control channel, and $m_i$ is the number of event occurrences since the control action $\pi_i$ has been issued, and $m \in [0,N_{l,c}]$ counts the number of consecutive control losses.
\end{definition}
We denote by $\Theta_c \subseteq (\Pi\cup \emptyset) \times (\Pi \times [0,N_c])^{\le N+1} \times [0,N_{l,c}]$ the set of all the possible control channel configurations.
By Definition \ref{DefII}, we know $\theta_c$ is changed if one of the following four behaviors happens: (i) a new control action is issued, (ii) a new control action is executed, (iii) a control action gets lost, (iv) a new event occurs.
To update $\theta_c$, we next define four operations, denoted by $\textbf{IN}^{ctr}:\Theta_c \times \Pi \rightarrow \Theta_c$, $\textbf{OUT}^{ctr}:\Theta_c \rightarrow \Theta_c$, $\textbf{LOSS}^{ctr}:\Theta_c \times [1,N+1] \rightarrow \Theta_c$, and $\textbf{PLUS}:\Theta_c  \rightarrow \Theta_c$,  respectively.
Given a  $\theta_c=(\phi,y,m)\in \Theta_c$,
\begin{enumerate}

\item if a new control action $\pi \in \Pi$ is issued, we need to further consider the following two cases.
\emph{Case1:} If $\pi$ is the initial control action, we have $\phi=\pi$ since $\pi$ can be executed beforehand;
\emph{Case2:} If $\pi$ is not the initial control action, by FIFO, we need to add $(\pi,0)$ to the end of $y$.
Formally, for any $\theta_c=(\phi,y,n)\in \Theta_c$ and any $\pi \in \Pi$, define $$\textbf{IN}^{ctr}(\theta_c,\pi)=(\phi',y',m'),$$ where $\phi'=\pi$, $y'=y$, and $m'=m$ if $\phi=\emptyset$ (no control actions have ever been executed), and $\phi'=\phi$, $y'=y(\pi,0)$, and $m'=m$ if $\phi \neq \emptyset$ (some control actions have been executed before);

\item if a new control action $\pi \in \Pi$ is executed, by FIFO,  $\pi$ is the first control action queued at the control channel.
After the execution, the control action taking effect becomes $\pi$.
Meanwhile, since $m$ is used to track the number of consecutive control losses, we need to reset $m$ to $0$ after a new control action execution.
Formally, for any $\theta_c=(\phi,y,m)\in \Theta_c$, if $y=(\pi_1,m_1)\cdots (\pi_h,m_h)\neq \varepsilon$, define $$\textbf{OUT}^{ctr}(\theta_c)=(\phi',y',m'),$$ where $\phi'=\pi_1$ and $y'=(\pi_2,m_2)\cdots (\pi_h,m_h)$ and $m'=0$;

\item if the $i$th control action in the control channel gets lost, by definition, we need to remove it from $y$.
Meanwhile, since a new control loss occurs, the number of consecutive control losses now is $m+1$.
Formally, for any $\theta_c=(\phi,y,m)\in \Theta_c$ with $y=(\pi_1,m_1)\cdots (\pi_h,m_h)\neq \varepsilon$ and any $i \in [1,h]$, define $$\textbf{LOSS}^{ctr}(\theta_c,i)=(\phi', y',m'),$$  where $y'=(\pi_1,m_1)\cdots (\pi_{i-1},m_{i-1})(\pi_{i+1},m_{i+1})\cdots (\pi_h,m_h)$ and $\phi'=\phi$ and $m'=m+1$;

\item if a new event occurs in $G$, all the natural numbers in $y$ (if $y \neq \varepsilon$) should plus 1 for tracking the control delays.
Hence, for any $\theta_c=(\phi,y,m)\in \Theta_c$, define $$\textbf{PLUS}(\theta_c)=(\phi', y',m'),$$ where $\phi'=\phi$ and $y'=y^+$ and $m'=m$.
\end{enumerate}

Given a $\theta_o=(x,n)\in \Theta_o$, let $[\theta_o]_1=x$ and $[\theta_o]_2=n$ be the first and second component of $\theta_o$, respectively.
Similarly, given a $\theta_c=(\phi,y,m)\in \Theta_c$, let $[\theta_c]_1=\phi$, $[\theta_c]_2=y$, and $[\theta_c]_3=m$  be the first, the second, and the third component of $\theta_c$, respectively.

To estimate states under communication delays and losses,  besides $q\in Q$,  we also need to track $\theta_o\in \Theta_o$ and $\theta_c\in \Theta_c$  since they can affect the future behaviors of the controlled system.
To this end, we denote each state of the controlled system by a triplet $(q,\theta_o, \theta_c) \in Q  \times \Theta_o \times \Theta_c$.
We call such a state as an augmented state.
We  show how to update the augmented state estimate upon each new communication.
The procedure can be briefly summarized as repeatedly executing the following two steps.

\emph{Step1:}
Let $Z \subseteq Q \times \Theta_o \times \Theta_c$ be a set of augmented states calculated right after a new observation or the initial augmented state, i.e., $Z=\{(q_{0},\theta_o=(\varepsilon,0), \theta_c=(\emptyset,\varepsilon,0))\}$.
The delayed unobservable reach of $Z$ under an admissible control action $\pi\in \Pi$, denoted by $\text{DUR}(Z,\pi)$, is defined as follows.

\begin{enumerate}
  \item Initially, for all $(q,\theta_o,\theta_c) \in Z$,
  \begin{align}\label{Eq7}
  (q, \theta_o, \textbf{IN}^{ctr}(\theta_c,\pi)) \in  \text{DUR}(Z,\pi);
 \end{align}
 \item Then, we repeatedly apply the following operations until convergence is achieved.
\begin{itemize}
  \item For all $(q,\theta_o,\theta_c) \in \text{DUR}(Z,\pi)$, if $\delta(q,\sigma)!$ and $\sigma \in [\theta_c]_1$ and $\textbf{NUM}([\theta_o]_1)+1\le N_o$ and $\textbf{NUM}([\theta_c]_2)+1\le N_c$, then

\begin{align}\label{Eq8}
     (\delta(q,\sigma), \textbf{IN}^{obs}(\theta_o,\sigma),  \textbf{PLUS}(\theta_c)) \in  {\text{DUR}}(Z,\pi);
 \end{align}

\item For all $(q,\theta_o,\theta_c) \in \text{DUR}(Z,\pi)$, if $[\theta_c]_2 \neq \varepsilon$, then
 \begin{align}\label{Eq9}
  (q, \theta_o, \textbf{OUT}^{ctr}(\theta_c)) \in  \text{DUR}(Z,\pi);
\end{align}
 \item For all $(q,\theta_o,\theta_c) \in \text{DUR}(Z,\pi)$, if  $[\theta_o]_1 \neq \varepsilon$ and $[\theta_o]_2+1 \le N_{l,o}$, then for all $i \in [1, |[\theta_o]_1|]$
 \begin{align}\label{Eq10}
 (q,\textbf{LOSS}^{obs}(\theta_o,i), \theta_c) \in  \text{DUR}(Z,\pi);
\end{align}
\item For all $(q,\theta_o,\theta_c) \in \text{DUR}(Z,\pi)$, if $[\theta_c]_2 \neq \varepsilon$ and $[\theta_c]_3+1 \le N_{l,c}$, then for all $i \in [1, |[\theta_c]_2|]$
 \begin{align}\label{Eq11}
(q,\theta_o, \textbf{LOSS}^{ctr}(\theta_c,i)) \in  \text{DUR}(Z,\pi).
\end{align}
\end{itemize}
\end{enumerate}

\begin{remark}
In the context of networked DES, only ``an observable event is communicated'' is observable.
The behaviors of  ``an event (observable or not) occurs'', ``a control action is executed'', ``an observable event gets lost'', and ``a control action gets lost'' are all unobservable.
They are considered by (\ref{Eq8}), (\ref{Eq9}), (\ref{Eq10}), and (\ref{Eq11}), respectively.
And (\ref{Eq7}) is used to insert the newly issued control action $\pi$ into the control channel.
\end{remark}

Intuitively, ${\text{DUR}}(Z,\pi)$ consists of all the augmented states that can be reached from augmented states  in $Z$ in an ``unobservable'' way.
Specifically, for any $(q,\theta_o,\theta_c) \in \text{DUR}(Z,\pi)$,  by definitions, an event $\sigma$ can occur at $q$ only if (i) $\sigma$ is active at $q$, i.e., $\delta(q,\sigma)!$, (ii) $\sigma$ is allowed to occur by the control action that is taking effect, i.e., $\sigma \in [\theta_c]_1$, (iii) after the occurrence of $\sigma$, the control delays and observation delays are no larger than $N_c$ and $N_o$, i.e., $\textbf{NUM}([\theta_c]_2)+1 \le N_c  \wedge \textbf{NUM}([\theta_o]_1)+1 \le N_o$.
If  $\sigma$ occurs at $q$, then (a) the plant moves to state $\delta(q,\sigma)$, (b) $\theta_o$ is updated to $\textbf{IN}^{obs}(\theta_o,\sigma)$ for recording the occurrence of $\sigma$, and (c) $\theta_c$ is updated to $\textbf{PLUS}(\theta_c)$  for tracking the control delays.
That is illustrated by  $ (\delta(q,\sigma), \textbf{IN}^{obs}(\theta_o,\sigma),  \textbf{PLUS}(\theta_c)) \in  \text{DUR}(Z,\pi)$ in (\ref{Eq8}).
Furthermore, for any $(q,\theta_o,\theta_c) \in \text{DUR}(Z,\pi)$, a control action can be executed only if the queue of control actions delayed  at the control channel is not empty, i.e., $[\theta_c]_2 \neq \varepsilon$.
We write $[\theta_c]_2=(\pi_1,m_1) \cdots (\pi_h,m_h)$ for $\pi_i \in \Pi$ and $m_i \in [0,N_c]$.
When a new control action $\pi$ is executed, by FIFO,  the control action that is taking effect becomes $\pi=\pi_1$, and the control actions delayed at the control channel is $\pi_2\cdots\pi_h$.
This is illustrated by $ (q, \theta_o, \textbf{OUT}^{ctr}(\theta_c)) \in  \text{DUR}(Z,\pi)$ in (\ref{Eq9}).
On the other hand, for any $(q,\theta_o,\theta_c) \in \text{DUR}(Z,\pi)$, an observable event occurrence can get lost only if the observation channel is not empty, and the consecutive observation losses are no larger than $N_{l,o}$ after the observation loss, i.e., $[\theta_o]_1 \neq \varepsilon$ and $[\theta_o]_2 +1 \le N_{l,o}$.
When the $i$th, $i \in [1,|[\theta_o]_1|]$ observable event gets lost from the observation channel, we have $(q,\textbf{LOSS}^{obs}(\theta_o,i), \theta_c) \in  \text{DUR}(Z,\pi)$ in (\ref{Eq10}).
Similarly, if $[\theta_c]_2 \neq \varepsilon$ and $[\theta_c]_3+1 \le N_{l,c}$, we know the $i$th, $i \in [1,|[\theta_c]_2|]$  control action may get lost from the control channel.
Correspondingly, $(q,\theta_o, \textbf{LOSS}^{ctr}(\theta_c,i)) \in  \text{DUR}(Z,\pi)$ in (\ref{Eq11}) .

\emph{Step2:} Let $Z \subseteq Q \times \Theta_o \times \Theta_c$ be a given augmented state estimate.
The delayed observable reach of  $Z$ under an observable event $\sigma \in \Sigma_o$, denoted by $\text{DOR}(Z,\sigma)$,  is defined as:
\begin{align}\label{Eq12}
\text{DOR}(Z,\sigma)=&\{(q,\textbf{OUT}^{obs}(\theta_o),\theta_c):(\exists (q,\theta_o,\theta_c) \in Z)\notag\\
&[\theta_o]_1=(\sigma_1,n_1)\cdots(\sigma_k,n_k) \neq \varepsilon \wedge \sigma_1=\sigma\}.
\end{align}

 $\text{DOR}(Z,\sigma)$ includes all the augmented states can be reached from augmented states in  $Z$ following a new communication of $\sigma$.
By FIFO, an observable event can be communicated only if it is the first event queued at the observation channel.
Hence, we only consider all the $\sigma \in \Sigma_o$ such that there exists $(q,\theta_o,\theta_c) \in Z$ with $[\theta_o]_1=(\sigma_1,n_1)\cdots(\sigma_k,n_k) \neq \varepsilon \wedge \sigma_1=\sigma$.
When $\sigma$ is communicated, we remove $(\sigma_1,n_1)$ from $\theta_o$.
As we can see, $\theta_o$ is updated to $\textbf{OUT}^{obs}(\theta_o)$  after the communication of $\sigma$.
We assume $\text{DOR}(Z,\sigma)$ is updated right after a new observation $\sigma$ but before the next control action is issued.
Therefore, we keep $\theta_c$ unchanged in (\ref{Eq12}).

For a communicated  string $t\in \Sigma_o^*$, let the set of augmented states calculated  by alternatively applying \emph{Step1} and \emph{Step2} be the augmented state estimate for $t$.
Formally,
\begin{definition}\label{Def3}
Given a system $G$ and a networked supervisor $S$ defined over $\Sigma_o^*$, for any $t \in f^{-1}(\psi^f(\mathcal{L}(G_S)))$, let $\tilde{\mathcal{E}}_S(t)$ be the augmented state estimate calculated by alternatively applying $\textup{DUR}(\cdot)$ and $\textup{DOR}(\cdot)$ as follows.

\begin{itemize}
  \item Initially,  $\tilde{\mathcal{E}}_S(\varepsilon)=\textup{DUR}(\{(q_0,(\varepsilon,0),(\emptyset,\varepsilon,0))\},S(\varepsilon))$;
  \item For all $t^i,t^i\sigma_{i+1} \in \overline{\{t\}}$, $i=0,1,\ldots,|t|-1$,  $$\tilde{\mathcal{E}}_S(t^i\sigma_{i+1})=\textup{DUR}(\textup{DOR}(\tilde{\mathcal{E}}_S(t^i), \sigma_{i+1}),S(t^i\sigma_{i+1})).$$
\end{itemize}

\end{definition}

We next discuss the relationship between augmented states in $\tilde{\mathcal{E}}_S(t)$ and states in $G_S$ that can be reached from $\tilde{q}_0$ via strings $\mu\in \mathcal{L}(G_S)$ with $f^{-1}(\psi^f(\mu))=t$.

\begin{proposition}\label{Prop3}
Given a system $G$ and a networked supervisor $S$ defined over $\Sigma_o^*$, for all $t \in f^{-1}(\psi^f(\mathcal{L}(G_S)))$, we have
\begin{align}\label{Eq13}
&(q,\theta_o,\theta_c)\in \tilde{\mathcal{E}}_S(t) \Rightarrow (\exists \mu \in \mathcal{L}(G_S))\notag \\
& f^{-1}(\psi^f(\mu))=t \wedge \tilde{\delta}(\tilde{q}_0,\mu)=(a,x,n,\phi,y,m,p)\wedge \notag \\
& q=a \wedge \theta_o=(x,n) \wedge \theta_c=(\phi,y,m).
\end{align}
\end{proposition}
\begin{proof}
Please see Appendix B.
\end{proof}
\begin{proposition}\label{Prop4}
For any $\mu \in \mathcal{L}(G_S)$, we write $\tilde{\delta}(\tilde{q}_0,\mu)=\tilde{q}=(a,x,n,\phi,y,m,p)$.
Then,  $(q,\theta_c,\theta_o) \in \tilde{\mathcal{E}}_S(f^{-1}(\psi^f(\mu)))$, where $q=a$, $\theta_o=(x,n)$, and $\theta_c=(\phi,y,m)$.
\end{proposition}
\begin{proof}
Please see Appendix D.
\end{proof}

Given a set of augmented states $Z \in  2^{Q \times \Theta_o \times \Theta_c}$, let $\textup{FC}(Z)=\{q \in Q:(\exists (q,\theta_o,\theta_c) \in Z)\}$ be the set of first components of augmented states in $Z$.
The following theorem shows that $\textup{FC}(\tilde{\mathcal{E}}_S(t))$ indeed estimates  states of the controlled system.

\begin{theorem}\label{Theo1}
Given a system $G$ and a networked supervisor $S$ defined over $\Sigma_o^*$, for all $t \in f^{-1}(\psi^f(\mathcal{L}(G_S)))$,  $\textup{FC}(\tilde{\mathcal{E}}_S(t))={\mathcal{E}}_S(t)$.
\end{theorem}
\begin{proof}
We first prove $\textup{FC}(\tilde{\mathcal{E}}_S(t)) \subseteq {\mathcal{E}}_S(t)$.
For any $(q,\theta_o,\theta_c) \in \tilde{\mathcal{E}}_S(t)$, by Proposition \ref{Prop3} and Definition \ref{Def2}, $q \in {\mathcal{E}}_S(t)$.
Therefore,  $\textup{FC}(\tilde{\mathcal{E}}_S(t)) \subseteq {\mathcal{E}}_S(t)$.
Next, we prove  ${\mathcal{E}}_S(t) \subseteq \textup{FC}(\tilde{\mathcal{E}}_S(t))$.
For any $q \in {\mathcal{E}}_S(t)$, by Definition \ref{Def2}, $\exists \mu \in \mathcal{L}(G_S)$ such that $f^{-1}(\psi^f(\mu))=t$ and $q=\delta(q_0,\psi(\mu))$.
We write $\tilde{\delta}(\tilde{q}_0,\mu)=(a,x,n,\phi,y,m,p)$.
By Proposition \ref{Prop1}, $q=a$.
By Proposition \ref{Prop4}, $(q',\theta_c,\theta_o) \in \tilde{\mathcal{E}}_S(f^{-1}(\psi^f(\mu)))=\tilde{\mathcal{E}}_S(t)$, where $q'=a$, $\theta_o=(x,n)$, and $\theta_c=(\phi,y,m)$.
Therefore, $q=a=q' \in \textup{FC}(\tilde{\mathcal{E}}_S(t))$.
Since $q$ is arbitrarily given,  ${\mathcal{E}}_S(t) \subseteq \textup{FC}(\tilde{\mathcal{E}}_S(t))$.
\end{proof}

\begin{figure}
	\begin{center}
		\includegraphics[width=9.2cm]{fig4.pdf}
		\caption{Online state estimation under communcation delays and losses.}
		\label{Fig4}
	\end{center}
\end{figure}

\begin{remark}
The online  process for estimating states of the controlled system under communication delays and losses is depicted in Fig.\ref{Fig4}.
It can be briefly summarized as repeatedly executing: (i) an
observable event occurrence $\sigma \in \Sigma_o$ is communicated to the networked supervisor, and $Z'$ is updated to $Z'=\textup{DOR}(Z,\sigma)$;
(ii)
a newly issued control action $\pi \in \Pi$ is sent to the actuator of the plant, and then the corresponding augmented state estimate $Z=\textup{DUR}(Z',\pi)$ is calculated using (\ref{Eq7})$\sim$(\ref{Eq11}).
By Theorem \ref{Theo1}, the current NSE can be obtained by taking all the first components of augmented states in $Z$, i.e., $\textup{FC}(Z)$.
\end{remark}

\begin{remark}
By Fig.\ref{Fig4}, the augmented state estimate is updated only when  a new control action $\pi \in \Pi$ is issued (following a new observation of $\sigma\in \Sigma_o$).
For any $Z \in  2^{Q \times \Theta_o \times \Theta_c}$, the complexities for computing $\textup{DOR}(Z,\sigma)$ and  $\textup{DUR}(\textup{DOR}(Z,\sigma),\pi)$ are linear in the size of $\Theta_o$ and  $Q \times \Theta_o\times \Theta_c$, respectively.
Therefore,  the computational complexity for augmented state estimation  is stepwise order of $\mathcal{O}(|Q| \times |\Theta_o| \times |\Theta_c|)$.
Since $\Theta_o \subseteq (\Sigma_o\times [0,N_o])^{\le N_o+1}\times [0,N_{l,o}]$ and  $\Theta_c \subseteq (\Pi\cup \emptyset) \times (\Pi \times [0,N_c])^{\le N+1} \times [0,N_{l,c}]$, we have
\begin{align*}
\mathcal{O}(|Q| \times |\Theta_o| \times |\Theta_c|)=&\mathcal{O}(|Q|\times |\Sigma|^{N_o}\times 2^{N \times |\Sigma|}\times (N_o+1)^{N_o}\\
&  \times (N_c+1)^N \times N_{l,o} \times N_{l,c}).
\end{align*}
Given $N_c$, $N_o$, $N_{l,c}$, and $N_{l,o}$ are fixed, we know $\mathcal{O}(|Q| \times |\Theta_o| \times |\Theta_c|)$ is polynomial with respect to (w.r.t.) $|Q|$ and exponential w.r.t. $|\Sigma|$.
\end{remark}

\begin{example}
Consider again the system $G$ and the networked supervisor $S$ depicted in Fig.\ref{Fig21} and Fig.\ref{Fig22}, respectively.
As in Example \ref{Ex2}, let $\Sigma_c=\Sigma$, $\Sigma_o=\{\alpha,\beta\}$, and $N_c=N_o=N_{l,c}=N_{l,o}=1$.

Initially, by (\ref{Eq7}), $z_1=(q_1,(\varepsilon,0),(S(\varepsilon),\varepsilon,0)) \in \tilde{\mathcal{E}}_S(\varepsilon)$.
By Fig.\ref{Fig21}, $\delta(q_1,\alpha)!$.
Moreover, since $\alpha \in S(\varepsilon)$ and $\textbf{NUM}(\varepsilon)+1\le N_c,N_o$, by (\ref{Eq8}), $z_2=(q_2,((\alpha,0),0),(S(\varepsilon),\varepsilon,0)) \in \tilde{\mathcal{E}}_S(\varepsilon)$.
In $z_2$, if $\alpha$ gets lost,  by (\ref{Eq10}), $z_3=(q_2,(\varepsilon,1),(S(\varepsilon),\varepsilon,0)) \in \tilde{\mathcal{E}}_S(\varepsilon)$.
Therefore, $\tilde{\mathcal{E}}_S(\varepsilon)=\{z_1,z_2,z_3\}$. By Theorem \ref{Theo1}, $\mathcal{E}_S(\varepsilon)=\{q_1,q_2\}$.
Next, if $\alpha$ is communicated, by $(\ref{Eq12})$, $$\textup{DOR}(\tilde{\mathcal{E}}_S(\varepsilon),\alpha)=\{(q_2,(\varepsilon,0),(S(\varepsilon),\varepsilon,0))\}.$$
Then, by (\ref{Eq7}), we know $z_4=(q_2,(\varepsilon,0),(S(\varepsilon),(S(\alpha),0),0))\in \tilde{\mathcal{E}}_S(\alpha)$.
If  $S(\alpha)$ gets lost, by (\ref{Eq11}),  $z_5=(q_2,(\varepsilon,0),(S(\varepsilon),\varepsilon,1))\in \tilde{\mathcal{E}}_S(\alpha)$.
Otherwise, if  $S(\alpha)$ is executed, by (\ref{Eq9}), we have $z_6=(q_2,(\varepsilon,0),(S(\alpha),\varepsilon,0))\in \tilde{\mathcal{E}}_S(\alpha)$.
Since $S(\alpha)=\{\beta,\lambda\}$ and $\textbf{NUM}(\varepsilon)+1\le N_c,N_o$, by (\ref{Eq8}), we have  $z_7,z_8,z_9 \in \tilde{\mathcal{E}}_S(\alpha)$, where $z_7=(q_3,(\varepsilon,0),(S(\alpha),\varepsilon,0))$, $z_8=(q_5,(\varepsilon,0),(S(\alpha),\varepsilon,0))$, and $z_9=(q_4,((\beta,0),0),(S(\alpha),\varepsilon,0))$.
Since $\delta(q_4,\lambda)=q_5$, $S(\alpha)=\{\beta,\lambda\}$, $\textbf{NUM}((\beta,0))+1\le N_o$, and $\textbf{NUM}(\varepsilon)+1\le N_c$, also by (\ref{Eq8}), $z_{10}=(q_5,((\beta,1),0),(S(\alpha),\varepsilon,0))\in \tilde{\mathcal{E}}_S(\alpha)$.
If $\beta$ gets lost in $z_9$ or $z_{10}$, by (\ref{Eq10}), $z_{11}=(q_4,(\varepsilon,1),(S(\alpha),\varepsilon,0))\in \tilde{\mathcal{E}}_S(\alpha)$ and $z_{12}=(q_5,(\varepsilon,1),(S(\alpha),\varepsilon,0))\in \tilde{\mathcal{E}}_S(\alpha)$.
Therefore, $\tilde{\mathcal{E}}_S(\alpha)=\{z_4 \sim z_{12}\}$.
By Theorem \ref{Theo1}, $\mathcal{E}_S(\alpha)=\{q_2,q_3,q_4,q_5\}$.

\end{example}

\section{Application}

In this section,  we show how to apply the approaches proposed in \cite{yin16tac1} for calculating maximally-permissive and safe  supervisors to calculate corresponding maximally-permissive and safe networked supervisors.

\subsection{Networked safety}

We start by defining networked safety of DES under communication delays and losses.
Let $H=(Q_H,\Sigma,\delta_H,\Gamma_H, q_0) \sqsubseteq G$ be a sub-automaton of $G$ that characterizes the specification language (safe behaviors).
That is, $Q_H$ captures all the safe behaviors in the sense that all the strings generated by $G$ are safe if they are ended in states in $Q_H$ and unsafe if they are ended in states in $Q\setminus Q_H$.
Then, the property of networked safety of DES can be defined as follows.
\begin{definition}\label{Def4}
Given a system automaton $G$, a specification automaton $H$, and a networked supervisor $S$ defined over $\Sigma_o^*$,  we say that $\mathcal{L}(S/G)$ is networked safe w.r.t. $Q_H\subseteq Q$ and $G$ if $(\forall s \in  \mathcal{L}(S/G))\delta(q_0,s)\in Q_H$.
\end{definition}

Inspired by the work of \cite{yin16tac2}, we next show that networked safety can be formulated as information-state-based (IS-based) property.
Here, we refer to an \textsl{information state} as a set of augmented states.
To be more specific,
we define the IS-based property $\varphi$ w.r.t. $G$ as a function $\varphi: 2^{Q \times \Theta_o \times \Theta_c} \rightarrow \{0,1\}$, where for all $Z \in 2^{Q \times \Theta_o \times \Theta_c}$, $\varphi(Z)=1$ means $Z$ satisfies the property $\varphi$.
We say that the language generated under $S$ w.r.t. $G$ satisfies the property $\varphi$, denoted by $\mathcal{L}(S/G) \models_G \varphi$, if all the augmented state estimates generated under $S$ satisfy $\varphi$, i.e., $(\forall t \in f^{-1}(\psi^f(\mathcal{L}(G_S))))\varphi(\tilde{\mathcal{E}}_S(t))=1$.
We say $S$ is property-$\varphi$ enforcing w.r.t. $G$ if $\mathcal{L}(S/G) \models_G \varphi$.
Let us define the IS-based property $\varphi_{safe}:2^{Q \times \Theta_o \times \Theta_c} \rightarrow \{0,1\}$  as: for any $Z \in 2^{Q \times \Theta_o \times \Theta_c}$,
\begin{align}\label{Eq14}
&\varphi_{safe}(Z)=1 \Leftrightarrow  \textup{FC}(Z)\subseteq Q_H.
\end{align}
\begin{proposition}
Given automata $G$ and $H$, and a networked supervisor $S$ defined over $\Sigma_o^*$,
$\mathcal{L}(S/G)$ is networked safe  w.r.t. $Q_H\subseteq Q$ and $G$ if and only if $\mathcal{L}(S/G)\models_G \varphi_{safe}$.
\end{proposition}
\begin{proof}
($\Rightarrow$) By contradiction.
Suppose $\mathcal{L}(S/G) \not \models_G \varphi_{safe}$.
By definition, $\exists t\in f^{-1}(\psi^f(\mathcal{L}(G_S)))$ such that $\varphi_{safe}(\tilde{\mathcal{E}}_S(t))=0$.
By (\ref{Eq14}), $\exists (q,\theta_o,\theta_c)\in \tilde{\mathcal{E}}_S(t)$ such that $q \in Q\setminus Q_H$.
By Theorem \ref{Theo1}, $q \in {\mathcal{E}}_S(t)$.
By the definition of ${\mathcal{E}}_S(\cdot)$, $\exists \mu \in \mathcal{L}(G_S)$ such that $f^{-1}(\psi^f(\mu))=t$  and $q=\delta(q_{0},\psi(\mu))$.
Therefore, $\exists \psi(\mu) \in \psi(\mathcal{L}(G_S))$ such that  $\delta(q_0,\psi(\mu))=q \in Q \setminus Q_H$.
By Definition \ref{Def1}, $\psi(\mathcal{L}(G_S))=\mathcal{L}(S/G)$.
Thus, $\mathcal{L}(S/G)$ is not networked safe.
($\Leftarrow$)
Also by contradiction.
Suppose that $\mathcal{L}(S/G)$ is not networked safe.
By Definitions \ref{Def4} and \ref{Def1}, $\exists \mu \in \mathcal{L}(G_S)$ such that $\delta(q_{0},\psi(\mu)) \in Q\setminus Q_H$.
We write $\tilde{\delta}(\tilde{q}_0,\mu)=(q,x,n,\phi,y,m,p)$ and $f^{-1}(\psi^f(\mu))=t$.
By Proposition \ref{Prop1}, $q=\delta(q_0,\psi(\mu))\in Q\setminus Q_H$.
By the definition of ${\mathcal{E}}_S(\cdot)$,  we know $q \in {\mathcal{E}}_S(t)$.
By Theorem \ref{Theo1}, $\exists (a,\theta_c,\theta_o) \in \tilde{\mathcal{E}}_S(t)$ with $a=q$.
Since $q \in Q\setminus Q_H$, $\varphi_{safe}(\tilde{\mathcal{E}}_S(t))=0$, which contradicts $\mathcal{L}(S/G)\models_G \varphi_{safe}$.
\end{proof}

\subsection{Networked supervisor synthesis}

To synthesize the maximally-permissive and safe supervisors, the authors in \cite{yin16tac1} constructed a \textsl{Bipartite Transition System} (BTS) that considers all the admissible control actions  upon each new observation, and then estimates states of the controlled system under a given control action.
We next generalize the \textsl{Bipartite Transition System} (BTS) to the \textsl{Networked Bipartite Transition System} (NBTS) using  techiniques introduced in this paper.
Formally, a NBTS $T$ w.r.t. $G$ is a seven-tuple
\begin{align}
T=(Q_Y^T,Q_Z^T,h^T_{YZ},h^T_{ZY},\Sigma_o,\Pi,y_0),
\end{align}
where
\begin{itemize}
  \item $Q_Y^T \subseteq Q \times \Theta_o \times \Theta_c$ is the set of $Y$-states;
  \item $Q_Z^T \subseteq (Q \times \Theta_o \times \Theta_c)\times \Pi$ is the set of $Z$-states, and each $Z$-state $z=(I(z),\Pi(z))$ consists of two parts  such that $I(z)$ and $\Pi(z)$ denote, respectively, the information state and the control action parts of $z$;
  \item $h^T_{YZ}:Q_Y^T\times \Pi \rightarrow Q_Z^T$ is a transition function from $Y$-states to $Z$-states, which is defined as follows: for any $y\in Q_Y^T$ and any $\pi \in \Pi$, $h^T_{YZ}(y,\pi)=(\text{DUR}(y,\pi),\pi)$;
\item $h^T_{ZY}:Q_Z^T \times \Sigma_o \rightarrow Q_Y^T$ is a transition function from $Z$-states to $Y$-states, which is defined as follows: for any $z \in Q_Z^T$  and any $\sigma \in \Sigma_o$,  if $(\exists (q,\theta_o,\theta_c) \in I(z))[\theta_o]_1=(\sigma_1,n_1)\cdots (\sigma_k,n_k) \wedge \sigma=\sigma_1$, $ h^T_{ZY}(z,\sigma)=\text{DOR}(I(z),\sigma)$;
\item $\Sigma_o$ is the set of observable events of $G$;
\item $\Pi$ is the set of admissible control actions;
\item $y_0=(q_0,(\varepsilon,0),(\emptyset,\varepsilon,0))$ is the initial $Y$-state.
\end{itemize}

\begin{remark}
The NBTS is an extension of the BTS in the case of communication delays and losses.
A NBTS also consists of two types of states, named Y-states and Z-states.
A Y-state estimates all the augmented states the system can immediately reach right after a new observable event communication (by applying the operation of ``delayed observable reach'' on its predecessor).
From a Y-state, all the admissible control decisions are considered.
A Z-state collects all the augmented states that are reachable from its
predecessor (a Y-state) under a given control action (by applying the operation of ``delayed observable reach'' on its predecessor).
\end{remark}

The following notions are similar with their non-networked counterparts \cite{yin16tac1}.
Let $T$ be a NBTS.
We say $T$ satisies $\varphi_{safe}$ if $\forall z \in Q_Z^T$, $\varphi_{safe}(I(z))=1$.
For each $Y$-state $y \in Q_Y^T$, we denote by $C_T(y)=\{\pi \in \Pi:h_{YZ}^T(y,\pi)!\}$ the set of control actions defined at $y$.
We say $T$ is complete, if
\begin{enumerate}
\item For all $y \in Q_Y^T$, $C_T(y)\neq \emptyset$;
\item For all $z \in Q_Z^T$ and all $\sigma \in \Sigma_o$, $(\exists (q,\theta_o,\theta_c) \in I(z))[\theta_o]_1=(\sigma_1,n_1)\cdots (\sigma_k,n_k)\neq \varepsilon \wedge \sigma=\sigma_1$ implies $ h^T_{ZY}(z,\sigma)!$.
\end{enumerate}
The first property says that for any reachable $Y$-state, there exists at least one control contion defined at that state,
and the second property says that if an observable event is active at a $Z$-state, we can not disable its occurrence.

We call $S(\varepsilon)\sigma_1S(\sigma_1)\sigma_2 \cdots\sigma_n S(\sigma_1\cdots\sigma_n)$ a \emph{run}, where $\sigma_i\in \Sigma_o$.
We write $y \xrightarrow{\pi} z$ if $h^T_{YZ}(y,\pi)=z$, and $z \xrightarrow{\sigma} y$ if $h^T_{ZY}(z,\sigma)=y$.
The occurrence of the \emph{run} $S(\varepsilon)\sigma_1S(\sigma_1)\sigma_2 \cdots\sigma_n S(\sigma_1\cdots\sigma_n)$ will reach
an alternating sequence of $Y$-states and $Z$-states
$$y_0 \xrightarrow{S(\varepsilon)} z_0 \xrightarrow{\sigma_1} y_1 \xrightarrow{S(\sigma_1)}\cdots \xrightarrow{S(\sigma_1\cdots\sigma_{n-1})} z_{n-1} \xrightarrow{\sigma_n} y_n \xrightarrow{S(\sigma_1\cdots\sigma_n)}z_n.$$

Let $t=\sigma_1\cdots\sigma_n$.
We denote by $IS_S^Y(t)$ and $IS_S^Z(t)$ the last $Y$- and $Z$-states in $y_0z_0y_1z_2\cdots z_{n-1}y_nz_n$, respectively, i.e., $IS_S^Y(t)=y_n$ and $IS_S^Z(t)=z_n$.
By the definition of $T$ and Definition \ref{Def3}, $I(IS_S^Z(t))=\tilde{\mathcal{E}}_S(t)$, i.e., the information part of $IS_S^Z(t)$ is the augmented state estimate right after observing $t$ under $S$.

\begin{definition}\label{Def5}
A networked supervisor $S=(A,\gamma)$ with $A=(X,\Sigma_o,\zeta, x_0)$ is said to be included into a NBTS $T$, if for any $t \in f^{-1}(\psi^f(\mathcal{L}(G_S)))$,  $\zeta(x_0,t)=I(IS_S^Z(t))$ and $\gamma(\zeta(x_0,t))\in C_T(IS_S^Y(t))$.
To complete the definition of $S$, for all $t \in \Sigma_o^* \setminus f^{-1}(\psi^f(\mathcal{L}(G_S)))$, define $\zeta(x_0,t)=x_{etr}$ with $\gamma(x_{etr})=\Sigma$.
\end{definition}

We denote by $\mathbb{S}(T)$ all the networked supervisors included in $T$.
An \emph{All Inclusive Networked Controller} (AINC) is a NBTS that satisfies
the defined IS-based property $\varphi_{safe}$ and is as large as possible.

\begin{definition}\label{Def6}
Given a system $G$ and the IS-based property $\varphi_{safe}:I \rightarrow \{0,1\}$,  the AINS for property $\varphi_{safe}$, denoted by $$AINS_{\varphi_{safe}}(G)=(Q_Y^{AINS},Q_Z^{AINS},h^{AINS}_{YZ},h^{AINS}_{ZY},\Sigma_o,\Pi,y_0),$$  is the largest complete $NBTS$ satisfying $\varphi_{safe}$.
\end{definition}

The following theorem shows that $AINS_{\varphi_{safe}}(G)$ contains all the $\varphi_{safe}$-enforcing networked supervisors.

\begin{theorem}
Given a system $G$ and the IS-based property $\varphi_{safe}:2^{Q \times \Theta_o \times \Theta_c} \rightarrow \{0,1\}$,  a networked supervisor $S$ is property $\varphi_{safe}$-enforcing iff it is included in $AINS_{\varphi_{safe}}(G)$, i.e., $\mathcal{L}(S/G) \models_G \varphi_{safe} \Leftrightarrow S \in \mathbb{S}(AINS_{\varphi_{safe}}(G)) $.
\end{theorem}
\begin{proof}
($\Leftarrow$) By  Definitions \ref{Def3} and \ref{Def5}, we have $\tilde{\mathcal{E}}_S(t)=I(IS^Z_S(t))$ for all $t \in f^{-1}(\psi^f(\mathcal{L}(G_S)))$.
Since $AINS_{\varphi_{safe}}(G)$ satisfies $\varphi_{safe}$, $\varphi_{safe}(\tilde{\mathcal{E}}_S(t))=1$.
Hence,  $\mathcal{L}(S/G) \models_G \varphi_{safe}$.

($\Rightarrow$)
Suppose there exists a networked supervisor $S$ such that $\mathcal{L}(S/G) \models_G \varphi_{safe}$ and  $S \notin \mathbb{S}(AINS_{\varphi_{safe}}(G))$.
Let $T$ be a complete NBTS such that all its Y-sates and Z-states are Y-sates and Z-states reached by $S$ via some $t\in f^{-1}(\psi^f(\mathcal{L}(G_S)))$.
Then, we have $S \in \mathbb{S}(T)$.
Since $\mathcal{L}(S/G) \models_G \varphi_{safe}$, $T$ satisfies $\varphi_{safe}$.
Hence, $S \in \mathbb{S}(T)$ and  $T$ is a complete NBTS satisfing $\varphi_{safe}$.
Since $S \notin \mathbb{S}(AINS_{\varphi_{safe}}(G))$, $\exists t\in f^{-1}(\psi^f(\mathcal{L}(G_S)))$ with $S(t)
\notin C_{AINS_{\varphi_{safe}}(G)}(IS^Y_S(t))$.
Thus,  $T \cup AINS_{\varphi_{safe}}(G)$ is a complete NBTS satisfying $\varphi_{safe}$, and is strictly larger than $AINS_{\varphi_{safe}}(G)$, which contradicts  $AINS_{\varphi_{safe}}(G)$ is the largest complete NBTS satisfying $\varphi_{safe}$.
\end{proof}

The techniques proposed in \cite{yin16tac1} can be easily extended to construct $AINS_{\varphi_{safe}}(G)$ with $T$, and then find a maximally-permissive networked supervisor from all the supervisors included in $AINS_{\varphi_{safe}}(G)$.
In this paper, we focus on how to estimate states of the controlled system with communication delays and losses.
The formal algorithms for synthesizing maximally-permissive networked supervisors  are beyond the scope of this paper.
The reader is referred to \cite{yin16tac1} for details.

\section{Conclusion}

In supervisory control, communication delays and losses are unavoidable when
 communication between the plant and the supervisor for
observation, and between the supervisor and the actuator for
control is carried out over some shared networks. We assume, in this paper, that (i) the delays do not change the order of the observations and controls,
(ii) both the observation delays and control delays are with upper bounds, and (iii) both the consecutive observation losses and the consecutive control losses are also with upper bounds.
A novel framework for supervisory control under communication delays and losses has been established.
Under this framework, an algorithm for online state estimation of a controlled system has been proposed.
The proposed algorithm can be used to solve the \textsl{supervisor synthesis problem} in networked DES.
As an application, we show how to use the existing methods to synthesize  maximally-permissive and safe networked supervisors.

\section{Appendix}

\subsection{Proof of Proposition \ref{Prop}}

\begin{proof}
Let us first define the following notation.

For any $y=(\pi_1,l_1)\cdots (\pi_h,l_h) \in (\Pi \times [0,N_c])^{\le N+1}$ and any $y'=(\pi'_1,l'_1)\cdots (\pi'_h,l'_h) \in (\Pi \times [0,N_c])^{\le N+1}$, we say $y$ is smaller than $y'$, denoted by $y \preceq y'$,  if $\pi_i \subseteq \pi'_i$ and $l_i=l_i'$ for all $i=1,\ldots,h$.
Note that $\varepsilon \preceq \varepsilon$ always holds.

Given a string $\mu_1 \in \mathcal{L}(G_{S_1})$, let us write $\tilde{\delta}_1(\tilde{q}_{0,1},\mu_1)=(q_1,x_1,n_1,\phi_1,y_1,m_1,p_1)$.
We next prove there always exists a $\mu_2 \in \mathcal{L}(G_{S_2})$ such that $\psi(\mu_1)=\psi(\mu_2)$, $\psi^f(\mu_1)=\psi^f(\mu_2)$, and $\tilde{\delta}_2(\tilde{q}_{0,2},\mu_2)=(q_2,x_2,n_2,\phi_2,y_2,m_2,p_2)$ with $q_2=q_1$, $x_2=x_1$, $n_2=n_1$, $\phi_1 \subseteq \phi_2$, $y_1 \preceq y_2$, and $m_2=m_1$.
The proof is by induction on the length of strings in $\mathcal{L}(G_{S_1})$.

\textbf{Base case:}
By definitions, we have $$\tilde{\delta}_1(\tilde{q}_{0,1},\varepsilon)=(q_0,\varepsilon,0,S_1(\varepsilon),\varepsilon,0,x_{0,1}),$$ and $$\tilde{\delta}_2(\tilde{q}_{0,2},\varepsilon)=(q_0,\varepsilon,0,S_2(\varepsilon),\varepsilon,0,x_{0,2}).$$
Since $\psi(\varepsilon)=\psi(\varepsilon)$, $\psi^f(\varepsilon)=\psi^f(\varepsilon)$, $q_0=q_0$, $\varepsilon=\varepsilon$, $0=0$, $S_1(\varepsilon)\subseteq S_2(\varepsilon)$, $\varepsilon \preceq \varepsilon$, and $0=0$, the base case is true.

\textbf{Induction hypothesis:} Given a $\mu_1 \in \mathcal{L}(G_{S_1})$, we write $\tilde{\delta}_1(\tilde{q}_{0,1},\mu_1)=(q_1,x_1,n_1,\phi_1,y_1,m_1,p_{1})$.
Then, there exists a $\mu_2 \in \mathcal{L}(G_{S_2})$ such that $\psi(\mu_1)=\psi(\mu_2)$, $\psi^f(\mu_1)=\psi^f(\mu_2)$, and $\tilde{\delta}_2(\tilde{q}_{0,2},\mu_2)=(q_2,x_2,n_2,\phi_2,y_2,m_2,p_2)$ with $q_2=q_1$, $x_2=x_1$, $n_2=n_1$, $\phi_1\subseteq \phi_2$, $y_1 \preceq y_2$, and $m_2=m_1$.
We next prove the same is also true for $\mu_1e \in \mathcal{L}(G_{S_1})$.
Write $\tilde{\delta}_1(\tilde{q}_{0,1},\mu_1 e)=(q'_1,x'_1,n'_1,\phi'_1,y'_1,m'_1,p'_{1})$.

\emph{Case 1:} $e \in \Sigma$.
Since $\mu_1e \in \mathcal{L}(G_{S_1})$, by (\ref{Eq1}), $\delta(q_1,e)!$, $e \in \phi_1$, $\textbf{NUM}(x_1)+1 \le N_o$, and $\textbf{NUM}(y_1)+1 \le N_c$.
Since $q_1=q_2$, $\phi_1 \subseteq \phi_2$, $x_1=x_2$, and $y_1 \preceq y_2$, one can verify $\delta(q_2,e)!$, $e \in \phi_2$, $\textbf{NUM}(x_2)+1 \le N_o$, and $\textbf{NUM}(y_2)+1 \le N_c$.
By (\ref{Eq1}), $\mu_2e \in \mathcal{L}(G_{S_2})$.
We write $\tilde{\delta}_2(\tilde{q}_{0,2},\mu_2 e)=(q'_2,x'_2,n'_2,\phi'_2,y'_2,m'_2,p'_2)$.
By (\ref{Eq1}), $q'_2=\delta(q_2,e)$, $x'_2=x_2^+(e,0)$ if $e \in \Sigma_o$ and $x'_2=x_2^+$ if $e \in \Sigma_{uo}$, $n'_2=n_2$, $\phi_2'=\phi_2$, $y'_2=y_2^+$, and $m_2'=m_2$.
Moreover, since  $\tilde{\delta}_1(\tilde{q}_{0,1},\mu_1 e)=(q'_1,x'_1,n'_1,\phi'_1,y'_1,m'_1,p'_{1})$,
by (\ref{Eq1}), $q'_1=\delta(q_1,e)$, $x'_1=x_1^+(e,0)$ if $e \in \Sigma_o$ and $x'_1=x_1^+$ if $e \in \Sigma_{uo}$, $n'_1=n_1$, $\phi_1'=\phi_1$, $y'_1=y_1^+$, and $m_1'=m_1$.
Since $q_2=q_1$, $q'_2=\delta(q_2,e)$, and $q'_1=\delta(q_1,e)$, we have $q'_2=q'_1$.
Since $x_2=x_1$, $x'_2=x_2^+(e,0)$ and $x'_1=x_1^+(e,0)$ if $e \in \Sigma_o$,   $x'_2=x_2^+$ and $x'_1=x_1^+$ if $e \in \Sigma_{uo}$, we have $x'_2=x'_1$.
Meanwhile, by the induction hypothesis, we know  $n_2=n_1$, $\phi_1\subseteq \phi_2$, $y_1 \preceq y_2$, and $m_2=m_1$.
Since $n'_1=n_1$, $\phi_1'=\phi_1$, $y'_1=y_1^+$, $m_1'=m_1$, $n'_2=n_2$, $\phi_2'=\phi_2$, $y'_2=y_2^+$, and $m_2'=m_2$, we have $n'_2=n'_1$, $\phi'_1 \subseteq \phi'_2$, $y'_1 \preceq y'_2$, and $m'_2=m'_1$.
Overall, we have $q'_1=q'_2$, $x'_1=x'_2$, $n'_1=n'_2$, $\phi_1'\subseteq \phi_2'$, $y'_1 \preceq y'_2$, and $m_1'=m_2'$.
Since  $\psi(\mu_1)=\psi(\mu_2)$ and $\psi^f(\mu_1)=\psi^f(\mu_2)$, by definitions, $\psi(\mu_1 e)=\psi(\mu_1) e=\psi(\mu_2) e=\psi(\mu_2 e)$ and $\psi^f(\mu_1 e)=\psi^f(\mu_1)=\psi^f(\mu_2)=\psi^f(\mu_2 e)$.

\emph{Case 2:} $e=o(i) \in \Sigma^o$.
Since $\mu_1o(i) \in \mathcal{L}(G_{S_1})$, by (\ref{Eq2}), $x_1=(\sigma_1,n_1)\cdots (\sigma_k,n_k) \neq\varepsilon$, $i\in [1,k]$, and $n_1+1\le N_{l,o}$.
Since $x_1=x_2$ and $n_1=n_2$, we have $\mu_1o(i) \in \mathcal{L}(G_{S_2})$.
Let us write $\tilde{\delta}_2(\tilde{q}_{0,2},\mu_2 e)=(q'_2,x'_2,n'_2,\phi'_2,y'_2,m'_2,p'_2)$.
By (\ref{Eq2}), $q'_2=q_2$, $$x'_2=(\sigma_1,n_1) \cdots (\sigma_{i-1},n_{i-1})(\sigma_{i+1},n_{i+1})\cdots (\sigma_k,n_k),$$  $n'_2=n_2+1$, $\phi_2'=\phi_2$, $y'_2=y_2$, and $m_2'=m_2$.
Moreover, since  $\tilde{\delta}_1(\tilde{q}_{0,1},\mu_1 e)=(q'_1,x'_1,n'_1,\phi'_1,y'_1,m'_1,p'_{1})$,
by (\ref{Eq2}), $q'_1=q_1$, $$x'_1=(\sigma_1,n_1)\cdots (\sigma_{i-1},n_{i-1})(\sigma_{i+1},n_{i+1})\cdots (\sigma_k,n_k),$$ $n'_1=n_1+1$, $\phi_1'=\phi_1$, $y'_1=y_1$, and $m_1'=m_1$.
Hence, we have $x'_1=x'_2$.
Since $n_1=n_2$, $n'_1=n_1+1$, and $n'_2=n_2+1$, we have $n'_1=n'_2$.
Moreover, by the induction hypothesis, $q_2=q_1$,  $\phi_1\subseteq \phi_2$, $y_1\preceq y_2$, and $m_2=m_1$.
Sicne $q'_1=q_1$, $\phi_1'=\phi_1$, $y'_1=y_1$, $m_1'=m_1$,  $q'_2=q_2$, $\phi_2'=\phi_2$, $y'_2=y_2$, and $m_2'=m_2$, we have $q'_2=q'_1$, $\phi'_1 \subseteq \phi'_2$, $y'_1 \preceq y'_2$, and  $m'_2=m'_1$.
Overall, we have $q'_1=q'_2$, $x'_1=x'_2$, $n'_1=n'_2$, $\phi_1'\subseteq \phi_2'$, $y'_1 \preceq y'_2$, and $m_1'=m_2'$.
Since  $\psi(\mu_1)=\psi(\mu_2)$ and $\psi^f(\mu_1)=\psi^f(\mu_2)$, by definitions, $\psi(\mu_1 e)=\psi(\mu_1)=\psi(\mu_2)=\psi(\mu_2 e)$ and $\psi^f(\mu_1 e)=\psi^f(\mu_1)=\psi^f(\mu_2)=\psi^f(\mu_2 e)$.

\emph{Case 3:}  $e=c(i) \in \Sigma^c$.
Since $\mu_1c(i) \in \mathcal{L}(G_{S_1})$, by (\ref{Eq3}), $y_1=(\pi_1,l_1)\cdots (\pi_h,l_h) \neq\varepsilon$, $i \in [1,h]$, and $m_1+1\le N_{l,c}$.
Since $y_1 \preceq y_2$, by definition, $y_2=(\pi'_1,l'_1) \cdots (\pi'_h, l'_h)$ such that $\pi_i \subseteq \pi_i'$ and $l_i=l_i'$ for all $i \in [1,h]$.
Then, by (\ref{Eq3}), we have $\mu_2c(i) \in \mathcal{L}(G_{S_2})$.
We write $\tilde{\delta}_2(\tilde{q}_{0,2},\mu_2 e)=(q'_2,x'_2,n'_2,\phi'_2,y'_2,m'_2,p'_2)$.
By (\ref{Eq3}), $q'_2=q_2$, $x'_2=x_2$, $n'_2=n_2$, $\phi_2'=\phi_2$, $m_2'=m_2+1$, and $$y'_2=(\pi'_1,l'_1) \cdots (\pi'_{i-1},l'_{i-1})(\pi'_{i+1},l'_{i+1})\cdots (\pi'_h,l'_h).$$
Since  $\tilde{\delta}_1(\tilde{q}_{0,1},\mu_1 e)=(q'_1,x'_1,n'_1,\phi'_1,y'_1,m'_1,p'_{1})$,
by (\ref{Eq3}),  $q'_1=q_1$, $x'_1=x_1$, $n'_1=n_1$, $\phi_1'=\phi_1$,  $m_1'=m_1+1$, and $$y'_1=(\pi_1,l_1) \cdots (\pi_{i-1},l_{i-1})(\pi_{i+1},l_{i+1})\cdots (\pi_h,l_h).$$
Since $\pi_i \subseteq \pi_i'$ and $l_i=l_i'$ for all $i \in [1,h]$,  $y'_1 \preceq y'_2$.
Since $m_1=m_2$, $m'_1=m_1+1$, and $m'_2=m_2+1$,  $m'_1=m'_2$.
Moreover, by the induction hypothesis, $q_2=q_1$, $x_2=x_1$, $n_2=n_1$, and $\phi_1\subseteq \phi_2$.
Sicne $q'_1=q_1$, $x'_1=x_1$, $n_1'=n_1$, $\phi_1'=\phi_1$, $q'_2=q_2$, $x'_2=x_2$, $n_2'=n_2$, and $\phi_2'=\phi_2$, we have $q'_2=q'_1$, $x'_2=x'_1$, $n_2'=n_1'$, and $\phi'_1 \subseteq \phi'_2$.
Overall, we have $q'_2=q'_1$, $x'_2=x'_1$, $n'_2=n'_1$, $\phi'_1\subseteq \phi'_2$, $y'_1 \preceq y'_2$, and $m'_2=m'_1$.
Since  $\psi(\mu_1)=\psi(\mu_2)$ and $\psi^f(\mu_1)=\psi^f(\mu_2)$, by definitions, $\psi(\mu_1 e)=\psi(\mu_1)=\psi(\mu_2)=\psi(\mu_2 e)$ and $\psi^f(\mu_1 e)=\psi^f(\mu_1)=\psi^f(\mu_2)=\psi^f(\mu_2 e)$.

\emph{Case 4:} $e=f(\sigma) \in \Sigma^f$.
Since $\mu_1f(\sigma) \in \mathcal{L}(G_{S_1})$, by (\ref{Eq4}),  $x_1=(\sigma_1,n_1)\cdots (\sigma_k,n_k) \neq \varepsilon$ and $\sigma=\sigma_1$.
Since $x_1=x_2$, by (\ref{Eq4}),  $\mu_2f(\sigma) \in \mathcal{L}(G_{S_2})$.
We write $$\tilde{\delta}_2(\tilde{q}_{0,2},\mu_2 e)=(q'_2,x'_2,n'_2,\phi'_2,y'_2,m'_2,p'_2).$$
By (\ref{Eq4}), $q'_2=q_2$, $x'_2=(\sigma_2,n_2) \cdots (\sigma_k,n_k)$, $n'_2=0$, $\phi_2'=\phi_2$, $y'_2=y_2(\gamma_2(p_2,\sigma),0)$, and $m_2'=m_2$.
We write $t=f^{-1}(\psi^f(\mu_2))$.
By Proposition \ref{Prop1}, we have $\zeta_2(x_{0,2},t)=p_2$.
Thus, $\gamma_2(\zeta_2(p_2,\sigma))=S_2(t\sigma)$ and  $y'_2=y_2(S_2(t\sigma),0)$.
Furthermore, since  $\tilde{\delta}_1(\tilde{q}_{0,1},\mu_1 e)=(q'_1,x'_1,n'_1,\phi'_1,y'_1,m'_1, p'_{1})$,
by (\ref{Eq4}), $q'_1=q_1$, $x'_1=(\sigma_2,n_2) \cdots (\sigma_k,n_k)$, $n'_1=0$, $\phi_1'=\phi_1$, $y'_1=y_1(\gamma_1(p_1,\sigma),0)$, and $m_1'=m_1$.
Therefore,  $x'_1=x_2'$ and $n'_1=n_2'=0$.
Meanwhile, since $f^{-1}(\psi^f(\mu_1))=f^{-1}(\psi^f(\mu_2))$, we know $f^{-1}(\psi^f(\mu_1))=t$.
By Proposition \ref{Prop1}, $p_1=\zeta_1(x_{0,1},t)$.
Hence, $\gamma_1(p_1,\sigma)=S_1(t\sigma)$ and $y'_1=y_1(S_1(t\sigma),0)$.
Sicne $y'_1=y_1(S_1(t\sigma),0)$, $y'_2=y_2(S_2(t\sigma),0)$, $y_1 \preceq y_2$, and $S_1(t\sigma) \subseteq  S_2(t\sigma)$, we have $y_1'\preceq y_2'$.
Meanwhile, by the induction hypothesis, $q_2=q_1$, $\phi_1 \subseteq \phi_2$, and $m_2=m_1$.
Since $q'_1=q_1$, $\phi_1'=\phi_1$, $m_1'=m_1$, $q'_2=q_2$, $\phi_2'=\phi_2$, and $m_2'=m_2$, we have $q'_2=q'_1$, $\phi'_1 \subseteq \phi'_2$, and $m'_2=m'_1$.
Overall, we have $q'_2=q'_1$, $x'_2=x'_1$, $n'_2=n'_1$, $\phi'_1\subseteq \phi'_2$, $y'_1 \preceq y'_2$, and $m'_2=m'_1$.
Since  $\psi(\mu_1)=\psi(\mu_2)$ and $\psi^f(\mu_1)=\psi^f(\mu_2)$, by definitions, $\psi(\mu_1 e)=\psi(\mu_1)=\psi(\mu_2)=\psi(\mu_2 e)$ and $\psi^f(\mu_1 e)=\psi^f(\mu_1)e=\psi^f(\mu_2)e=\psi^f(\mu_2 e)$.

\emph{Case 5:} $e=g(\pi) \in \Sigma^g$.
Since $\mu_1g(\pi) \in \mathcal{L}(G_{S_1})$, by (\ref{Eq5}), $y_1 \neq \varepsilon$.
Let us write $y_1=(\pi_1,l_1)\cdots (\pi_h,l_h)$ for $\pi_i\in \Pi$ and $l_i \le N_c$.
Then, $\pi=\pi_1$.
Since $y_1 \preceq y_2$,  $y_1=(\pi'_1,l'_1)\cdots (\pi'_h,l'_h)$ with $\pi_i \subseteq \pi_i'$ and $l_i=l_i'$.
By (\ref{Eq5}), $\mu_2e' \in \mathcal{L}(G_{S_2})$ with $e'=g(\pi_1')$.
We write $\tilde{\delta}_2(\tilde{q}_{0,2},\mu_2 e')=(q'_2,x'_2,n'_2,\phi'_2,y'_2,m'_2,p'_2)$.
By (\ref{Eq5}), $q'_2=q_2$, $x'_2=x_2$, $n'_2=n_2$, $\phi_2'=\pi_1'$, $y'_2=(\pi'_2,l'_2)\cdots (\pi'_h,l'_h)$, and $m_2'=0$.
Furthermore, since  $\tilde{\delta}_1(\tilde{q}_{0,1},\mu_1 e)=(q'_1,x'_1,n'_1,\phi'_1,y'_1, m'_1, p'_{1})$,
by (\ref{Eq5}), we have $q'_1=q_1$, $x'_1=x_1$, $n'_1=n_1$, $\phi_1'=\pi_1$, $y'_1=(\pi_2,l_2)\cdots (\pi_h, l_h)$, and $m_1'=0$.
Since $\pi_1\subseteq \pi_2$, we have $\phi_1'\subseteq \phi_2'$.
Since  $y'_1=(\pi_2,l_2)\cdots (\pi_h, l_h)$ and $y'_2=(\pi'_2,l'_2)\cdots (\pi'_h,l'_h)$, we have $y'_1 \preceq y'_2$.
Since $m_1'=0$ and $m_2'=0$, we know $m_1'=m_2'$.
Meanwhile, by the induction hypothesis, $q_2=q_1$, $x_2=x_1$, and  $n_2=n_1$.
Since $q'_1=q_1$, $x'_1=x_1$, $n'_1=n_1$, $q'_2=q_2$, $x'_2=x_2$, and $n'_2=n_2$, we have $q'_1=q'_2$, $x'_1=x'_2$, and $n'_1=n'_2$.
Overall, we have $q'_1=q'_2$, $x'_1=x'_2$, $n'_1=n'_2$, $\phi_1'\subseteq \phi_2'$, $y'_1 \preceq y'_2$, and $m_1'=m_2'$.
Since  $\psi(\mu_1)=\psi(\mu_2)$ and $\psi^f(\mu_1)=\psi^f(\mu_2)$, by definitions, $\psi(\mu_1 e)=\psi(\mu_1)=\psi(\mu_2)=\psi(\mu_2 e')$ and $\psi^f(\mu_1 e)=\psi^f(\mu_1)=\psi^f(\mu_2)=\psi^f(\mu_2 e')$.

By the above proof, we know for all $\mu_1 \in \mathcal{L}(G_{S_1})$, $\exists \mu_2 \in \mathcal{L}(G_{S_2})$ such that $\psi(\mu_1)=\psi(\mu_2)$.
Hence, $\psi(\mathcal{L}(G_{S_1}))\subseteq \psi(\mathcal{L}(G_{S_2}))$.
By Definition \ref{Def1}, $\mathcal{L}(S_1/G) \subseteq \mathcal{L}(S_2/G)$.
\end{proof}

\subsection{Proof of Proposition \ref{Prop3}}

\begin{proof}
Let us first define
\begin{align*}
& \mathcal{T}(t)=\{(q,\theta_o,\theta_c): (\exists \mu \in \mathcal{L}(G_S))f^{-1}(\psi^f(\mu))=t \wedge \tilde{\delta}(\tilde{q}_0,\mu)\\
& =(a,x,n,\phi,y,m,p)\wedge q=a \wedge \theta_o=(x,n) \wedge \theta_c=(\phi,y,m)\}.
\end{align*}
Next, we prove $\tilde{\mathcal{E}}_S(t)\subseteq \mathcal{T}(t)$ by induction on the length of  $t \in f^{-1}(\psi^f(\mathcal{L}(G_S)))$.

\textbf{Base case:} For any $z=(q,\theta_c,\theta_o) \in \tilde{\mathcal{E}}_S(\varepsilon)$, by the definition of $\textup{DUR}(\cdot)$,  there exists a sequence of augmented states $z_0z_1 \cdots z_k$ such that $z_0=(q_0,(\varepsilon,0),(S(\varepsilon),\varepsilon,0))$, $z_k=z$, and $z_i$ is the augmented state calculated by applying one of operations in (\ref{Eq8})$\sim$(\ref{Eq11}) on $z_{i-1}$, $i=1,\ldots,k$.
Since the initial state of $G_S$ is $z_0=(q_0, \varepsilon, 0, S(\varepsilon), \varepsilon, 0, x_0)$, by the definition of $\mathcal{T}(\cdot)$, $z_0 \in {\mathcal{T}}(\varepsilon)$.
Next, we have the following claim.
\begin{claim}\label{Cla1}
For any $t \in f^{-1}(\psi^f(\mathcal{L}(G_S)))$, if $z \in \mathcal{T}(t)$ and $z'$ is the augmented state obtained by applying one of operations in (\ref{Eq8})$\sim$(\ref{Eq11}) on $z$, then $z' \in \mathcal{T}(t)$.
\end{claim}
We prove Claim \ref{Cla1} in Appendix C.
Since $z_0 \in {\mathcal{T}}(\varepsilon)$, by recursively applying Claim \ref{Cla1},  $z=z_k \in {\mathcal{T}}(\varepsilon)$.
Therefore, the base case holds, i.e., $\tilde{\mathcal{E}}_S(\varepsilon) \subseteq \mathcal{T}(\varepsilon)$.

\textbf{Induction hypothesis:} For all $t \in f^{-1}(\psi^f(\mathcal{L}(G_S)))$ with $|t|\le n$, we have $\tilde{\mathcal{E}}_S(t)\subseteq \mathcal{T}(t)$.
We next prove the same is also true for $t\sigma \in f^{-1}(\psi^f(\mathcal{L}(G_S)))$.

If $\tilde{\mathcal{E}}_S(t\sigma)=\emptyset$, then $\tilde{\mathcal{E}}_S(t\sigma)\subseteq \mathcal{T}(t\sigma)$ is trivially true.
Otherwise, for any $z \in \tilde{\mathcal{E}}_S(t\sigma)$, by the definitions of $\textup{DOR}(\cdot)$ and $\textup{DUR}(\cdot)$, there exists a sequence of augmented states $z_0z_1 \cdots z_k$ such that (i) $z_0$ is the augmented state calculated by applying successively (\ref{Eq12}) and (\ref{Eq7}) on some $(q,\theta_o,\theta_c) \in \tilde{\mathcal{E}}_S(t)$, i.e., $z_0=(q, \textbf{OUT}^{obs}(\theta_o),\textbf{IN}^{ctr}(\theta_c,S(t\sigma)))$, (ii) $z_k=z$, and (iii) $z_i$ is the augmented state calculated by applying one of operations in (\ref{Eq8})$\sim$(\ref{Eq11}) on $z_{i-1}$, $i=1,\ldots,k$.

Next, we prove $z_0 \in {\mathcal{T}}(t\sigma)$.
Since $(q,\theta_o,\theta_c) \in \tilde{\mathcal{E}}_S(t) \subseteq \mathcal{T}(t)$, there exists $\mu \in \mathcal{L}(G_S)$ with $f^{-1}(\psi^f(\mu))=t$ and $\tilde{\delta}(\tilde{q}_0,\mu)=(a,x,n,\phi,y,m,p)$ such that $q=a$, $\theta_o=(x,n)$, and $\theta_c=(\phi,y,m)$.
Since $\textbf{OUT}^{obs}(\theta_o)$ is defined, we have $x \neq \varepsilon$.
We write $x=(\sigma_1,n_1)\cdots (\sigma_k,n_k)$ for $\sigma_i\in \Sigma_o$ and $n_i \in [0,N_o]$.
Then, by (\ref{Eq4}), $\tilde{\delta}(\tilde{q}_0,\mu f(\sigma))=(a',x',n',\phi',y',m',p')$, where $a'=a$, $x'=(\sigma_2,n_2)\cdots (\sigma_k,n_k)$,  $n'=0$, $\phi'=\phi$, $y'=y(\gamma(\zeta(p,\sigma)),0)$, $m'=m$, and $p'=\zeta(p,\sigma)$.
Since $f^{-1}(\psi^f(\mu f(\sigma)))=t\sigma$, by the definition of $\mathcal{T}(\cdot)$,  $(a',(x',n'),(\phi',y',m'))\in \mathcal{T}(t\sigma)$.
Since $f^{-1}(\psi^f(\mu))=t$, by Proposition \ref{Prop1},  $p=\zeta(x_0,t)$.
Hence, $\zeta(p,\sigma)=\zeta(x_0,t\sigma)$.
By definition, $\gamma(\zeta(p,\sigma))=S(t\sigma)$.
Therefore, $y'=y(\gamma(\zeta(p,\sigma)),0)=y(S(t\sigma),0)$.
Moreover, since $a'=q$, $\phi'=\phi$, $n'=0$, and $m'=m$, we have $$(a',(x',n'),(\phi',y',m'))=(q,(x',0),(\phi,y(S(t\sigma),0),m))\in \mathcal{T}(t\sigma).$$

Since $\theta_o=(x,n)$, by the definition of $\textbf{OUT}^{obs}(\cdot)$,  $\theta'_o=(x',0)$.
Since $\theta_c=(\phi,y,m)$, by the definition of $\textbf{IN}^{ctr}(\cdot)$, $\textbf{IN}^{ctr}(\theta_c,S(t\sigma))=(\phi,y(S(t\sigma),0),m)$.
Therefore,
\begin{align*}
z_0&=(q, \textbf{OUT}^{obs}(\theta_o),\textbf{IN}^{ctr}(\theta_c,S(t\sigma)))\\
&=(q,(x',0),(\phi,y(S(t\sigma),0),m))\in \mathcal{T}(t\sigma).
\end{align*}
Since $z_0 \in {\mathcal{T}}(t\sigma)$, by recursively applying  Claim \ref{Cla1},  $z=z_k \in {\mathcal{T}}(t\sigma)$.
Therefore, $\tilde{\mathcal{E}}_S(t\sigma) \subseteq \mathcal{T}(t\sigma)$.
That completes the proof.
\end{proof}

\subsection{Proof of Claim \ref{Cla1}}

\begin{proof}

Write $z=(q,\theta_{o},\theta_{c})$ and $z'=(q',\theta'_{o},\theta'_{c})$.
Since $z \in \mathcal{T}(t)$, there exists a $\mu \in \mathcal{L}(G_S)$ such that $f^{-1}(\psi^f(\mu))=t$ and $\tilde{\delta}(\tilde{q}_0,\mu)=\tilde{q}=(a,x,n,\phi,y,m,p)$ with $q=a$, $\theta_{o}=(x,n)$, and $\theta_{c}=(\phi,y,m)$.
Since $z'$ is the augmented state obtained by applying one of operations in (\ref{Eq8})$\sim$(\ref{Eq11}) on $z$, one of the following four cases must be true.

\emph{{Case 1:}}
$z'=(\delta(q,\sigma), \textbf{IN}^{obs}(\theta_{o},\sigma),\textbf{PLUS}(\theta_{c}))$.
By (\ref{Eq8}), there exists a $\sigma \in \Sigma$ with $\delta(q,\sigma)!$, $\sigma \in [\theta_{c}]_1$, $\textbf{NUM}([\theta_{o}]_1)+1\le N_o$, $\textbf{NUM}([\theta_{c}]_2)+1 \le N_c$.
Since $q=a$, $[\theta_{c}]_1=\phi$, $[\theta_{o}]_1=x$, and $[\theta_{c}]_2=y$, we have $\delta(a,\sigma)!$,  $\sigma \in \phi$, $\textbf{NUM}(x)+1\le N_o$, and $\textbf{NUM}(y)+1 \le N_c$.
By (\ref{Eq1}), $\sigma$ is defined at $\tilde{q}$ in $G_S$.
Let us write $\tilde{\delta}(\tilde{q},\sigma)=\tilde{\delta}(\tilde{q}_0,\mu\sigma)=(a',x',n',\phi',y',m',p')$.
By (\ref{Eq1}), we have  $a'=\delta(a,\sigma)$, $x'=x^+(\sigma,0)$ if $\sigma \in \Sigma_o$, $x'=x^+$ if $\sigma \in \Sigma_{uo}$,  $n'=n$, $\phi'=\phi$,  $y'=y^+$, $m'=m$, and $p'=p$.
Since $\sigma \in \Sigma$, we have $f^{-1}(\psi^f(\mu\sigma))=f^{-1}(\psi^f(\mu))=t$.
By the definition of $\mathcal{T}(\cdot)$, we know if $\sigma \in \Sigma_o$, $(a',(x', n'),(\pi', y',m'))=(\delta(a,\sigma),(x^+(\sigma,0),n),(\phi, y^+,m))\in \mathcal{T}(t)$, and if $\sigma \in \Sigma_{uo}$, $(a',(x', n'),(\pi', y',m'))=(\delta(a,\sigma),(x^+,n),(\phi, y^+,m))\in \mathcal{T}(t)$.
By the definition of $\textbf{IN}^{obs}(\cdot)$,  if $\sigma \in \Sigma_o$, $\textbf{IN}^{obs}(\theta_{o},\sigma)=(x^+(\sigma,0),n)$, and if $\sigma \in \Sigma_{uo}$, $\textbf{IN}^{obs}(\theta_{o},\sigma)=(x^+,n)$.
By the definition of $\textbf{PLUS}(\cdot)$, $\textbf{PLUS}(\theta_{c})=(\phi, y^+,m)$.
Moreover, since $q=a$,  $z'=(\delta(q,\sigma), \textbf{IN}^{obs}(\theta_{o},\sigma),\textbf{PLUS}(\theta_{c}))\in \mathcal{T}(t)$.

\emph{{Case 2:}}
$z'=(q, \theta_{o},\textbf{OUT}^{ctr}(\theta_{c}))$.
By (\ref{Eq9}), $[\theta_{c}]_2 \neq \varepsilon$. Thus, $y \neq\varepsilon$.
We write $y=(\pi_1,m_1)\cdots (\pi_h,m_h)$ for $\pi_i \in \Pi$ and $m_i \le N_c$.
By (\ref{Eq5}), $g(\pi_1)$ is defined at $\tilde{q}$ in $G_S$.
Write $\tilde{\delta}(\tilde{q},g(\pi_1))=\tilde{\delta}(\tilde{q}_0,\mu\sigma)=(a',x',n',\phi',y',m',p')$.
By (\ref{Eq5}), $a'=a$, $x'=x$, $n'=n$, $\phi'=\pi_1$, $y'=(\pi_2,m_2)\cdots (\pi_h,m_h)$, $m'=0$, and $p'=p$.
Since $g(\pi_1) \in \Sigma_g$, $f^{-1}(\psi^f(\mu g(\pi_1)))=f^{-1}(\psi^f(\mu))=t$.
By the definition of $\mathcal{T}(\cdot)$, we have $(a',(x', n'),(\pi', y',m'))=(a,(x, n),(\pi_1, y',0))\in \mathcal{T}(t)$.
Sicne $\theta_c=(\phi,y,m)$, by the definition of $\textbf{OUT}^{ctr}(\cdot)$,  $\textbf{OUT}^{ctr}(\theta_{c})=(\pi_1,y',0)$.
Moreover, since $q=a$ and $\theta_o=(x,n)$, we have $z'=(q, \theta_{o},\textbf{OUT}^{ctr}(\theta_{c}))=(q,(x, n),(\pi_1, y',0)) \in \mathcal{T}(t)$.

\emph{{Case 3:}}
$z'=(q, \textbf{LOSS}^{obs}(\theta_{o},i),\theta_{c})$.
By (\ref{Eq10}), we have $[\theta_{o}]_1 \neq \varepsilon$, $[\theta_{o}]_2 +1 \le N_{l,o}$, and $i \in [1, |[\theta_{o}]_1|]$.
Since $[\theta_{o}]_1=x$ and $[\theta_{o}]_2=n$, we have $x \neq \varepsilon$, $n+1 \le N_{l,o}$, and $i \in [1, |x|]$.
We write $x=(\sigma_1,n_1)\cdots (\sigma_k,n_k)$ for $\sigma_i\in \Sigma_o$ and $n_i \le N_o$.
Since $i \in [1, |x|]=[1,k]$, by (\ref{Eq2}), $o(i)$ is defined at $\tilde{q}$ in $G_S$.
Let us write $\tilde{\delta}(\tilde{q},o(i))=\tilde{\delta}(\tilde{q}_0,\mu o(i))=(a',x',n',\phi',y',m',p')$.
Also by (\ref{Eq2}),  $a'=a$, $x'=(\sigma_1,n_1)\cdots (\sigma_{i-1},n_{i-1}) (\sigma_{i+1},n_{i+1})\cdots (\sigma_k,n_k),$  $n'=n+1$, $\phi'=\phi$, $y'=y$, $m'=m$, and $p'=p$.
Since $o(i) \in \Sigma^o$, we have  $f^{-1}(\psi^f(\mu o(i)))=f^{-1}(\psi^f(\mu))=t$.
By the definition of $\mathcal{T}(\cdot)$, $(a',(x', n'), (\phi', y', m'))=(a,(x', n+1), (\phi, y, m))\in \mathcal{T}(t)$.
Since $\theta_{o}=(x,n)$, by the definition of $\textbf{LOSS}^{obs}(\cdot)$, $\textbf{LOSS}^{obs}(\theta_{o},i)=(x',n+1)$.
Moreover, since $q=a$ and $\theta_c=(\phi, y, m)$, we have $z'=(q, \textbf{LOSS}^{obs}(\theta_{o},i),\theta_{c})=(a,(x', n+1), (\phi, y, m)) \in \mathcal{T}(t)$.

\emph{{Case 4:}}
$z'=(q, \theta_{o}, \textbf{LOSS}^{ctr}(\theta_{c},i))$.
By (\ref{Eq11}), we have $[\theta_{c}]_2  \neq \varepsilon$, $[\theta_{c}]_3+1 \le N_{l,c}$, and $i \in [1, |[\theta_{c}]_2|]$.
Moreover, since $\theta_{c}=(\phi,y,m)$, we have $y \neq \varepsilon$, $m+1 \le N_{l,c}$, and $i \in [1,|y|]$.
Write $y=(\pi_1,m_1)\cdots (\pi_h,m_h)$ for $\pi_i \in \Pi$ and $m_i \le N_c$.
Since $i \in [1,|y|]=[1,h]$, by (\ref{Eq3}),  $c(i)$ is defined at $\tilde{q}$ in $G_S$.
We write $\tilde{\delta}(\tilde{q},c(i))=\tilde{\delta}(\tilde{q}_0,\mu c(i))=(a',x',n',\phi',y',m',p')$.
By (\ref{Eq3}), we have $a'=a$, $x'=x$, $n'=n$, $\phi'=\phi$, $m'=m+1$, $p'=p$, and $y'=(\pi_1,m_1)\cdots (\pi_{i-1},m_{i-1}) (\pi_{i+1},m_{i+1})\cdots (\pi_h,m_h)$.
Since $c(i) \in \Sigma^c$,   $f^{-1}(\psi^f(\mu c(i)))=f^{-1}(\psi^f(\mu))=t$.
By the definition of $\mathcal{T}(\cdot)$,  $(a',(x', n'),(\phi', y', m'))=(a,(x,n),(\phi,y',m+1))\in \mathcal{T}(t)$.
By the definition of $\textbf{LOSS}^{ctr}(\cdot)$, $\textbf{LOSS}^{ctr}(\theta_{c},i)=(\phi,y',m+1)$.
Hence,  $\textbf{LOSS}^{ctr}(\theta_{o},i)=(\phi,y',m+1)$.
Moreover, since $q=a$ and $\theta_o=(x,n)$, $z'=(q, \theta_{o}, \textbf{LOSS}^{ctr}(\theta_{c},i))=(a,(x,n),(\phi,y',m+1)) \in \mathcal{T}(t)$.
\end{proof}

\subsection{Proof of Proposition \ref{Prop4}}
\begin{proof}
The proof is by induction on the length of $\mu \in \mathcal{L}(G_S)$.

\textbf{Base case:} By definition, $\tilde{\delta}(\tilde{q}_0,\varepsilon)=(q_0,\varepsilon, 0, S(\varepsilon),\varepsilon, 0, x_0)$.
Since $\tilde{\mathcal{E}}_S(\varepsilon)=\text{DUR}(\{(q_0,(\varepsilon,0),(\emptyset,\varepsilon,0))\},S(\varepsilon))$, by (\ref{Eq7}), we have $(q_0,(\varepsilon,0),(S(\varepsilon),\varepsilon,0)) \in \tilde{\mathcal{E}}_S(\varepsilon)$.
The base case is true.

\textbf{Induction hypothesis:} For all $\mu \in \mathcal{L}(G_S)$ with $|\mu| \le k$, we write  $\tilde{\delta}(\tilde{q}_0,\mu)=\tilde{q}=(a,x,n,\phi,y,m,p)$.
We also write $f^{-1}(\psi^f(\mu))=t$.
Then, $(q,\theta_c,\theta_o) \in \tilde{\mathcal{E}}_S(f^{-1}(\psi^f(\mu)))=\tilde{\mathcal{E}}_S(t)$, where $q=a$, $\theta_o=(x,n)$, and $\theta_c=(\phi,y,m)$.
We next prove the same is also true for $\mu e \in \mathcal{L}(G_S)$.

For any $\mu e \in \mathcal{L}(G_S)$ with $|\mu| = k$, let $\tilde{\delta}(\tilde{q}_0,\mu e)=\tilde{q}'=(a',x',n',\phi',y',m',p')$.
Since $\tilde{\delta}(\tilde{q}_0,\mu)=\tilde{q}$, $\tilde{\delta}(\tilde{q},e)=\tilde{q}'$.
Let $q'=a'$, $\theta'_o=(x',n')$, and $\theta'_c=(\phi',y',m')$.
We next prove $(q',\theta'_o,\theta'_c) \in \tilde{\mathcal{E}}_S(f^{-1}(\psi^f(\mu e)))$.
Since $e\in \tilde{\Sigma}$, one of the following cases must be true: (i) $e\in \Sigma$, (ii) $e \in \Sigma^o$, (iii) $e \in \Sigma^c$, (iv) $e \in \Sigma^g$, and (v) $e \in \Sigma^f$.
We consider each of them separately as follows.

\emph{Case 1:} $e \in \Sigma$. Since $e \in \Sigma$, $f^{-1}(\psi^f(\mu))=f^{-1}(\psi^f(\mu e))=t$.
Therefore, to prove $(q',\theta'_o,\theta'_c)\in \tilde{\mathcal{E}}_S(f^{-1}(\psi^f(\mu e)))$, we only need to prove $(q',\theta'_o,\theta'_c)\in \tilde{\mathcal{E}}_S(t)$.

Since $\tilde{\delta}(\tilde{q},e)=\tilde{q}'$,  by (\ref{Eq1}),   $\delta(a,e)!$, $e \in \phi$, $\textbf{NUM}(x)+1\le N_o$, and $\textbf{NUM}(y)+1 \le N_c$.
Since $\theta_o=(x,n)$ and $\theta_c=(\phi,y,m)$, we have $\delta(a,e)!$, $e \in [\theta_c]_1$, $\textbf{NUM}([\theta_o]_1)+1\le N_o$, and $\textbf{NUM}([\theta_c]_2)+1\le N_c$.
Moreover, since $(q=a,\theta_o,\theta_c) \in \tilde{\mathcal{E}}_S(t)$, by (\ref{Eq8}), $(\delta(a,e), \textbf{IN}^{obs}(\theta_o,e),  \textbf{PLUS}(\theta_c)) \in \tilde{\mathcal{E}}_S(t)$.

By (\ref{Eq1}), $a'=\delta(a,e)$,  $x'=x^+$ (if $e \in \Sigma_{uo}$),  $x'=x^+(e,0)$ (if $e \in \Sigma_{o}$), $n'=n$, $\phi'=\phi$, $y'=y^+$, and $m'=m$.
Therefore,  if $e \in \Sigma_{uo}$, $(q',\theta'_o,\theta'_c)=(\delta(a,e), (x^+,n),(\phi, y^+, m))$, and if $e \in \Sigma_{o}$, $(q',\theta'_o,\theta'_c)=(\delta(a,e), (x^+(e,0),n),(\phi, y^+, m))$.
Since $\theta_o=(x,n)$ and $\theta_c=(\phi,y,m)$,  we know if  $e \in \Sigma_{uo}$, $\textbf{IN}^{obs}(\theta_o,e)=(x^+,n)$ and $\textbf{PLUS}(\theta_c)=(\phi,y^+,m)$, and if $e \in \Sigma_{o}$, $\textbf{IN}^{obs}(\theta_o,e)=(x^+(e,0),n)$ and $\textbf{PLUS}(\theta_c)=(\phi,y^+,m)$.
Therefore, $(q',\theta'_o,\theta'_c)=(\delta(a,e), \textbf{IN}^{obs}(\theta_o,e),  \textbf{PLUS}(\theta_c))\in \tilde{\mathcal{E}}_S(t)$.

\emph{Case 2:} $e=o(i) \in \Sigma^o$.
Since $\tilde{\delta}(\tilde{q},o(i))=\tilde{q}'$ where $\tilde{q}=(a,x,n,\phi,y,m,p)$, by (\ref{Eq2}), we know $x \neq\varepsilon$, $i\in [1,|x|]$, and $n+1 \le N_{l,o}$.
We write $x=(\sigma_1,n_1)\cdots (\sigma_k,n_k)$ for $\sigma_i\in \Sigma_o$ and $n_i \in [0,N_o]$.
Since $\tilde{q}'=(a',x',n',\phi',y',m',p')$, by (\ref{Eq2}), we have $a'=a$, $x'=(\sigma_1,n_1)\cdots (\sigma_{i-1},n_{i-1})(\sigma_{i+1},n_{i+1})\cdots (\sigma_k,n_k),$ $n'=n+1$, $\phi'=\phi$, $y'=y$, and $m'=m$.
Therefore, $(q',\theta'_o,\theta'_c)=(a',(x',n'),(\phi', y', m'))=(a, (x',n+1),(\phi, y, m))$.
Since $\theta_o=(x,n)$, $x \neq \varepsilon$, $i \in [1,|x|]$, and $n+1\le N_{l,o}$, $\textbf{LOSS}^{obs}(\theta_o,i)=(x',n+1)$.
Moreover, since $\theta_c=(\phi,y,m)$, $(q',\theta'_o,\theta'_c)=(a, (x',n+1),\theta_c)=(a,\textbf{LOSS}^{obs}(\theta_o,i), \theta_c)$.
Since $(q=a,\theta_o,\theta_c) \in \tilde{\mathcal{E}}_S(t)$, by (\ref{Eq10}),  $(a,\textbf{LOSS}^{obs}(\theta_o,i),  \theta_c) \in \tilde{\mathcal{E}}_S(t)$.
Thus, $(q',\theta'_o,\theta'_c) \in \tilde{\mathcal{E}}_S(t)$.
Since $e \in \Sigma^o$,  $f^{-1}(\psi^f(\mu e))=f^{-1}(\psi^f(\mu))=t$.
Thus,  $(q',\theta'_o,\theta'_c) \in \tilde{\mathcal{E}}_S(f^{-1}(\psi^f(\mu e)))$.

\emph{{Case 3:}} $e=c(i) \in \Sigma^c$.
Since $\tilde{\delta}(\tilde{q},c(i))=\tilde{q}'$ where $\tilde{q}=(a,x,n,\phi,y,m,p)$, by (\ref{Eq3}), $y \neq\varepsilon$, $i \in [1,|y|]$, and $m+1 \le N_{l,c}$.
We write $y=(\pi_1,m_1)\cdots (\pi_h,m_h)$ for $\pi_i\in \Pi$ and $m_i \in [0,N_c]$.
Since $\tilde{q}'=(a',x',n',\phi',y',m',p')$, by (\ref{Eq3}),  $a'=a$, $x'=x$, $n'=n$, $\phi'=\phi$, $y'=(\pi_1,m_1)\cdots (\pi_{i-1},m_{i-1})(\pi_{i+1},m_{i+1}) \cdots (\pi_h,m_h),$ and $m'=m+1$.
Therefore, $(q',\theta'_o,\theta'_c)=(a',(x',n'),(\phi', y', m'))=(q, (x,n),(\phi, y', m+1))$.
Since $a'=a$ and $\theta_o=(x,n)$, $(q',\theta'_o,\theta'_c)=(a, \theta_o,(\phi, y', m+1))$.
Since $y \neq \varepsilon$, $i\in [1,|y|]$, and $m+1 \le N_{l,c}$, $\textbf{LOSS}^{ctr}(\theta_c,i)=(\phi, y', m+1)$.
Thus, $(q',\theta'_o,\theta'_c)=(a, \theta_o,(\phi, y', m+1))=(a, \theta_o, \textbf{LOSS}^{ctr}(\theta_{c},i))$.
Since $(q=a,\theta_o,\theta_c) \in \tilde{\mathcal{E}}_S(t)$, by (\ref{Eq11}),  $(a, \theta_o, \textbf{LOSS}^{ctr}(\theta_{c},i)) \in \tilde{\mathcal{E}}_S(t)$.
Thus,  $(q',\theta'_o,\theta'_c) \in \tilde{\mathcal{E}}_S(t)$.
Moreover, since $e \in \Sigma^c$, $f^{-1}(\psi^f(\mu e))=f^{-1}(\psi^f(\mu))=t$.
Therefore, $(q',\theta'_o,\theta'_c) \in \tilde{\mathcal{E}}_S(f^{-1}(\psi^f(\mu e)))$.

\emph{{Case 4:}} $e=g(\pi) \in \Sigma^g$.
Since $\tilde{\delta}(\tilde{q},g(\pi))=\tilde{q}'$ where $\tilde{q}=(a,x,n,\phi,y,m,p)$, by (\ref{Eq5}),  $y \neq\varepsilon$.
Write $y=(\pi_1,m_1)\cdots (\pi_h,m_h)$ for $\pi_i\in \Pi$ and $m_i \in [0,N_c]$.
Since $\tilde{q}'=(a',x',n',\phi',y',m',p')$, by (\ref{Eq5}), $a'=a$, $x'=x$, $n'=n$, $\phi'=\pi_1$, $y'=(\pi_2,m_2)\cdots (\pi_h,m_h),$ and $m'=m$.
Thus, $$(q',\theta'_o,\theta'_c)=(a', (x',n'),(\pi', y', m'))=(a, (x,n),(\pi_1, y', m)).$$
Since $\theta_o=(x,n)$,  $(q',\theta'_o,\theta'_c)=(a, \theta_o,(\phi, y', m))$.
Meanwhile, since $y\neq\varepsilon$, $\textbf{OUT}^{ctr}(\theta_c)=(\pi_1, y', m)$.
Therefore, $(q',\theta'_o,\theta'_c)=(a, \theta_o, \textbf{OUT}^{ctr}(\theta_{c}))$.
Since $(q=a,\theta_o,\theta_c) \in \tilde{\mathcal{E}}_S(t)$, by (\ref{Eq11}),  $(a, \theta_o, \textbf{OUT}^{ctr}(\theta_{c})) \in \tilde{\mathcal{E}}_S(t)$.
Thus, $(q',\theta'_o,\theta'_c) \in \tilde{\mathcal{E}}_S(t)$.
Moreover, since $e \in \Sigma^g$, $f^{-1}(\psi^f(\mu e))=f^{-1}(\psi^f(\mu))=t$.
Therefore, $(q',\theta'_o,\theta'_c) \in \tilde{\mathcal{E}}_S(f^{-1}(\psi^f(\mu e)))$.

\emph{{Case 5:}} $e=f(\sigma) \in \Sigma^f$.
Since $\tilde{\delta}(\tilde{q},f(\sigma))=\tilde{q}'$ were $\tilde{q}=(a,x,n,\phi,y,m,p)$, by (\ref{Eq4}),  $x \neq \varepsilon$.
Let us write $x=(\sigma_1,n_1)\cdots (\sigma_k,n_k)$ for $\sigma_i\in \Sigma_o$ and $n_i \le [0,N_o]$.
Since $\tilde{q}'=(a',x',n',\phi',y',m',p')$, by (\ref{Eq4}),  we know $a'=a$, $x'=(\sigma_2,n_2) \cdots(\sigma_k,n_k)$, $n'=0$, $\phi'=\phi$, $y'=y(\gamma(\zeta(p,\sigma)),0)$, and $m'=m$.
Thus, $(q',\theta'_o,\theta'_c)=(a',(x',n'),(\phi',y',m'))=(a, (x',0),(\phi, y', m))$.
Since $\tilde{\delta}(\tilde{q}_0,\mu)=\tilde{q}=(a,x,n,\phi,y,m,p)$, by Proposition \ref{Prop1}, $p=\zeta(x_0,f^{-1}(\psi^f(\mu)))=\zeta(x_0,t)$.
Since $p'=\zeta(p,\sigma)$, we have  $p'=\zeta(x_0, t\sigma)$.
By the definition of $S$, we know $\gamma(p')=S(t\sigma)$, which implies $y'=y(S(t\sigma),0)$.
Since $\theta_o=(x,n)$,  $\textbf{OUT}^{obs}(\theta_o)=(x', 0)$.
Meanwhile, since $\theta_c=(\phi,y,m)$, by the definition of $\textbf{IN}^{ctr}(\cdot)$, $\textbf{IN}^{ctr}(\theta_c, S(t\sigma))=(\phi, y(S(t\sigma),0), m)$.
Therefore, $(q',\theta'_o,\theta'_c)=(a, \textbf{OUT}^{obs}(\theta_o),\textbf{IN}^{ctr}(\theta_c,S(t\sigma)))$.
Since $(q=a,\theta_o,\theta_c) \in \tilde{\mathcal{E}}_S(t)$, by (\ref{Eq12}) and (\ref{Eq7}), $(a, \textbf{OUT}^{obs}(\theta_o),\textbf{IN}^{ctr}(\theta_c,S(t\sigma)))\in \textup{DUR}(\textup{DOR}(\tilde{\mathcal{E}}_S(t),\sigma),S(t\sigma))$.
By Definition \ref{Def3}, we have $(a, \textbf{OUT}^{obs}(\theta_o),\textbf{IN}^{ctr}(\theta_c,S(t\sigma))) \in \tilde{\mathcal{E}}_S(t\sigma)$.
Thus, $(q',\theta'_o,\theta'_c) \in \tilde{\mathcal{E}}_S(t\sigma)$.
Since $e=f(\sigma) \in \Sigma^f$, we have  $f^{-1}(\psi^f(\mu e))=t\sigma$.
Therefore, $(q',\theta'_o,\theta'_c) \in \tilde{\mathcal{E}}_S(f^{-1}(\psi^f(\mu e)))$.
\end{proof}

\bibliographystyle{IEEEtran}

redpajama_set_name: RedPajamaArXiv