 The temporal operators are essentially interpreted as they are in linear temporal logic: the instant of evaluation is simply shifted backwards and forwards on the given history. Note that the requirement “\(t'\in h\)” is redundant in the semantic clause for the past operator \(P\) as there is no backward branching. It is crucial, however, in the clause for the future operator \(F\). As usual, the strong temporal operators \(H\) and \(G\) are defined as the duals of \(P\) and \(F\), respectively. The modal operators quantify over the set of histories passing through the current instant. The operator \(\Diamond\) is an existential quantifier over that set and captures possibility, while its dual \(\Box\) involves universal quantification and expresses ‘inevitability’ or ‘historical necessity’.