Page "Simulation preorder" Paragraph 10

Given two states p and q in S, q simulates p, written p ≤ q if there is a simulation R such that ( p, q ) ∈ R. The relation ≤ is a preorder, and is usually called the simulation preorder.

It is the largest simulation relation over a given transition system.