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 waitingis 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
Please cite the source for reprints, feel free to verify the sources cited in the article, and point out any errors or lack of clarity of expression. You can comment in the comments section below or email to GreenMeeple@yahoo.com