AGV 6.2 -- Expressing Program Properties using LTL

Previous chapter: Linear-Time Temporal Logic (LTL)

This is a learning note of a course in CISPA, UdS. Taught by Bernd Finkbeiner

Introduction

In this section, we consider again our concurrent program $\small{\text{TURN}}$ introduced in section 1.1. As discussed before, a major property of interest is mutual exclusion,i.e., at any given point of time, at most one process is in the $\text{critical}$ region. We can express mutual exclusion, as well as other properties of turn, in LTL.

$\textbf{Example 1.1. }\small{\text{TURN}}:$
$$\text{local $t$: boolean where initially $t$ = $false$}\newline
P_0::\left[ \begin{array}{l}\text{loop forever do}\newline
\hspace{1cm}\left[ \begin{array}{l}
\ell_0: \text{await }\neg t; \newline
\ell_1: \text{critical;} \newline
\ell_2: t := true; \newline
\end{array} \right]\end{array} \right]
\mid\mid P_1::\left[ \begin{array}{l}
\text{loop forever do}\newline
\hspace{1cm}\left[ \begin{array}{l}
m_0: \text{await } t; \newline
m_1: \text{critical;} \newline
m_2: t := false; \newline
\end{array} \right]\end{array} \right]$$

Properties of the Concurrent Program $\small{\text{TURN}}$

Mutual exclusion : $\square\neg(\ell_1\wedge m_1)$

$\ell_{1}$ and $m_1$ cannot ($\neg$) be true at the same time ($\wedge$) at every point in time ($\square$)

The property can equivalently be formulated as $\neg(\textit{true}\ \mathcal{U}\ (\ell_1\wedge m_1))$, which means that the system remains true, until the a violation of mutual exclusion, i.e., $\ell_1\wedge m_1$, occurs

Finite waiting : $\square((\ell_0\rightarrow\Diamond\ell_1)\wedge(m_0\rightarrow\Diamond m_1))$

If ($\rightarrow$) $\ell_0$ is reached, eventually ($\Diamond$) it moves to $\ell_1$ and so as $m_0$ and $m_1$, this happens forever ($\square$)

In other words, each process only waits a finite amount of time (in locations $\ell_0$ and $m_0$, respectively) until it enters the $\text{critical}$ region (in locations $\ell_1$ and $m_1$, respectively):

This property is a Liveness conditions, usually involve infinite number of steps. Usually it is only meaningful when it is held under additional assumptions on the fairness of the scheduler.

Finite waiting under Fairness : $(\square\Diamond P_0\wedge\square\Diamond P_1)\rightarrow\square((\ell_0\rightarrow\Diamond\ell_1)\wedge(m_0\rightarrow\Diamond m_1))$

Finite waiting is required if both $P_0$ and $P_1$ will always happens (taking turns)

Let the atomic propositions $P_0$ and $P_1$ denote that the scheduler allows the respective process to advance in the current step. The subformula $\square\Diamond P_0$ states that process $P_0$ is scheduled infinitely often (always eventually). The finite waiting property is thus only required to hold if both processes are scheduled infinitely often.

Bounded overtaking : $\square(\ell_0\rightarrow(\neg m_1\ \mathcal{U}\ (m_1\ \mathcal{U}\ (\neg m_1\ \mathcal{U}\ \ell_1))))$

If $\ell_0$ is reached, it must leave the location $m_1$, and wait until $\ell_1$ is reached; when it leaves $\ell_1$, then it is allowed to move back to location $m_1$ again. This repeats infinitely.

In program $\small{\text{TURN}}$, the shared variable $t$ ensures that the processes take turns in entering their respective $\text{critical}$ regions. Bounded Overtaking refers to once process $P_0$ reaches location $\ell_0$, process $P_1$ can enter location $m_1$ at most once before Process $P_0$ enters location $\ell_1$.

This formulization of bounded overtaking requires that Process $P_1$ will eventually reach $\ell_1$. Sometimes we may also prefer a weaker requirement, where waiting forever is fine, as long as Process $P_1$ does not get to enter $m_1$ more than once in the meantime. We can simply change the operator into weak until$(\mathcal{W})$ to allow the processes to wait forever: $\square(\ell_0\rightarrow(\neg m_1\ \mathcal{W}\ (m_1\ \mathcal{W}\ (\neg m_1\ \mathcal{W}\ \ell_1))))$

Summary

In the next section, we will define the semantics of the logic for our automaton.

---

Next chapter: LTL and Counting Languages

Further Reading: Safety and liveness properties. Linear time property