# Global satisfiability in LTL

In propositional linear temporal logic (LTL) over $\mathbb{N}$, it is decidable whether a formula $\varphi$ is satisfiable from time point 0.

Is it known to be un/decidable to check the satisfiability of a formula over all time points? For example, given a formula $\varphi$ and a model $M$, can we check whether $\langle M,i\rangle \models \varphi$ for all $i \in \mathbb{N}$

The statement $\langle M,i\rangle\models \varphi$ for all $i\in \mathbb{N}$ is equivalent to $\langle M,0\rangle\models G\varphi$. Thus, you can check the latter.