Temporal specifications
Temporal specifications
Frédéric Herbreteau, Bordeaux INP/LaBRI (frederic.herbreteau@bordeaux-inp.fr)
Objective
- Use model-checking to assert the correctness of a system
- from a model $M$: a set of runs given as a transition system
- and a specification $\varphi$ \(M \models \varphi\)
- The specification $\varphi$ shall specify which runs are correct and which are not
- A dedicated algorithm is then use to decide wether $M \models \varphi$ or not
Not all specifications are invariant properties
Specifications and properties
What is a specification?
- Property of the runs of a system: which runs are correct and which are not?
- Must have a clear and well-defined semantics
Example: mutual exclusion
”$\textcolor{blue}{P_1}$ and $\textcolor{red}{P_2}$ do not access the critical section simultaneously”
Formalising specifications
- $AP$ = set of atomic propositions on states (labels)
- $\Sigma = 2^{AP}$ is the set of all sets of atomic propositions (observations)
- $\Sigma^*$ and $\Sigma^\omega$ are the sets finite and infinite sequences over $\Sigma$
- A property $P$ is any subset of infinite traces from $\Sigma^\omega$
Example: mutual exclusion (cf. previous slide)
- $AP$?
- What is $\Sigma$?
- Give some traces from $\Sigma^*$ From $\Sigma^\omega$?
- Express “$\textcolor{blue}{P_1}$ and $\textcolor{red}{P_2}$ do not access the critical section simultaneously”
Temporal properties
- Temporal refers to logical time
- Temporal properties express requirements over infinite sequences of states
Example:
- “Accesses to the critical section are alternatively granted to $\textcolor{blue}{P_1}$ and $\textcolor{red}{P_2}$”
- “If $\textcolor{blue}{P_1}$ requests the critical section, then access is eventually granted”
- A temporal property is true for a model if all its runs satisfy the property
- Two kinds of temporal properties: safety and liveness
Safety properties - “Nothing bad will never happen”
Example:
- Invariant properties are a special case of safety properties
- Partial correcteness for sequential programs
- ”$\textcolor{blue}{P_1}$ and $\textcolor{red}{P_2}$ do not access the critical section simultaneously”
- “Accesses to the critical section are alternatively granted to $\textcolor{blue}{P_1}$ and $\textcolor{red}{P_2}$”
A safety property is characterised by a set $B \subseteq \Sigma^*$ of finite counter-examples
Definition A set $P \subseteq \Sigma^\omega$ is a safety property if there exists a set $B \subseteq \Sigma^*$ of finite counter-examples such that $P = \Sigma^\omega - (B \Sigma^\omega)$
Liveness properties - “Something good will eventually happen”
Example:
- Termination for sequential program
- “Each process will eventually enter the critical section”
- “If $\textcolor{blue}{P_1}$ requests the critical section, then access is enventually granted”
- “Processes enter the critical section infinitely often”
A liveness property is characterised by infinite counter-examples.
Definition: $P \subseteq \Sigma^\omega$ is a liveness property if every finite sequence can be extended into an infinite sequence in $P$
Example: mutual exclusion
Safety: “nothing bad never happens” - finite counter-examples Liveness: “something good eventually happens” - infinite counter-examples
Example: Processes compete to access their critical sections protected by a lock.
Safety of liveness?
- Two processes never access their critical section at the same time
- Each process accesses the critical section infinitely often
- If a process requires access to the critical section, access is eventually granted
- The lock is never stolen
Decomposition of specifications
Decomposition lemma: For every property $P \subseteq \Sigma^\omega$, there exists a safety property $S$ and a liveness property $L$ such that $P = S \cap L$.
Proof: let $Closure(P)$ be the set of words $w \in \Sigma^\omega$ s.t. all their prefixes are prefixes of words in $P$. Then, choose $S = Closure(P)$ and $L = P \cup (\Sigma^\omega - Closure(P))$
Exercise: which properties are safety and liveness at the same time?
- Specifications mix safety, to ensure good behavior, and liveness, to ensure progress
- For sequential programs: correctness (w.r.t. precondition and postcondition) and termination
Temporal Logic
Temporal formulas
$\varphi ::= p \, \vert \, \lnot \varphi \, \vert \, \varphi \land \varphi \, \vert \varphi \lor \varphi \, \vert \, \varphi \implies \varphi \, \vert \, \Box \varphi \, \vert \, \Diamond \varphi \qquad\qquad \text{with } p \in AP$
- $\Box$ means “always”
- $\Diamond$ means “eventually”
Example:
- $\Box \lnot (\textcolor{blue}{cs_1} \land \textcolor{red}{cs_2})$
- $\Diamond \textcolor{blue}{cs_1} \land \Diamond \textcolor{red}{cs_2}$
- $\Box (\textcolor{blue}{req_1} \implies \Diamond \textcolor{blue}{cs_1})$
Semantics of temporal formulas
Expressed over infinite sequences of observations (sets of labels):
Example: labels ${\textcolor{blue}{cs_1}$, $\textcolor{red}{cs_2}}$ trace: {} {} {$\textcolor{blue}{cs_1}$} {} {$\textcolor{red}{cs_2}$} {} {} … {} {$\textcolor{red}{cs_2}$} {} {$\textcolor{blue}{cs_1}$} {} {} {$\textcolor{blue}{cs_1}$, $\textcolor{red}{cs_2}$} {} {} …
$\sigma$ an infinite trace, $\sigma[i]$ its value in $i$, $\sigma[i…]$ its suffix from $i$
- $\sigma \models p$ if $p \in \sigma[1]$
- $\sigma \models \lnot \varphi$ if $\sigma \not\models \varphi$
- $\sigma \models \varphi_1 \land \varphi_2$ if $\sigma \models \varphi_1$ and $\sigma \models \varphi_2$
- $\sigma \models \Box \varphi$ if $\sigma[i…] \models \varphi$ for every $i \ge 1$
- $\sigma \models \Diamond \varphi$ if there exists $i \ge 1$ such that $\sigma[i…] \models \varphi$
Illustration
Example: Labels: ${\textcolor{blue}{req_1}, \textcolor{blue}{cs_1}, \textcolor{red}{cs_2}}$
Traces:
- $\sigma_1$: {} {} {$\textcolor{blue}{cs_1}$} {} {$\textcolor{red}{cs_2}$} {} {} … {} {$\textcolor{red}{cs_2}$} {} {$\textcolor{blue}{cs_1}$} {} {} {$\textcolor{blue}{cs_1}$, $\textcolor{red}{cs_2}$} {} {} …
- $\sigma_2$: {} {$\textcolor{blue}{cs_1}$} {} {} {$\textcolor{red}{cs_2}$} {$\textcolor{blue}{req_1}$} {} {} {} {$\textcolor{blue}{cs_1}$} {} … {} {$\textcolor{blue}{req_1}$} {} {$\textcolor{red}{cs_2}$} {} {} {} {} …
Are the formulas below satisfied or not by the traces above?
- $\Box \lnot (\textcolor{blue}{cs_1} \land \textcolor{red}{cs_2})$
- $\Diamond \textcolor{blue}{cs_1} \land \Diamond \textcolor{red}{cs_2}$
- $\Box (\textcolor{blue}{req_1} \implies \Diamond \textcolor{blue}{cs_1})$
Combining operators
- $\Box\Diamond$ “infinitely often”
- $\Diamond\Box$ “almost always”
- $\rightsquigarrow$ “leads-to” (
~>in TLA+): $\varphi_1 \rightsquigarrow \varphi_2$ is a shortcut for $\varphi_1 \implies \Diamond \varphi_2$
Example: Write traces that satisfy the formulas below, and traces that falsify them:
- $\Box\Diamond \textcolor{blue}{cs_1}$
- $\Diamond\Box \textcolor{blue}{req_1}$
- $\textcolor{blue}{req_1} \rightsquigarrow \textcolor{blue}{cs_1}$
- $\Box (\textcolor{blue}{req_1} \rightsquigarrow \textcolor{blue}{cs_1})$
Relation between $\Box$ and $\Diamond$
Exercise: Give traces that are respectively satisfied by $\Box p$, $\Box \lnot p$, $\lnot \Box p$, $\Diamond p$, $\Diamond \neg p$, $\neg \Diamond p$
- What is the difference between $\Box \lnot p$ and $\lnot \Box p$?
- What is the difference between $\Diamond \lnot p$ and $\lnot \Diamond p$?
- What is the relation between $\Box$ and $\Diamond$?
Semantics over a transition system
Definition A transition system $M$ satisfies a temporal formula $\varphi$ ($M \models \varphi$) if $\sigma \models \varphi$ for every infinite trace $\sigma$ from an initial state of $M$.
Example: Which formulas below are satisfied by the model to the right?
- $\Box \lnot (\textcolor{blue}{cs_1} \land \textcolor{red}{cs_2})$
- $\Diamond \textcolor{blue}{cs_1} \land \Diamond \textcolor{red}{cs_2}$
- $\Box (\textcolor{blue}{req_1} \implies \Diamond \textcolor{blue}{cs_1})$
Temporal formulas in TLA+
-
Corresponding TLA+ operators:
~,/\,\/,=>,[],<> -
Specification of temporal formulas:
NoStarvation == [](req1 ~> cs1) (* in the .tla file *)
PROPERTY NoStarvation \* in the .cfg file