Another popular approach to specifying concurrent systems involves the use of behavior equivalences and preorders to relate specifications and implementations. In this framework, which has been extensively explored by researchers in process algebra, specifications and implementations are given in the same notation; the former describes the desired high-level behavior, while the latter provides lower-level details indicating how this behavior is to be achieved. In equivalence-based methodologies, proving an implementation correct amounts to establishing that it behaves ``the same as'' its specification; in those based on preorders, one instead shows that the implementation provides ``at least'' the behavior dictated by the specification.
In support of this approach, a number of different equivalences and preorders have been proposed based on what aspects of system behavior should be observable. Relations may be classified on the basis of the degree to which they abstract away from internal details (viz. the intensional/extensional dichotomy) of system descriptions; the amount of sensitivity they display to choices systems make during their execution (viz. the linear/branching time dichotomy); and the stance they adopt with respect to interleaving vs. true concurrency.
These relations also serve to bridge the gap between intensional and extensional models of concurrency described above. That is, in order to define a relation over intensional models, one first selects the extensional, or ``observable'', information that processes may exhibit and then uses this as the basis for relating models.