No. It should be: 1 2 3 P ● ● ○ (next P) ● ○ ○ All formulae share the same timeline in terms of state numbering. In no

No. It should be: 1 2 3 P ● ● ○ (next P) ● ○ ○ All formulae share the same timeline in terms of state numbering. In non-temporal logic, all operators operate on the values at a single time. So, when we say "P and Q", or "not P", these implicitly all apply to some state i. Temporal logic adds "next", which links a state i to the state i+1. (next P) in state i refers to the value of P in state (i+1). (always P) refers to states (i ... inf). In this example, the value of (next P) in state 2 must be false, because it refers to P's value in state 3.