solidangle: Indeed, there are a lot of graph algebras out there, and I looked at many of them, including the Kleene Algebras. So far I haven't found any algebra with the decomposition axiom, but if you come across one, please let me know!

Why do I need the decomposition axiom? I haven't actually provided a motivation for it (or why I defined overlay and connect the way I did). So, here it is: just like LolWolf, I wanted to represent arbitrary graphs and only graphs using expressions, so expression x -> y -> z should be just a graph, and therefore I should be able to construct it from smaller pieces. But what should these pieces be? We can't make it equal to x -> y + y -> z because then our definition of -> would be partial, since it's not always possible to find 'the last node' (in this case y) that we need to connect to z (e.g. the left-hand side may be a cycle). The only choice that seems to work is to connect all vertices on the left-hand side to all vertices on the right hand side, which leads directly to the decomposition axiom.

Great, thanks!