More graph excitement, for your viewing pleasure.
Given two graphs G1 = (V1, E1) and G2 = (V2, E2), and a binary relation R, R is a simulation if for every vertex in V1 and V2 and every edge in E1, if there is a mapping between two vertices (x1 and x2) (that is, an entry in R), and an edge from the vertex in V1 - x1 - to another vertex in V1 - y1 - then there is a mapping from that second vertex - y1 - to a vertex in V2 - call it y2, and an edge between the vertices x2 and y2. You can make your simulation more strict by labelling the edges, and requiring that the edges in each graph that are 'equivalent' be of the same label.
Perhaps a picture would help. Let's say you've got three 'points'. You've got an edge from x1 to y1, and a mapping from x1 to x2:
X1------->X2
|
|
\/
Y1
If that's the case, then there must be some point y2 that makes the picture look like this:
X1------->X2
| |
| |
\/ \/
Y1------->Y2
One use of this sort of thing - relations, simulations, graphs - is typing semistructured data. The above writeup breathes its full force in this case - the tighter the typing you make, the more complex is the model you end up with. The less strict, the less closely your model resembles the original system, and potentially the less useful the model is.