A Topological Approach for Computing Supremal Sublanguages for Some Language Equations in Supervisory Control Theory

We have the next useful result, which is a straightforward consequence of the semi-topology endowed on $M$.

Remark: To make the paper more self-contained, we here briefly explain why the interior $M\backslash(M\backslash E)^{\square}$ is indeed the supremal open subset of $E$ in the semi-topology $(M,\mathcal{T})$. Let $M\backslash L^{\square}\subseteq E$ be any given open subset of $E$. We have $L^{\square}\supseteq M\backslash E$, from $M\backslash L^{\square}\subseteq E$, and thus $L^{\square}\supseteq(M\backslash E)^{\square}$. It then follows that $M\backslash L^{\square}\subseteq M\backslash(M\backslash E)^{\square}$. $M\backslash(M\backslash E)^{\square}$ is clearly an open subset of $E$.

Indeed, in the terminology of the rough set theory [18], $M\backslash(M\backslash E)^{\square}$ is the largest under-approximation of $E$ in the collection of open subsets of $E$.

The next result could be more convenient in some applications, which is a direct consequence of Theorem 1.

Corollary 1 states that, if the semi-topology induced by $\square$ on $M$ satisfies the following property ($*$): the family of open sets corresponds to the family of closed sets, then $M\backslash(M\backslash E)^{\square}$ is also the largest under-approximation of $E$ in the collection of closed subsets of $E$. We shall refer to any (semi-topological) closure operator that satisfies the property ($*$) as a clopen closure operator.

Theorem 1 can be used in the following way. Suppose we can formulate a property as the solutions of an equation $K=M\backslash(M\backslash K)^{\square}$, with $K\subseteq E\subseteq M$ and a function $\square:2^{M}\longrightarrow 2^{M}$. If $\square$ is a semi-topological closure operator, then this equation states that $K$ is equal to its interior $K^{\circ}$, that is, $K$ is open, in the semi-topology induced by $\square$ on $M$. Then, the supremal solution of this equation exists and is equal to the interior $E^{\circ}=M\backslash(M\backslash E)^{\square}$ of $E$.

Corollary 1 can be used in a similar manner. Suppose we can formulate a property as the solutions of an equation $K=K^{\square}$, with $K\subseteq E\subseteq M$ and a function $\square:2^{M}\longrightarrow 2^{M}$. If $\square$ is a clopen closure operator, then the supremal solution of this equation exists and is equal to the interior $E^{\circ}=M\backslash(M\backslash E)^{\square}$ of $E$.

Remark: If $\square$ is a clopen closure operator, then $K=K^{\square}$ ($K$ is a closed set) if and only if $K=M\backslash(M\backslash K)^{\square}=K^{\circ}$ ($K$ is an open set).

In the rest of this paper, for generality, we mostly only consider equations of the form $K=M\backslash(M\backslash K)^{\square}$. However, we shall work with the equation $K=K^{\square}$ if $\square$ is a clopen closure operator and it is more convenient to do so.

Let $M_{i}\subseteq\Sigma^{*}$ be any given language and let $\square_{i}:2^{M_{i}}\longrightarrow 2^{M_{i}}$ be any semi-topological closure operator on $M_{i}$, for each $i\in[1,n]$. Let $E\subseteq\bigcap_{i=1}^{n}M_{i}$.

Consider a system $\Delta$ of language equations in the topologized forms

with $K\subseteq E$. Thus, any solution of this system is an open set in the semi-topology induced by $\square_{i}$ on $M_{i}$, for each $i\in[1,n]$. By T2, the supremal solution exists, and it can be successively approximated with the iteration scheme

where $K_{0}=E$, and each function $\circ_{i}:2^{M_{i}}\longrightarrow 2^{M_{i}}$ is a semi-topological interior operator that is dual to $\square_{i}$, with $K^{\circ_{i}}:=M_{i}\backslash(M_{i}\backslash K)^{\square_{i}}$ for any $K\subseteq M_{i}$. The correctness of the iteration scheme is shown in the following.

Proof: The descending chain

is obtained. We first show that $K^{\uparrow}\subseteq K_{i}$ for each $i\geq 0$.

By definition, $(K^{\uparrow})^{\circ_{j}}=K^{\uparrow}$ for each $j\in[1,n]$. Thus, for each $i\geq 0$, $K^{\uparrow}\subseteq K_{i}$ implies $K^{\uparrow}\subseteq K_{i}^{\circ_{1}\circ_{2}\ldots\circ_{n}}=K_{i+1}$. The claim $K^{\uparrow}\subseteq K_{i}$, for each $i\geq 0$, follows from $K^{\uparrow}\subseteq E=K_{0}$. Thus, we have $K^{\uparrow}\subseteq K_{l}$.

Next, we show $K^{\uparrow}\supseteq K_{l}$. By definition, $K_{l}=K_{l+1}=K_{l}^{\circ_{1}\circ_{2}\ldots\circ_{n}}$. Thus, we have $K_{l}^{\circ_{j}}\subseteq K_{l}=K_{l}^{\circ_{1}\circ_{2}\ldots\circ_{n}}\subseteq K_{l}^{\circ_{j}}$, for each $j\in[1,n]$. That is, $K_{l}=K_{l}^{\circ_{j}}$ for each $j\in[1,n]$. With $K_{l}\subseteq E$, we know that $K_{l}$ is also a solution of the system $\Delta$ of equations. Thus, $K^{\uparrow}\supseteq K_{l}$. $\blacksquare$

In some cases, the topological approach given above cannot be directly applied. This is so, for example, when we need to search for the supremal solution of $K\subseteq E$, while the topological characterization only applies to $\overline{K}$. For example, consider the following system $\Theta$ of equations

where $K\subseteq E$. As before, $M_{i}\subseteq\Sigma^{*}$ is any given language and $\square_{i}:2^{M_{i}}\longrightarrow 2^{M_{i}}$ is a semi-topological closure operator (on $M_{i}$), for each $i\in[1,n]$. Here, $\overline{E}\subseteq\bigcap_{i=1}^{n}M_{i}$. The supremal solution for this system exists (see Proposition 2 for a generalization).

In this case, the use of the weakened requirement $\overline{K}\subseteq\overline{E}$ (for the search space) allows one to apply the topological techniques developed before for $\overline{K}$. However, this relaxation only computes the supremal solution of $\overline{K}$ from the topologized equations. The solution needs to be constrained as we only ask for the supremal solution of $K$, for which it holds that $K\subseteq\overline{K}\cap E$. This leads to a natural iteration scheme that successively approximates the supremal solution of $K$, subjected to the language equations for $\overline{K}$. Now, consider a more general setup, where we have a system $\Lambda$ of equations

where $K\subseteq E$. Here, $M_{i}$ and $\square_{i}$ are the same as before.

We assume $\square:2^{M}\longrightarrow 2^{M}$ is a semi-topological closure operator on some $M\subseteq\Sigma^{*}$ such that the equation $X=X^{\square}$ has an equivalent dual $X=M\backslash(M\backslash X)^{\square^{\prime}}$ for some semi-topological closure operator $\square^{\prime}:2^{M}\longrightarrow 2^{M}$. Let $E^{\square}\subseteq\bigcap_{i=1}^{n}M_{i}$.

Then, the following iteration scheme ($\#$) works for the system $\Lambda$, by replacing $K^{\square}$ with $X$.

1. 1.

   Let $i=0$ and $K_{i}=E$.

2. 2.

   Solve the following system $\Gamma(i)$ of equations

   	$\displaystyle X=M\backslash(M\backslash X)^{\square^{\prime}},$
   	$\displaystyle X=M_{1}\backslash(M_{1}\backslash X)^{\square_{1}},$
   	$\displaystyle X=M_{2}\backslash(M_{2}\backslash X)^{\square_{2}},$
   	$\displaystyle\ldots,$
   	$\displaystyle X=M_{n}\backslash(M_{n}\backslash X)^{\square_{n}},$

   where $X\subseteq K_{i}^{\square}$. The supremal solution $X_{i}$ exists, as for the system $\Delta$, and can be computed with the iteration scheme as given below.

   $$L_{j+1}=L_{j}^{\circ_{1}\circ_{2}\ldots\circ_{n}\circ^{\prime}},$$

   where $L_{0}=K_{i}^{\square}$. Let $K_{i+1}=K_{i}\cap X_{i}$. Let $i:=i+1$ and repeat step 2).

Remark: The system $\Lambda$ contains the system $\Theta$ as a special case. Indeed, let $\square:2^{\Sigma^{*}}\longrightarrow 2^{\Sigma^{*}}$ be defined such that $K^{\square}=\overline{K}$ for any $K\subseteq\Sigma^{*}$. $\square$ is a semi-topological closure operator on $\Sigma^{*}$ and the equation $X=X^{\square}$ has an equivalent dual $X=\Sigma^{*}\backslash(\Sigma^{*}\backslash X)^{\square^{\prime}}$, where $\square^{\prime}:2^{\Sigma^{*}}\longrightarrow 2^{\Sigma^{*}}$ is a semi-topological closure operator on $\Sigma^{*}$ defined such that $L^{\square^{\prime}}=L\Sigma^{*}$ for any $L\subseteq\Sigma^{*}$. Indeed, we have $X=\overline{X}$ iff $\overline{X}\subseteq X$ iff $\overline{X}\cap(\Sigma^{*}\backslash X)=\varnothing$ iff $X\cap(\Sigma^{*}\backslash X)\Sigma^{*}=\varnothing$ iff $X\subseteq\Sigma^{*}\backslash(\Sigma^{*}\backslash X)\Sigma^{*}$ iff $X=\Sigma^{*}\backslash(\Sigma^{*}\backslash X)\Sigma^{*}$. The system $\Lambda$ also contains the system $\Delta$ as a special case, by setting $K^{\square}=K$ for any $K\subseteq\Sigma^{*}$.

Before we show the correctness of the iteration scheme given above, we first show some useful results.

Proof: Suppose $\square:2^{M}\longrightarrow 2^{M}$ is a clopen closure operator on $M$. Then, for any language $L\subseteq M$, $L$ satisfies the equation $X=X^{\square}$ (that is, $L$ is a closed set) iff $L$ satisfies the equation $X=M\backslash(M\backslash X)^{\square}$ (that is, $L$ is an open set). We can choose $\square^{\prime}:=\square$. $\blacksquare$

Remark: $\square$ being a clopen closure operator on $M$ is a sufficient, but in general not necessary, condition for $X=X^{\square}$ to have an equivalent dual $X=M\backslash(M\backslash X)^{\square^{\prime}}$, for some semi-topological closure operator $\square^{\prime}$. For example, $K=\overline{K}$ has an equivalent dual $K=\Sigma^{*}\backslash(\Sigma^{*}\backslash K)\Sigma^{*}$ but the prefix closure operator is a semi-topological closure operator on $\Sigma^{*}$ that is not clopen.

We have the next useful result.

Proof: Each $K_{\alpha}$ satisfies the equation $X=X^{\square}$. Thus, $K_{\alpha}=M\backslash(M\backslash K_{\alpha})^{\square^{\prime}}$ for each $\alpha\in I$. That is, each $K_{\alpha}$ is an open set for the semi-topology on $M$ induced by $\square^{\prime}$. It follows that $\bigcup_{\alpha\in I}K_{\alpha}$ is also an open set and thus it satisfies the equation $X=M\backslash(M\backslash X)^{\square^{\prime}}$. It then follows that $\bigcup_{\alpha\in I}K_{\alpha}$ satisfies the equation $X=X^{\square}$, that is, $\bigcup_{\alpha\in I}K_{\alpha}$ is a closed set in the semi-topology induced by $\square$. The statement holds even when $I$ is an empty index set, for which we have $\bigcup_{\alpha\in I}K_{\alpha}=\varnothing$. $\blacksquare$

We now show the following result.

Proof: Since $\square$ is a semi-topological closure operator on $M$, we have $\varnothing^{\square}=\varnothing$; we have that $\varnothing$ is a solution of the system $\Lambda$. Let $\{K_{\alpha}\mid\alpha\in I\}$ be any (non-empty) set of solutions of the system $\Lambda$. We show that $\bigcup\{K_{\alpha}\mid\alpha\in I\}$ is also a solution of the system $\Lambda$. We only need to show that, for each $i\in[1,n]$,

We have that $(\bigcup\{K_{\alpha}\mid\alpha\in I\})^{\square}\supseteq\bigcup_{\alpha\in I}K_{\alpha}^{\square}$. Thus,

It follows that

$(M_{i}\backslash(\bigcup\{K_{\alpha}\mid\alpha\in I\})^{\square})^{\square_{i}}\subseteq(\bigcap_{\alpha\in I}(M_{i}\backslash K_{\alpha}^{\square}))^{\square_{i}}\subseteq\bigcap_{\alpha\in I}(M_{i}\backslash K_{\alpha}^{\square})^{\square_{i}}.$

Thus,

$M_{i}\backslash(M_{i}\backslash(\bigcup\{K_{\alpha}\mid\alpha\in I\})^{\square})^{\square_{i}}\supseteq M_{i}\backslash\bigcap_{\alpha\in I}(M_{i}\backslash K_{\alpha}^{\square})^{\square_{i}}=\bigcup_{\alpha\in I}M_{i}\backslash(M_{i}\backslash K_{\alpha}^{\square})^{\square_{i}}=\bigcup_{\alpha\in I}K_{\alpha}^{\square}$.

By Lemma 2, we have that

This finishes the proof. $\blacksquare$

The correctness of the successive approximation scheme is shown below.

Proof: The descending chain

is obtained from the iteration scheme. We first show that $K_{i}\supseteq K^{\uparrow}$ for each $i\geq 0$.

To that end, we shall show that, for any $i\geq 0$, $K_{i}\supseteq K^{\uparrow}$ implies $K_{i+1}\supseteq K^{\uparrow}$. Since $K_{i+1}=K_{i}\cap X_{i}$, we only need to show that $K_{i}\supseteq K^{\uparrow}$ implies $X_{i}\supseteq K^{\uparrow}$, where $X_{i}$ is the supremal solution of the system $\Gamma(i)$ of equations

where $X\subseteq K_{i}^{\square}$.

Suppose $K^{\uparrow}\subseteq K_{i}$, we have $(K^{\uparrow})^{\square}\subseteq K_{i}^{\square}$. Since $K^{\uparrow}$ is the supremal solution of the system $\Lambda$ and $(K^{\uparrow})^{\square}\subseteq K_{i}^{\square}$, we conclude that $(K^{\uparrow})^{\square}$ is a solution of the system $\Gamma(i)$. Thus, $(K^{\uparrow})^{\square}\subseteq X_{i}$. Consequently, we have $K^{\uparrow}\subseteq X_{i}$.

This finishes the proof of the claim that, for any $i\geq 0$, $K_{i}\supseteq K^{\uparrow}$ implies $K_{i+1}\supseteq K^{\uparrow}$. Now, since $K^{\uparrow}\subseteq E=K_{0}$, we conclude that $K_{i}\supseteq K^{\uparrow}$ for each $i\geq 0$.

We have $K_{l}=K_{l+1}=K_{l}\cap X_{l}$. Thus, we have $K_{l}\subseteq X_{l}$. We recall that $X_{l}$ is the supremal solution of the system $\Gamma(l)$ of equations

where $X\subseteq K_{l}^{\square}$, which is computed with the iteration

with $L_{0}=K_{l}^{\square}$. Since the computation terminates, there is some $m\geq 0$ such that $X_{l}=K_{l}^{\square(\circ_{1}\circ_{2}\ldots\circ_{n}\circ^{\prime})^{m}}$. Thus,

Let $T:=K_{l}^{\square\circ_{1}\circ_{2}\ldots\circ_{n}\circ^{\prime}}$. We have $T=T^{\circ^{\prime}}=M\backslash(M\backslash T)^{\square^{\prime}}$. Since $X=X^{\circ^{\prime}}=M\backslash(M\backslash X)^{\square^{\prime}}$ has an equivalent dual $X=X^{\square}$, we have $T=T^{\square}$. Thus, from $K_{l}\subseteq T$, we obtain $K_{l}^{\square}\subseteq T^{\square}=T=K_{l}^{\square\circ_{1}\circ_{2}\ldots\circ_{n}\circ^{\prime}}$. We then conclude that

where $K_{l}\subseteq E$. Thus, $K_{l}$ is a solution of the system $\Lambda$ and we have $K_{l}\subseteq K^{\uparrow}$. This, when combined with the fact that $K^{\uparrow}\subseteq K_{l}$, shows that $K_{l}=K^{\uparrow}$. This finishes the proof. $\blacksquare$

In general, consider the system $\Xi$ of equations

with $K\subseteq E$. Let $M_{i}\subseteq\Sigma^{*}$ be any given language and $\square_{i}:2^{M_{i}}\longrightarrow 2^{M_{i}}$ be a semi-topological closure operator (on $M_{i}$), for each $i\in[1,n]$. For each $i\in[1,n]$, let $\square_{i}^{\prime}$ be a semi-topological closure operator on some $M_{i}^{\prime}\subseteq\Sigma^{*}$ such that the equation $X=X^{\square_{i}^{\prime}}$ has an equivalent dual $X=M_{i}^{\prime}\backslash(M_{i}^{\prime}\backslash X)^{\square_{i}^{\prime\prime}}$ for some semi-topological closure operator $\square_{i}^{\prime\prime}$ on $M_{i}^{\prime}$. Here, $E^{\square_{i}^{\prime}}\subseteq M_{i}$ for each $i\in[1,n]$.

Remark: The system $\Xi$ is a straightforward generalization of the system $\Lambda$. In particular, if $\square_{1}^{\prime}=\square_{2}^{\prime}=\ldots=\square_{n}^{\prime}$, then the system $\Xi$ degenerates into the system $\Lambda$.

By an analysis which is similar to the proof of Proposition 2, the supremal solution $K^{\uparrow}$ of the system $\Xi$ exists. A strategy to solve the system $\Xi$ is to iteratively solve each equation, by using the technique developed in Section 3.3. This leads to a natural iteration scheme shown below.

Given any equation $K^{\square_{i}^{\prime}}=M_{i}\backslash(M_{i}\backslash K^{\square_{i}^{\prime}})^{\square_{i}},$ with $K\subseteq L$. The supremal solution exists and is denoted by $L^{\diamond_{i}}$ for convenience, which can be computed with the technique developed in Section 3.3. Then, the system $\Xi$ is solved with the following iteration scheme

$K_{j+1}=K_{j}^{\diamond_{1}\diamond_{2}\ldots\diamond_{n}}$,

with $K_{0}=E$. The correctness of the iteration scheme is shown below.

Proof: The descending chain

is obtained from the iteration scheme. We first show that $K_{i}\supseteq K^{\uparrow}$ for each $i\geq 0$.

To that end, we shall show that, for any $i\geq 0$, $K_{i}\supseteq K^{\uparrow}$ implies $K_{i+1}\supseteq K^{\uparrow}$. Indeed, suppose $K_{i}\supseteq K^{\uparrow}$. Then, $K^{\uparrow}$ is a solution of the system of equations

where $K\subseteq K_{i}$. In particular, we have $K^{\uparrow}$ is a solution of the equation $K^{\square_{1}^{\prime}}=M_{1}\backslash(M_{1}\backslash K^{\square_{1}^{\prime}})^{\square_{1}},$ with $K\subseteq K_{i}$. Thus, $K^{\uparrow}\subseteq K_{i}^{\diamond_{1}}$. It follows that $K^{\uparrow}$ is a solution of the equation $K^{\square_{2}^{\prime}}=M_{2}\backslash(M_{2}\backslash K^{\square_{2}^{\prime}})^{\square_{2}},$ with $K\subseteq K_{i}^{\diamond_{1}}$. We then have $K^{\uparrow}\subseteq K_{i}^{\diamond_{1}\diamond_{2}}$. The same reasoning shows that $K^{\uparrow}\subseteq K_{i}^{\diamond_{1}\diamond_{2}\ldots\diamond_{n}}=K_{i+1}$.

The claim that $K_{i}\supseteq K^{\uparrow}$ for each $i\geq 0$ then follows from $K^{\uparrow}\subseteq E=K_{0}$. Thus, $K_{l}\supseteq K^{\uparrow}$.

We have $K_{l}=K_{l+1}=K_{l}^{\diamond_{1}\diamond_{2}\ldots\diamond_{n}}\subseteq K_{l}^{\diamond_{i}}\subseteq K_{l}$, for each $i\in[1,n]$. Thus, we have $K_{l}=K_{l}^{\diamond_{i}}$, for each $i\in[1,n]$. Thus, $K_{l}$ is a solution of the system $\Xi$ and $K_{l}\subseteq K^{\uparrow}$. $\blacksquare$

In this subsection, we present some example properties which can be specified with a topologized equation, including the properties of normality, $L$-closedness, prefix-closedness and trace-closedness. It thus follows that the supremal sublanguages for these properties can be expressed with the same formula given in Section 3.1.