@@ -79,10 +79,7 @@ During my internship, under the supervision of \href{https://group-mmm.org/~ichi
The first part of the internship consisted in a bibliographical work whose aim was to get a better understanding of tools and results that could later be used to achieve our goals. The ones who ended up being at the base of this work are presented in this section.
It is assumed that the reader is already familiar with basic notions of order theory and category theory. In particular, the following notations are used :
\begin{itemize}
\item$\pi$ and $\pi'$ are the projections along the first and second components of a binary product.
\end{itemize}
It is assumed that the reader is already familiar with basic notions of order theory and category theory.
@@ -99,6 +96,8 @@ Let $F : \mathbb{B} \rightarrow \mathbb{B}$ be an endofunctor over a category $\
Intuitively, $X$ is a state space, $F$ a behavior type and $c$ a transition structure. An $F$-coalgbera is thus a transition system of the behavior type $F$.
\begin{example}
We use $\pi$ and $\pi'$ for the projections along the first and second components of a binary product.
A (non-labelled) Büchi automaton is a tuple $(X,c)$ where $X$ is the set of states and $c : X \rightarrow\mathcal{P}X$ (a coalgebra for the product of $2$ and the powerset functor $\mathcal{P} : \mathbf{Set}\rightarrow\mathbf{Set}$) is the transition function~: $(\pi' \circ c)(x)$ is the subset of states reachable from $x$ and $(\pi\circ c)^{-1}(1)$ is the set of accepting states.
Similarly, a (non-labelled) Markov chain is a tuple $(X,c)$ where $X$ is the set of states and $c : X \rightarrow2\times\mathcal{D}_{\le1}X$ (a coalgebra for the product of $2$ and the subdistribution functor $\mathcal{D}_{\le1} : \mathbf{Set}\rightarrow\mathbf{Set}$) is the transition function~: $(\pi' \circ c)(x)(y)$ is the probability of reaching $y$ from $x$ and $(\pi\circ c)^{-1}(1)$ is the set of accepting states.
...
...
@@ -160,10 +159,10 @@ Let $F : \mathbf{Set} \rightarrow \mathbf{Set}$ be an endofunctor and $\Omega$ b
Similarly, take $F =\mathcal{P}(\mathrm{AP})\times\mathcal{D}_{\le1}(-)$, $\Omega=[0,1]$ (with $x \sqsubseteq y \iff x \ge y$), $\Gamma=\{\bot, \top, {\min},{\max}\}$ with the usual interpretations and $\Lambda=\mathrm{AP}\cup\{{\lozenge}\}$ with