Partial order reductions are a family of techniques for diminishing the statespace explosion problem for model-checking concurrent programs. They are based on the Observation that execution sequences of a concurrent program can be grouped together into equivalence classes that are indistinguishable by the property to be checked. Applying the reduction to a description of a program results in a reduced state-space that generates at least one representative for each equivalence class. When moving to branching models, e.g., as in branching temporal logics or process algebras, the execution sequences are grouped together into a Single tree. In this case, the reduction must also be sensitive to preserving the branching points, where executions with a common prefix depart from each other.