 A tense-logical model (TIME,\(\le\),C,\(\TRUE\)) based on a branching time system is a structure, where (TIME,\(\le)\) is a partially ordered set of moments of time, and C is a set of so-called histories or chronicles i.e., maximally ordered linear subsets in (TIME,\(\le)\). It is standard procedure how to define “=” and “\(\lt\)” in terms of “\(\le\)”. The before/after relation, \(\lt\), is supposed to be irreflexive, asymmetric, transitive and backwards linear. Backwards linearity means “no backwards branching” i.e.