A directed graph is a pair G=(V,E)G=(V,E) with EV×VE\subseteq V\times V. An (u,v)(u,v), written uvu\to v, has source uu and target vv. This convention allows loops and allows both uvu\to v and vuv\to u; additional hypotheses can exclude them. There are no parallel copies of an edge when EE is a set.

Paths

follow successive arrows; a returns to its starting vertex. Edge orientation must be stated when the graph describes dependencies: “requires” and “is used by” give opposite conventions.