= 0$ if $a \le b$. Furthermore $*-a = *$ for all $a\in \mathbb{N}$. It is easy to see that subtraction is well-behaved.

Given a set $S$ and an ordered monoid (with subtraction) $\mathcal{M}$, it is easy to check that also $\mathcal{M}^S$ is an ordered monoid (with subtraction), where the elements are functions from $S$ to $\mathcal{M}$ and the partial order, the monoidal operation and the subtraction are taken pointwise.

The following path monoid is useful if we want to annotate a graph with information over which paths are present. Note that due to the caused by the abstraction, a path in the abstract graph does not necessarily imply the existence of a corresponding path in a concrete graph. Hence annotations based on such a monoid can yield useful additional information.

\[ex:path-monoid\] Given a graph $G$, we denote by $E_G^+\subseteq V_G\times V_G$ the transitive closure of the edge relation $E^{\to}_G = 
  \{(\sSrc_G(e),\sTgt_G(e)) \mid e \in E_G\}$. The *path monoid* $\mathcal{P}_G$ of $G$ has the carrier set $\mathcal{P}(E_G^+)$. The partial order is simply inclusion and the monoid operation is defined as follows: given $P_0,P_1\in \mathcal{P}_G$, we have $$\begin{aligned}
    P_0+P_1 & = & \{(v_0,v_n)\mid \exists v_1,\dots,v_{n-1} \colon
    (v_i,v_{i+1})\in P_{j_i}, \\ & & 