# Is there a restriction of Linear Temporal Logic that has a “Markov” property?

I have a problem, that I can formulate as model-finding in Linear Temporal Logic (via Büchi automata). I also have the additional knowledge, that there is always satisfied a Markov-like property, specifically, for any pair of formulas $\phi, \psi$ whenever $\vdash F (\phi \implies X \psi)$ then also $\vdash G (\phi \implies X \psi)$. I think that this property could be somehow exploited to simplify or speed up the model finding process. Any ideas?