$\def\nec{\Box}
\def\pos{\Diamond}
\def\U{{\cal U}}
\def\W{{\cal W}}
\def\R{{\cal R}}
\def\B{{\cal B}}
\def\X{\bigcirc}
$
Exercise 1 (from 14/1/2022). In each cycle, a process X can be in the ready queue ($\color{blue}r$) or
performing some input/output ($\color{blue}{io}$) operation. Additionally, the CPU
can be busy ($\color{blue}{b}$) executing some process or it can be empty ($\color{blue}{\neg
b}$). Formulate the following sentences in LTL
If the CPU is empty and X is not ready then X is performing
input/output
$\color{blue}{\nec (\neg b \wedge \neg r \to io)}$
If process X is ready, the CPU must be busy in the next cycle
$\color{blue}{\nec (r \to \X b)}$
Process X does not suffer from starvation, that is, when it is
in the ready queue, it will eventually leave it
$\color{blue}{\nec (r \to \pos \neg r)}$ which is
equivalent to $\color{blue}{\nec \pos \neg r}$
Process X never gets permanently blocked doing input/output
$\color{blue}{\neg \pos \nec io}$ which is
equivalent to $\color{blue}{\nec \pos \neg io}$
Between each two different periods of input/output, process X
always passes through the ready queue
$\color{blue}{\nec \neg (io \wedge \X \neg
io \wedge \X (\neg r \ \U \ io))}$ which is
equivalent to $\color{blue}{\nec (io \wedge \X \neg io \to \X (r \ \R
\ \neg io))}$
Exercise 2 (from 5/7/2021). A chronometer has a start/stop
button ($\color{blue}b$). The watch can be stopped
($\color{blue}{s}$) or running ($\color{blue}{\neg
s}$). Besides, the time can be at zero 00:00:00 ($\color{blue}{z}$) or not. Formulate the following sentences in LTL
When we push the button, if it was stopped, it starts
running and vice versa, unless we keep it pushed in the next moment
$\color{blue}{\nec (b \wedge \X \neg b \to (p
\leftrightarrow \X \neg p))}$. This is equivalent to
$\color{blue}{\nec (b \wedge \X \neg b \wedge p \to \X \neg p) \wedge
\nec (b \wedge \X \neg b \wedge \neg p \to \X p)}$
If we keep the button pushed two consecutive situations, the
watch stops and resets to zero immediately after
$\color{blue}{\nec (b \wedge \X b \to \X
\X (s \wedge z))}$
If the button is not pushed, the watch does not change its state (stopped/running)
$\color{blue}{\nec (\neg b \to (s
\leftrightarrow \X s)}$
The watch is set to zero an infinite number of times
$\color{blue}{\nec \pos z}$
We never push the button indefinitely
$\color{blue}{\nec \neg \nec b}$ or, if
preferred, $\color{blue}{\neg \pos \nec b}$ or equivalently $\color{blue}{\nec \pos \neg b}$
Exercise 3 (from 7/6/2021). The fire alarm can start
ringing ($\color{blue}r$) when a sensor detects smoke ($\color{blue}s$) or when it is activated manually
($\color{blue}m$), for instance, for an evacuation drill. Formulate the following sentences in LTL
If smoke is detected, the alarm will start ringing at some moment
$\color{blue}{\nec (s \to \pos r)}$
If it is activated manually, it starts ringing immediately after
$\color{blue}{\nec (m \to \X r)}$
When the alarm is ringing, it stops doing so after a while
A direct reading gives us
$\color{blue}{\nec (r \to \pos \neg r)}$, but this is equivalent
to $\color{blue}{\nec \pos \neg r}$ or $\color{blue}{\neg \pos
\nec r}$ (it never starts ringing forever)
You can always activate the alarm manually as much as you want
$\color{blue}{\nec \pos m}$
It cannot start ringing without detecting smoke before,
unless it was activated manually
$\color{blue}{\neg ((\neg s \wedge \neg m)
\ \U \ r)}$ which is equivalent to $\color{blue}{(s \vee m)\ \R \ \neg r}$ (before each ring, there is smoke or manual activation)
Exercise 4 (from 19/1/2021). A COVID-19 monitoring center
is making a weekly control on several sample patients. During the
last week, the patient may have been confined ($\color{blue}c$)
and/or have had symptoms ($\color{blue}s$) compatible with
COVID-19. Assuming that each transition represents the last week
passed after the previous control, formulate the following sentences in LTL
If the patient had symptoms, she must be confined the next
two weeks
$\color{blue}{\nec (s \to \X c \wedge \X
\X c)}$
At some moment, the patient won't have any symptom again
$\color{blue}{\pos \nec \neg s}$
A patient cannot remain indefinitely confined
$\color{blue}{\neg \pos \nec c}$
If a patient is confined, then she must have had symptoms before
Between two different confinment periods, the patient must have had symptoms
$\color{blue}{\nec \neg (c \wedge \X \neg c
\wedge \X (\neg s \ \U \ c))}$ that is, it is never the case that
we end a confinment $\color{blue}{c \wedge \neg c}$ but then, we don't have
symptoms until we reach a new confinment. This is equivalent to
$\color{blue}{\nec (c \wedge \X \neg c
\to \X ( s \ \R \ \neg c))}$
Exercise 5 (from 1/7/2019). An accused can go to trial
($\color{blue}t$) and, as a consequence, receive a
sentence ($\color{blue}s$) that can be appealed ($\color{blue}a$). Formulate the following sentences in LTL
The accused cannot be sentenced without a previous trial
If the accused goes to trial, she eventually gets a sentence
$\color{blue}{\nec ( t \to \pos s)}$
There is some moment in which no more appeals can be made
$\color{blue}{\pos \nec \neg a}$
The accused cannot go to trial twice without some appeal in between
A simple solution is $\color{blue}{\nec (t
\to \X (\neg t \ \W \ (a \wedge \neg t) ))}$ namely, if she goes
to trial either she is not judged ever again or she is not judged
until an appeal occurs. This formula is equivalent to $\color{blue}{\nec (t
\to \X (a \ \R \ \neg t) )}$ or to $\color{blue}{\nec \neg (t
\wedge \X (\neg a \ \U \ t) )}$