A relation on states of labelled transition systems matching every transition with a transition of the same label in either direction, with successor states again related. In particular, transitions are matched individually, rather than silently skipped. For CSP processes this preserves CSP traces, CSP stable failures and CSP divergences.
New to topics? Read the docs here!