<p>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.</p>

CC BY-SA 3.0
2016-01-28T15:26:51.240Z
2016-01-28T15:26:51.240Z
Shaull
<p>In propositional linear temporal logic (LTL) over $\mathbb{N}$, it is decidable whether a formula $\varphi$ is satisfiable from time point 0. </p>

<p>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}$</p>

<decidability><temporal-logic><linear-temporal-logic>
Global satisfiability in LTL
Tyler Durden
# Global satisfiability in LTL

(Asked by: username_0 on 2016-01-28)

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}$

**Tags:** decidability, temporal-logic, linear-temporal-logic


---

## 1 answers

### Answer by username_1 on 2016-01-28. Score: 2 | Accepted answer

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.


---

