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

However it doesn't make sense a priori to ask whether an entire trace satisfies some particular state formula;unlike regular propositional logic, the truth of state formulas changes over time, as the trace $$ progresses.

Introducing temporal connectives

So, how do we talk about formulas holding (or not) over time?In addition to making formulas out of $$ , $$ , $$ and propositions from the set $\mathrm{Prop}$ , we'll allow the use of temporal connectives .

• $\square$ always , or henceforth : We say that $\square$ is true at a moment $i$ , iff $$ is true from moment $i$ onwards.
• $◇$ eventually : We say that $◇$ is true at moment $i$ , iff $$ will eventually be true at moment $i$ or later.
• $U$ strong until : We say that $(U)$ is true at moment $i$ , iff $$ eventually becomes true, and until then $$ is true.
• $W$ weak until : Like Strong Until, but without the requirementthat $$ eventually becomes true.

As a mnemonic for the symbols `` $\square$ '' and `` $◇$ '', we can imagine a square block of wood sitting on a table.Orienting it like $\square$ , it will always sit there; orienting it like $◇$ , it will eventually teeter.

More formally, we define these connectives as follows.

Always

${}_i\square$ iff $ji\text{.}{}_j$

Eventually

${}_i◇$ iff $ki\text{.}{}_k$

Before continuing on with our two other connectives (strong- and weak-until),let's pull back a bit and look at our notation.