Adjoint Between Transition Systems and Synchronization Trees

26.08.2020

Contents/Index

Introduction
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$.

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$$

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.
$ST2TS$ is the right adjoint of $TS2ST$ and vice versa.