TP5: Linear Temporal Logic

Exercise 1. LTL semantics on a given trace

The diagram below describe a maximal execution (an infinite trace) that “loops” after the fifth state. The set of state properties of the first 5 states are, respectively, {q},{q},{q},{p} and ∅.

The table below has one LTL formula in each lines. For every formula, fill the table with the truth-value of the formula at the given index in the trace.

Exercise 2. A derived operator to reason about the past

We say that 𝜙 precedes 𝜓 holds for 𝑤, at 𝑘 (written $𝑤, 𝑘 \models \phi ,𝑃, \psi$) when:

$$\forall j \geq k . (w, j \models \psi) \Rightarrow \exists i \in [k, j].(w, i \models \phi)$$

That is, $𝑤 \models \phi,P,\psi$ as soon as:

$$\forall j. (w, j \models \psi) \Rightarrow \exists i \leq j. (w,i \models \phi)$$

Can you express this new modality in LTL or should we add it to the logic?

Exercise 3. Additional specification for a model with shared resources

We consider a parameterized system such as the Token Ring, with K “workers” that want to access a private resource in mutual exclusion. Each worker can be in any of the three states: $idle_i$ (do nothing); $wait_i$ (want to work but wait for access to the resource); or $work_i$(has access to the resource), where i∈1..K.

We can write the following requirement for this system, using an LTL formula and the “precede” connector studied in Exercise 2: “access to the critical section is allowed only to the workers that asked for it.” Meaning, before working, process i must have asked it.

Could you express the stronger requirement that: “access to the critical section is granted in the order where workers asked for it” ?

Try to find a LTL formula for this requirement.