3 ms·
Shouldn’t it then be: next P : ●ー●ー○ ?
by dejj 5y ago
Shouldn’t it then be:
next P : ●ー●ー○
?
- deleted 5y ago[deleted]
- sriram_malhar 5y agoNo. 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.
- dejj 5y agoI can comprehend your interpretation of ‘next’; it is algebraic: For all states ‘i’: ‘next P’ is true for state ‘i’, if P is true for state ‘i+1’. The article seems to have a side-effect based interpretation rather than an algebraic one. It seems that ‘next P’ updates the state state of ‘P’. Hence the different diagram.