In mathematics, especially order theory, a prefix ordered set generalizes the intuitive concept of a tree by introducing the possibility of continuous progress and continuous branching.
In this case, the elements of the set are usually referred to as executions of the system.
A prefix order is a binary relation "≤" over a set P which is antisymmetric, transitive, reflexive, and downward total, i.e., for all a, b, and c in P, we have that: While between partial orders it is usual to consider order-preserving functions, the most important type of functions between prefix orders are so-called history preserving functions.
Furthermore, functions that are history and future preserving surjections capture the notion of bisimulation between systems, and thus the intuition that a given refinement is correct with respect to a specification.
Instead, it leads to an arbitrary interleaving of the original prefix orders.