= \mathcal{M}_n^{V_G}$. For every graph morphism $\varphi \colon G \to H$ and $a \in \mathcal{S}^n(G)$, we have $\mathcal{S}^n_{\varphi}(a) \in \mathcal{M}_n^{V_{H}}$ with: $$\mathcal{S}^n_{\varphi}(a)(w) = \bigvee\limits_{\varphi(v)=w}^{}
      a(v), \quad \textit{where } v \in V_G \textit{ and }
      w \in V_{H}.$$ For a graph $G$, its *standard annotation* $s_G \in \mathcal{S}^n(G)$ is defined as the function which maps every node of $G$ to its out-degree (or $*$ if the out-degree is larger than $n$).

Finally, we consider annotations based on the path monoid (see Ex. \[ex:path-monoid\]).

\[ex:path-annot\] We define the functor $\mathcal{T}\colon\GR \to \Mon$ as follows: For every graph $G$, $\mathcal{T}(G) = \mathcal{P}_G$. For every graph morphism $\varphi \colon G \to H$ and $P \in \mathcal{T}(G)$, we have $\mathcal{T}_{\varphi}(P) \in \mathcal{P}_{H}$ with: $$\mathcal{T}_{\varphi}(P) = \{(\phi(v),\phi(w))\mid (v,w)\in
    P\}.$$ For a graph $G$, its *standard annotation* $s_G \in \mathcal{T}(G)$ is the transitive closure of the edge relation, i.e., $s_G = E_G^+$.

In the following we will consider only annotations satisfying certain properties in order to achieve soundness and completeness.

\[def:prop-annotations\] Let $\mathcal{A}:\C \to \Mon$ be an annotation functor, together with standard annotations. In this setting we say that

-   the *homomorphism property* holds if whenever $\phi$ is a mono, then $\mathcal{A}_\phi$ is a monoid homomorphism, preserving 