0.5 Using temporal logic to specify properties  (Page 4/11)

Strong Until

${}_i(U)$ iff $k\ge i\text{.}({}_{k}j\text{.}(ij<k{}_j))$ .

Any logic that includes temporal connectives is a temporal logic . More specifically, this is Linear Temporal Logic ( LTL ). The ``linear'' part of this name means thatwe are looking only at individual traces, rather than making formulas that discussall possible traces of a program. After all, a single program can result in many possible traces.An LTL formula does not allow us to say, for example, that a property holds in all possible executions of the program.However, SPIN overcomes some limitations by essentially testing an LTL formula against all possible traces.Will will return to SPIN in the next section .

In summary, the syntax used in SPIN is given by the following grammar.

Do we really need a whole new logic?

We could use regular ol' first-order logic as our formal language for specifying temporal properties.We'd do this by adding an explicit time index to each proposition in $\mathrm{Prop}$ , turning it into a unary relation.For example, instead of considering $\mathrm{Philosopher\_B\_has\_fork}$ in state 17, we'd instead write $\mathrm{Philosopher\_B\_has\_fork}\left(17\right)$ , and so on.

This approach, though, quickly becomes cumbersome. Consider the everyday concept ``Someday, X will happen''.We have to go through some contortions to shoehorn this concept into first-order logic:``There exists a day $d$ , such that $d$ is today or later, and X will happen on $d$ ''. Quite a mouthful forwhat is about the simplest temporal concept possible!