The three models that are studied in this project are called interleaving models. In this section we present the three models and how these are represented as a category. Furthermore we will develop some intuition of the models by examples. These examples are used later when we construct functors and develop adjoints between the different categories of these models.
A labeled transition system is a structure $$ TS = (S_{TS},S^{I}_{TS},L,Tran_{TS}) $$ where
Given two transition system, $TS_0$ and $TS_1$, an arrow $h : TS_0 \rightarrow TS_1$ is a pair $(\sigma,\lambda)$, where $\sigma : S_{TS_0} \rightarrow S_{TS_1}$ is a function, and $\lambda : L_{TS_0} \rightharpoonup L_{TS_1}$ a partial function, such that:
We define the category $\textbf{TS}$ of labeled transition systems with $TS_0 , TS_1 , \dots$ as objects and the pair $(\sigma,\lambda)$ as arrows.
A synchronization tree is an acyclic, reachable transition system $ST$ such that $$ (s',a,s),(s'',b,s) \in Trans_{ST} \Rightarrow s' = s'' \land a = b $$ That is we have no two different incoming paths to any node. We denote the category of synchronization trees $\textbf{ST}$ as a subcategory of $\textbf{TS}$.
Let us develop some intuition behind the categories $\textbf{TS}$ and $\textbf{ST}$. Say we have the $TS$ as seen in Figure 2. Name this $TS_1$. Regarded as a finite automaton where all states are accepting, this transition system defines the same language as the regular expression $$ (ab)^{*}(a|aa|\epsilon) $$ We can translate $TS_1$ into the $ST$ seen in Figure 3. Name this $ST_1$. $ST_1$ is infinite in size since the language of the corresponding $TS_1$ is infinite. However $TS_1$ is not infinite in size since transition systems are allowed to contain cycles.
We have that $L_{ST_1} = \{a,b\}$. We have that $s_{ST_1}^I = \{S_0\}$. We have that $S_{ST_1} = \{S_0,S_1, \dots \}$. And we have that $Trans_{ST_1} = \{ (S_0,a,S_1),(S_0,a,S_3), \dots \}$.
The tree in Figure 3 is one possible tree. We have an arrow $\eta_{ST} = (\sigma,\lambda)$ in $\textbf{ST}$ that translates $ST_1$ into the tree found in Figure 4. Name this $ST_2$. $\eta_{ST}$ is given as $$ \sigma(s_i) = \{ \alpha | s_0 \xrightarrow{a_0} s_1 \xrightarrow{a_1} \cdots \xrightarrow{a_{i - 1}} s_i \land \alpha = a_0 \cdots a_{i - 1} \} $$ That is for each state $s_i \in ST_1$ we translate into a path up till $s_i$. So state $s_i$ after translation is named $$ a_0 \cdots a_{i - 1} $$ For $\eta_{ST}$ we have that $$ \lambda = id $$ since the same set of labels is used.
Note that we do not have an arrow in $\textbf{ST}$ from $ST_2$ to $ST_1$. When constructing each new state, $s_{\alpha}$, two adjacent paths that comes from the same parent node and have the same label, are collapsed into one path. We can't use (2) of the definition of arrows in $TS$ to split the state $s_{\alpha}$ into two states. We call the tree of $ST_2$ the canonical form. Later when we discuss adjunctions, we will return to this canonical form.
The tree as seen in Figure 5 can be constructed using $ST_1$ with the same translation used to construct $ST_2$, but with $\lambda$ given as $$ \lambda = [a \mapsto a,b \mapsto c] $$ Name this tree $ST_3$.
A Hoare language is a pair $HL = (H_{HL},L_{HL})$, here $H_{HL}$ is the set of all strings that can be created within the language, and $L_{HL}$ is the alphabet. A Hoar language satisfies the following two properties
A partial map $\lambda : HL_0 \rightharpoonup HL_1$ is a morphism of Hoare languages from $(H_{HL_0},L_{HL_0})$ to $(H_{HL_1},L_{HL_1})$ if for each $s \in H_{HL_0}$ we have $\hat{\lambda}(s) \in H_{HL_1}$, where $\hat{\lambda} : L_{HL_0}^{*} \rightarrow L_{HL_1}^{*}$ is given as
This gives rise to the categori $\textbf{HL}$ of Hoare languages, with $(H,L)$ pairs as objects, and $\lambda$'s as arrows.
Again we can develop some intuition. Say we have $HL_1$. Here we define $$ L_{HL_1} = \{ a,b \} $$ So we have that $L_{HL_1}^{*}$ is every possible finite combination of series of the symbols $a$ and $b$. We let $H_{HL_1}$ match the language of $TS_1$. That is every possible string we can form with $TS_1$. We have that property $ii$ is satisfied, since we can stop in each state in a TS, that is we only travel one symbol at a time. So say we are in state $s_i$ of $S_{TS_1}$. This forms the string $$ \epsilon \cdot a_0 \cdot a_1 \cdots a_{i - 1} \in H_{HL_1} $$ We can do this recursively until the string $\epsilon$ is reached. This corresponds to how we have defined $\sigma$ in arrows of $\textbf{ST}$: the parent of state $s_i$ is named $$ \epsilon \cdot a_0 \cdots a_{i - 2} $$ We create $HL_2$ in the exact same manner, but with $$ L_{HL_2} = \{a,c\} $$ We have an arrow between $HL_1$ and $HL_2$. That is $\lambda_{HL}$ for which $$ \lambda_{HL} = [a \mapsto a,b \mapsto c] $$ Substituting symbols is exactly what $\lambda$ recursively does.