 Formally, a tree (or branching time structure) is a temporal frame \(\mathcal{T} = \left\langle T, \prec \right\rangle\) where the temporal precedence relation \(\prec\) is a backward-linear partial ordering on the set of time instants \(T\) which is such that any two instants have a common \(\prec\)-predecessor in \(T\). That is, every time instant in a tree has a linearly ordered set of \(\prec\)-predecessors, and any two instants share some common past. The former condition rules out backward-branching, while the latter ensures ‘historical connectedness’. In the philosophical literature, the temporal precedence relation \(\prec\) is commonly assumed to be irreflexive, i.e. a strict partial order, whereas in computer science, usually reflexive structures are studied.