I have a question as follows:
A temporal frame $(T,\prec)$ is reflexive if $\prec$ is reflexive.
Write down a temporal formula that is valid on all reflexive frames, but invalid on any other frames.
Should my answer be in this form of
a) $∀x(x\prec)$ or
b) $(GPx\rightarrow x)$ or $(HFx\rightarrow x)$?
For temporal logic, there are two main characterisations of time: Instant-based and interval-based.
In instant-based characterisation, the domain of discourse is a set of time instants (points in time) $T$ and a binary relation of temporal precedence $\prec$ on them. Hence a temporal frame can be represented as:
$$\mathcal{T}=\langle T,\prec\rangle$$
In interval-based characterisation, the domain of discourse is a set of time intervals. A typical structure contains the relations of temporal precedence $\prec$, inclusion $\sqsubseteq$, overlap $O$ on a set of time intervals $T$. Thus, the temporal frame can be represented as:
$$\mathcal{T}=\langle T,\prec,\sqsubseteq, O⟩$$
The standard semantics for the minimal temporal logic $\mathbf{K}_{t}$ is Kripke-style instant-based, interpreting possible worlds as time instants, and the accessibility relation as temporal precedence.
If the precedence relation is defined reflexive, then the sentence $\forall x(x\prec x)$ expresses the first-order property of the model over which the $\mathbf{K}_{t}$- formulas are evaluated. In case that the precedence relation is defined irreflexive, then $\forall x\neg(x\prec x)$ holds. Notice that these sentences are not in the language of $\mathbf{K}_{t}$.
By basic modal logic, we know that, for a proposition $p$, $\Box p\rightarrow p$ holds if and only if the accessibility relation is reflexive. Analogously, using the strong temporal operators $\mathrm{G}$ or $\mathrm{H}$, we can state that for a model $\mathfrak{T}$ of a reflexive frame
$$\forall x(x\prec x)\iff\mathfrak{T}\vDash Gp\rightarrow p$$ or $$\forall x(x\prec x)\iff\mathfrak{T}\vDash Hp\rightarrow p$$
Alternatively, using their weak duals
$$\forall x(x\prec x)\iff\mathfrak{T}\vDash p\rightarrow Fp$$ or $$\forall x(x\prec x)\iff\mathfrak{T}\vDash p\rightarrow Pp$$
for the class of reflexive frames. $ Gp\rightarrow p$ and the others on the right-hand side are the formulas sought for in the language of $\mathbf{K}_{t}$.
As a side note, a more challenging question would be to write a formula valid only on irreflexive frames. For, it is known by Lemmon’s completeness proof for $\mathbf{K}_{t}$ that any consistent set of $\mathbf{K}_{t}$-formulas is satisfiable in a model of an irreflexive frame. A method to circumvent this difficulty is to add a derived rule called Gabbay rule:
$$\mathrm{H}p\wedge\neg p, \phi\vdash\phi$$ where $p$ is an atomic proposition that does not occur in $\phi$ (mutatis mutandis for the other temporal operators).