Quantified temporal logics have the Barcan formulas and its converses for both G (it will always be the case that) and H (it has always been the case that), so that both $\forall x G \alpha \rightarrow G \forall x \alpha$/$G \forall x \alpha \rightarrow \forall x G \alpha$ and $\forall x H \alpha \rightarrow H \forall x \alpha$/$H \forall x \alpha \rightarrow \forall x H \alpha$ are theorems.
Are there known completeness results for quantified temporal logics extending or as strong as the one for lattices with axioms $G \alpha \rightarrow F \alpha$/$H \alpha \rightarrow P \alpha$ and $G \alpha \rightarrow GG \alpha$/$H \alpha \rightarrow HH \alpha$ and $FG \alpha \rightarrow GF \alpha$/$PH \alpha \rightarrow HP \alpha$?
