pathterminuspages/projects/aboutcontactabout me

Adjoint Between Transition Systems and Synchronization Trees



Adjoint Between Transition Systems and Hoare Languages
@Adjoint Between Transition Systems and Synchronization Trees

We now turn our focus to the adjoint that arises between TS and ST. Since ST is a subcategory of TS, that is $ST \in \textbf{ST} \Rightarrow ST \in \textbf{TS}$, we have have for now that the functor $ST2TS$ is the function that just leaves the input as is.

We now turn our attention to $TS2ST$. Given $$ TS_1 = (S_{TS_1},s^{I}_{TS_1},Tran_{TS_1},L_{TS_1}) $$ we can construct the functor using $HL2ST$ by adding a $TS2HL$. However using this method on $TS_1$ will result in $ST_2$ from which we can't get back to $TS_1$. We simply have lost the information about the cyclic transitions in the original structure.

Another approach is to construct $TS2ST$ by naming each state of the resulting $ST$ with the string formed by concatenation of each of the names of the subsequent states. This will ensure that we store enough information to obtain any given $TS$ mapped through $ST2TS \circ TS2ST$. We get $$ TS2ST(TS_1) = (S'_{TS_1},s^{I}_{TS_1},Tran'_{TS_1},L_{TS_1}) $$ where $$ S'_{TS_1} = \{ s_0 s_1 \cdots s_i | \exists s_i \in S_{TS_1} : s_0 \xrightarrow{a_0} \cdots \xrightarrow{a_{i - 1}} s_i \} $$ and $$ Tran'_{TS_1} = \{ (\bar{s}s,a,\bar{s}ss') | \bar{s}s,\bar{s}ss' \in S'_{TS_1}, s \xrightarrow{a} s' \in Tran_{TS_1} \} $$ Given $TS_1$ from Figure1 in the last article, we obtain $TS2ST(TS_1)$ as shown in Figure6. Name this $ST_4$.

Figure6 : Tree $ST_4$ obtained from $TS2ST(TS_1)$.

We can adjust the functor $ST2TS$ a bit. If we map down from the last char of the name of the state of a given $ST$, we obtain the original $TS$ with possible cycles. That is $$ ST2TS(ST_1) = (S'_{ST_1},s^{I}_{ST_1},Tran'_{ST_1},L_{ST_1}) $$ where $$ S'_{ST_1} = \{ s' | \bar{s} s' \in S_{ST_1} \} $$ with the possibility that $\bar{s} = \epsilon \lor s' = \epsilon$, and $$ Tran'_{ST_1} = \{ (s,a,s') | s,s' \in S'_{ST_1},\bar{s}s \xrightarrow{a} \bar{s}ss' \in Tran_{ST_1} \} $$ Now we have that $ST2TS(TS2ST(TS_1)) = TS_1$. Or in general that $$ ST2TS \circ TS2ST = id_{TS} $$ In general this does not hold the other way around. That is there exists a $ST_i$ such that $$ TS2ST \circ ST2TS \neq id_{ST} $$ As an example of why this fails observe the following, we have that $$ ST2TS(ST_2) = TS_{ST_2} $$ that is the exact same tree, but regarded as a TS. Now we have that $$ TS2ST(TS_{ST_2}) = ST_4 $$ and that $$ ST_4 \neq ST_2 $$

Constructing the Adjoint

The above functor gives rise to the natural transformation $$ \eta_{TS_1} : id(TS_1) \rightarrow ST2TS(TS2ST(TS_1)) $$ The diagram of a natural transformation, as given in Figure5 for $HL2ST \circ ST2HL$, commutes for $\eta_{TS_i}$, since any given arrow, $h' \in \textbf{TS}$, is mapped to itself. That is $$ h' = ST2TS(TS2ST(h')) $$ Finally we get the adjoint shown in Figure7.

Figure7 : The adjoint formed by the functors $TS2ST$ and $ST2TS$.

$ST2TS$ is the right adjoint of $TS2ST$ and vice versa.

CommentsGuest Name:Comment: