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

The awkwardness stems from the fact that in English, ``eventually'', ``always'',and ``until'' are primitives. When we design a formal language to capture with these concepts,shouldn't we too include them as primitives? Having our formal representations reflect ournatural conceptions of problems is the first law of programming!

This is why we have decided to incur the overhead of defining a new language, LTL.Still, you have noticed that the semantics we've given are phrased in terms of `` $i\text{.}$ ''. From a language designer's perspective, we might say thatLTL is a high-level language, and we give an interpreter for it written in first-order logic(over the domain of trace-indices).

Translating between english and ltl: examples

Let's look at how to turn a natural-English specification intotemporal logic, and vice versa.

How might we express the common client/server relationship ``if there is a request ( $r$ ), then it will be serviced ( $s$ )''?

Hmm, that seems obvious: $(rs)$ should do it, no? Alas, no. The problem is, the truth of thisformulawhich has no temporal connectives at allonly depends upon the trace's initial state, ${}_0$ in this case, whether ${}_0(rs)$ . This certainly doesn't match our intent, sincewe want the request and service to be able to happen at points in the future.Let's try again

After more thought, we can get something which does arguably match our intent: $\square (r◇s)$ . ``Whenever a request is made, a servicing willeventually happen.''

However, even this may not be what everybody wants. Some considerations:

• Even if $r$ is raised (and lowered) several times, a single moment of $s$ can satisfy the entire trace. This matches an intuition of $r$ indicating a single ring of a telephone (and $s$ being `pick up the phone'), but may not match the intuitionof $r$ being ``leave a voicemail'' (and $s$ being ``respond to a voicemail'').

• A trace in which $s$ is always true (regardless of $r$ ) certainly satisfies $$ . Did you expect the English statement to encompass this?
• Any trace in which requests are serviced instantaneously will satisfy $$ . While this might be intended, it might alsobe a bug of leftover servicings from previous requests.

• A trace in which a request is never made still satisfies this formula.While that is probably what is intended, it may not have occurred to you from the English statementalone.