Safety and Liveness Properties

During the execution, we will concern certain program properties, such as program correctness, program halt, no exceptions, etc. For those program properties one may interest in, it can be divided into two categories:

  • Safety Properties, It will not step into unexpected state during program execution (such as call with unmatched parameters, array subscript out of bounds, etc.):
  • Liveness Properties, The expected state will arrive during program execution eventually(such as halt, get resource request must return successfully, etc.).

The topology of program properties will be introduced below. Finally, for any program property, it can be decomposed into the intersection of its safety component and liveness component.

Definition 1: transfer system

The transfer system consists of a set of states \(\Sigma\) and a transfer relation \(\to\subseteq\Sigma\times\Sigma\), it is \(\langle\Sigma,\to\rangle\).

The state indicates the current state of the program execution, which is generally composed of the current execution program position (instruction pointer) and the program symbol value (memory space). The transfer relationship is defined by the program semantics.

Definition 2: Trace

\begin{align*} &\Sigma^{*} = \bigcup_{k=0}^{}\Sigma^{k}\\ &\Sigma^{\overrightarrow{*}} = \left\{ \sigma=(\sigma_1\sigma_2\cdots\sigma_k)\in \Sigma^{*}\;|\;\forall i<|\sigma|:\sigma_i \to\sigma_{i+1}\right\} \\ &\Sigma^{\overrightarrow{\omega}} = \left\{ \sigma=(\sigma_1\sigma_2\sigma_3\cdots)\in \Sigma^{\omega}\;|\;\forall i:\sigma_i \to\sigma_{i+1}\right\}\\ &\Sigma^{\overrightarrow{\infty}} = \Sigma^{\overrightarrow{*}}\cup\Sigma^{\overrightarrow{\omega}} \end{align*}

(\(|\sigma|\) is the length of \(\sigma\))

Clearly \(\Sigma^{\overrightarrow{*}}\subseteq\Sigma^{\overrightarrow{\infty}}\) , And \(\sigma\in\Sigma^{\overrightarrow{\infty}}\) is the trace of a program.

Definition 3: concatenation, prefix, suffix, extension

For \(u=(u_1\cdots u_n)\in\Sigma^{\overrightarrow{*}}\) , \(v=(v_1,v_2\cdots)\in\Sigma^{\overrightarrow{\infty}}\) , \(u_{n}\to v_1\), denote \(uv=(u_1\cdots u_n,v_1,v_2\cdots)\) is the concatenation of \(u\) and \(v\).

For \(U, V\subseteq \Sigma^{\overrightarrow{\infty}}\) , denote \(UV=\left\{ uv\;|\;u\in U,v\in V \right\}\) .

\(u\) is the prefix of \(w\) if \(\exists v:uv=w \), similarly \(v\) is the suffix of \(w\), denote \(u\preceq w\) , and \(w\) is a extension of \(u\), denote  \(w\succeq u\).

empty trace \(\epsilon\) , which satisfies \(|\varepsilon|=0\), \(\epsilon\sigma=\sigma\epsilon=\sigma\) .

Definition 4: Prefixa and Extension Closed

Let \(V\subseteq\Sigma^{\overrightarrow{\infty}}\)

  • If \(\forall u\preceq v\in V\) such that \(u\in V\) , then \(V\) is prefix closed.
  • If \(\forall w\succeq v\in V\) such that \(w\in V\) , then \(V\) is extension closed.

Definition 5: Limit Closed and Finite Witnesses

let \(V\subseteq\Sigma^{\overrightarrow{\infty}}\)

If \(\forall w\in \Sigma^{\overrightarrow{\infty}}\) , for any finite \(u\preceq w\) such that \(u\in V\) implies \(w\in V\) , then \(V\) is limit closed.
If \(\forall w\in V\) , there exist finite \(u\preceq w\) such that \(u\in V\) , then \(V\) is finite witnesses.

Proposition 1: if \(V\subseteq\Sigma^{\overrightarrow{\infty}}\) is prefix closed(extension closed), then \(\Sigma^{\overrightarrow{\infty}}\setminus V\) is extension closed(prefix closed).

Proof:

Assume \(\Sigma^{\overrightarrow{\infty}}\setminus V\) is not a extension closed set, so \(\exists w\succeq v\in \Sigma^{\overrightarrow{\infty}}\setminus V: w\not\in \Sigma^{\overrightarrow{\infty}}\setminus V\) that is \(w\in V\) . Since \(V\) is prefix closed, \(w\succeq v\in V\) . Contradiction, therefore \(\Sigma^{\overrightarrow{\infty}}\setminus V\) is extension closed.

Dually, if \(V\) is extension closed, then \(\Sigma^{\overrightarrow{\infty}}\setminus V\) is prefix closed.

Proposition 2: if \(V\subseteq\Sigma^{\overrightarrow{\infty}}\) is limit closed(finite witnesses), then \(\Sigma^{\overrightarrow{\infty}}\setminus V\) is finite witnesses(limit closed).

Proof:

Assume \(\Sigma^{\overrightarrow{\infty}}\setminus V\) is not a finite witnesses set, so \(\exists w\in \Sigma^{\overrightarrow{\infty}}\setminus V: \forall u\preceq w: u\not\in \Sigma^{\overrightarrow{\infty}}\setminus V\) ( \(u\) finite) that is \(\forall u\preceq w: u\in V\) . Since \(V\) is limit closed, \(w\in V\) . Contradiction, therefore \(\Sigma^{\overrightarrow{\infty}}\setminus V\) is finite witnesses.

Dually, if \(V\) is finite witnesses, then \(\Sigma^{\overrightarrow{\infty}}\setminus V\) is limit closed.

Definition 6: Topology space on \(\Sigma^{\overrightarrow{\infty}}\) : \((\Sigma^{\overrightarrow{\infty}}, \tau)\)

\(\tau\) is open sets, \(\tau = \left\{ W\Sigma^{\overrightarrow{\infty}}\;|\;W\subseteq\Sigma^{\overrightarrow{*}}\right\}\) .

Proposition 3:  \(\tau\) is open sets

Proof:

  •  \(\emptyset=W\Sigma^{\overrightarrow{\infty}}\in\tau\) , where \(W=\emptyset\).
  • \(\Sigma^{\infty}=W\Sigma^{\overrightarrow{\infty}}\in\tau\) , where \(W=\{\epsilon\}\).
  • \(W_{\alpha}\subseteq\Sigma^{\overrightarrow{*}}\) , \(\alpha\in I\) , and \(\bigcup_{\alpha\in I}^{}(W_{\alpha}\Sigma^{\overrightarrow{\infty}})=W\Sigma^{\overrightarrow{\infty}}\in\tau\) , where \(W=\left( \bigcup_{\alpha\in I}^{}W_{\alpha} \right)\subseteq\Sigma^{\overrightarrow{*}}\) .
  • \(U, V\subseteq \Sigma^{\overrightarrow{*}}\) , define \(U_{V}=\{u\in U\;|\;\exists v\in V: v\preceq u\}\subseteq U\) , similar definition for \(V_{U}\) .\begin{align*} &w\in U\Sigma^{\overrightarrow{\infty}}\cap V\Sigma^{\overrightarrow{\infty}}\\ \Leftrightarrow\;&\exists u\in U, v\in V: x, y\in \Sigma^{\overrightarrow{\infty}}, w=ux=vy\\ \Leftrightarrow\;&w\in V_U\Sigma^{\overrightarrow{\infty}}\;\text{or}\;w\in U_V\Sigma^{\overrightarrow{\infty}}\;(u\preceq v\;\text{or}\;v\preceq u) \end{align*}Hence \(U\Sigma^{\overrightarrow{\infty}} \cap V\Sigma^{\overrightarrow{\infty}}=U_V\Sigma^{\overrightarrow{\infty}} \cup V_U\Sigma^{\overrightarrow{\infty}}\) , let \(W=U_V \cup V_U\subseteq\Sigma^{\overrightarrow{*}}\) , then\(U\Sigma^{\overrightarrow{\infty}} \cap V\Sigma^{\overrightarrow{\infty}}=W\Sigma^{\overrightarrow{\infty}}\in \tau\).

Therefore \((\Sigma^{\overrightarrow{\infty}}, \tau)\) is a topology on \(\Sigma^{\overrightarrow{\infty}}\).

Lemma 1: \(V\subseteq\Sigma^{\overrightarrow{\infty}}\) is closed if and only if:

\(\forall w\in \Sigma^{\overrightarrow{\infty}}\) for any finite \(u\preceq w\) there exists \(v\succeq u\) such that \(v\in V\) , then \(w\in V\) .

Proof:

\((\Rightarrow)\) assume \(V\subseteq\Sigma^{\overrightarrow{\infty}}\) is closed, then there is \(U\subseteq\Sigma^{\overrightarrow{*}}\) satisfies \(\Sigma^{\overrightarrow{\infty}}\setminus V=U\Sigma^{\overrightarrow{\infty}}\) , if \(w\in \Sigma^{\overrightarrow{\infty}}, w\not\in V\) , then \(w\in U\Sigma^{\overrightarrow{\infty}}\) , there is finite prefix \(u\preceq w, u\in U\) , and \(\forall v\succeq u: v\in U\Sigma^{\overrightarrow{\infty}}\) that is \(v\not\in V\) , so its contrapositive \((\forall (w\in \Sigma^{\overrightarrow{\infty}}, \text{finite}\;u\preceq w): \exists v\succeq u: v\in V) \to w\in V\) holds.

\((\Leftarrow)\) let \(U=\left\{ u\in\Sigma^{\overrightarrow{*}}\;|\; \forall v\succeq u: v\not\in V \right\}\), Clearly \(U\Sigma^{\overrightarrow{\infty}}\subseteq\Sigma^{\overrightarrow{\infty}}\setminus V\) . if \(w\not\in V\) then \(\exists \text{finite}\;u\preceq w: \forall v\succeq u: v\not\in V\) , and \(u\in U\) so \(\exists v:uv=w\) that is \(w\in U\Sigma^{\overrightarrow{\infty}}\) , \(\Sigma^{\overrightarrow{\infty}}\setminus V\subseteq U\Sigma^{\overrightarrow{\infty}}\) . Therefore \(U\Sigma^{\overrightarrow{\infty}}=\Sigma^{\overrightarrow{\infty}}\setminus V\) is open, and \(V\) is closed.

Proposition 4: open and closed set

Let \(V\subseteq\Sigma^{\overrightarrow{\infty}}\)

  • \(V\) is closed if and only if \(V\) is prefix closed and limit closed.
  • \(V\) is open if and only if \(V\) is extension closed and finite witnesses.

Proof:

  • \((\Rightarrow)\) assume \(V\) is closed, for any \(u\preceq v\in V\) , let  \(u^{‘}\) be any finite prefix of \(u\) that is \(u^{‘}\preceq u\) , and \(v\succeq u \succeq u^{‘}\) , by lemma 1 \(u\in V\) implies \(V\) is prefix closed.By lemma 1 \(V\) is limit closed.\((\Leftarrow)\) assume \(V\) is prefix closed and limit closed, if \(w\not\in V\) that is \(w\in \Sigma^{\overrightarrow{\infty}}\setminus V\) , by proposition 1 and 2, \(\Sigma^{\overrightarrow{\infty}}\setminus V\) is extension closed and finite witnesses. From finite witnesses, there is finite \(u\preceq w\) such that \(u\in \Sigma^{\overrightarrow{\infty}}\setminus V\) , and from extension closed, for any \(v\succeq u\) satisfies \(v\in \Sigma^{\overrightarrow{\infty}}\setminus V\) so \(v\not\in V\) , its contrapositive \((\forall (w\in \Sigma^{\overrightarrow{\infty}}, \text{finite}\;u\preceq w): \exists v\succeq u: v\in V) \to w\in V\) hold. By lemma 1 \(V\) is closed.
  • \(V\) is open if and only if \(V\) is extension closed and finite witnesses.\(\Leftrightarrow\) \(\Sigma^{\overrightarrow{\infty}}\setminus V\) is prefix closed and limit closed. (Proposition 1 and 2)\(\Leftrightarrow\) \(\Sigma^{\overrightarrow{\infty}}\setminus V\) is closed (proved above)\(\Leftrightarrow\) \(V\) is open.

Proposition 5: closure and interior

Let \(V\subseteq\Sigma^{\overrightarrow{\infty}}\)

  • \(cl(V)=\left\{ w\in\Sigma^{\overrightarrow{\infty}} \;|\; \forall \text{finite}\;u\preceq w:\exists v\succeq u: v\in V\right\}\).
  • \(int(V)=\left\{ w\in\Sigma^{\overrightarrow{\infty}} \;|\; \exists \text{finite}\;u\preceq w:\forall v\succeq u: v\in V\right\}\).

Proof:

  • Let \(C(V)=\left\{ w\in\Sigma^{\overrightarrow{\infty}} \;|\; \forall \text{finite}\;u\preceq w:\exists v\succeq u: v\in V\right\}\) , assume \(\forall w\in \Sigma^{\overrightarrow{\infty}}\) for any finite \(u\preceq w\) there exist \(v\succeq u\) such that \(v\in C(V)\) , By the definition of \(C(V)\) there is \(v^{‘}\succeq u\) satisfies \(v^{‘}\in V\) , so \(w\in C(V)\) by lemma 1 \(C(V)\) is closed. Let \(V\subseteq \Gamma \subseteq\Sigma^{\overrightarrow{\infty}}\) , \( \Gamma\) is a closed set, assume \(w\in C(V)\) then \(\forall \text{finite}\;u\preceq w:\exists v\succeq u: v\in V \subseteq \Gamma \) , and \( \Gamma\) is closed, by lemma 1 \(w\in \Gamma\) that is \(C(V)\subseteq\Gamma\) .Therefore \(C(V)\) is the closure of \(V\).
  • Let \(I(V)=\left\{ w\in\Sigma^{\overrightarrow{\infty}} \;|\; \exists\text{finite}\;u\preceq w:\forall v\succeq u: v\in V\right\}\) , assume \(w\in I(V)\) then \(\exists\text{finite}\;u\preceq w:\forall v\succeq u: v\in V\) , from the definition of \(I(V)\), \(\forall v\succeq u: v\in I(V)\) , so \(w\in u\Sigma^{\overrightarrow{\infty}}\subseteq I(V)\) and \(u\Sigma^{\overrightarrow{\infty}}\) is open, \(I(V)=\bigcup_{w\in I(V)}^{}u\Sigma^{\overrightarrow{\infty}}\), hence \(I(V)\) is open.Let \(w\in\Delta\subseteq V\) , \(\Delta\) is a open set, so exists \(U \subseteq\Sigma^{\overrightarrow{*}}\) such that \(w\in U\Sigma^{\overrightarrow{\infty}} \subseteq \Delta\) , it follows \(\exists u\in U: u\preceq w\) , then \(\forall v\succeq u: v\in U\Sigma^{\overrightarrow{\infty}} \subseteq \Delta\subseteq V\) , from the definition of \(I(V)\), \(w\in I(V)\) that is \(\Delta\subseteq I(V)\) .Therefore \(I(V)\) is the interior of \(V\).

Definition 7: safety property and liveness property

  • If \(\forall w\in\left(\Sigma^{\overrightarrow{\infty}}\setminus W\right): \exists\text{finite}\;u\preceq w\;\text{s.t.}\;\forall v:uv\in\left(\Sigma^{\overrightarrow{\infty}}\setminus W\right)\) then \(W\) is a safety property.
  • If \(\forall\text{finite}\;u:\exists v\;\text{s.t.}\;uv\in W\) then \(W\) is a liveness property.

Note: The meaning of safety property is that if a trace violates the safety property, it can be identified by its finite prefix. The meaning of liveness property is that for any finite trace, there is always an extension to satisfy the liveness property.

Proposition 6: \(W\) is a safety property if and only if \(W\) closed.

Proof:

\begin{align*}&\text{W is safety property}\\&\Leftrightarrow \forall w\in\left(\Sigma^{\overrightarrow{\infty}}\setminus W\right): \exists\text{finite}\;u\preceq w\;\text{s.t.}\;\forall v:uv\in\left(\Sigma^{\overrightarrow{\infty}}\setminus W\right)\\ &\Leftrightarrow \left(\forall w\not\in W\right)\to\left(\exists\text{finite}\;u\preceq w\;\text{s.t.}\;\forall u^{‘}\succeq u:u^{‘}\in\left(\Sigma^{\overrightarrow{\infty}}\setminus W\right)\right)\\ &\Leftrightarrow \left(\forall\text{finite}\;u\preceq w\;\text{s.t.}\;\exists u^{‘}\succeq u:u^{‘}\in W\right)\to w\in W \quad\text{[contrapositive]}\\ &\Leftrightarrow W\;\text{is closed}\;\quad\text{[lemma 1]}\\ \end{align*}

Proposition 7: \(V\) is a liveness property if and only if \(V\) dense.

Proof:

\((\Rightarrow)\) \(V\) is a liveness property. Assume \(V\subseteq \Gamma\) , \(\Gamma\) is closed. if there exists \(w\in\Sigma^{\overrightarrow{\infty}}\setminus \Gamma\) that is \(w\not\in\Gamma\) , By lemma 1, there is finite \(u\preceq w\) such that for any \(v\succeq u\) it satisfies \(v\not\in V\) . And from \(V\) is a liveness property, exists \(v\succeq u\) such that \(v\in V\subseteq \Gamma\) , contradiction. Therefore \(\Sigma^{\overrightarrow{\infty}}\setminus \Gamma=\emptyset\) that is \(\Gamma=\Sigma^{\overrightarrow{\infty}}\) , \(V\) dense.

\((\Leftarrow)\) \(V\) dense. assume \(V\) is not liveness property, then exists finite \(u\) such that \(\forall v\succeq u: v\not\in V\) , so \(u\Sigma^{\overrightarrow{\infty}}\subseteq\Sigma^{\overrightarrow{\infty}}\setminus V\) that is \(V\subseteq\Sigma^{\overrightarrow{\infty}}\setminus u\Sigma^{\overrightarrow{\infty}}\) , And \(\Sigma^{\overrightarrow{\infty}}\setminus u\Sigma^{\overrightarrow{\infty}}\) is closed, by the dense of \(V\),  \(\Sigma^{\overrightarrow{\infty}}\setminus u\Sigma^{\overrightarrow{\infty}}=\Sigma^{\overrightarrow{\infty}}\) , \(u\Sigma^{\overrightarrow{\infty}}=\emptyset\) which implies \(u\) does not exists, contradiction. Therefore \(V\) is a liveness property.

Definition 8: safety component and liveness component

  • \(safe(V)=cl(V)\) .
  • \(live(V)=\Sigma^{\overrightarrow{\infty}}\setminus \left( cl(V)\setminus V \right)\).

Lemma 2: \((X,\tau)\) is a Topology space, \(Y\subseteq X\) then \(X\setminus (cl(Y)\setminus Y)\) dense.

Proof:

Let \(X\setminus (cl(Y)\setminus Y)\subseteq Z\) , \(Z\) is closed.

\(X\setminus Z \subseteq cl(Y) \setminus Y\)

And \(Y\subseteq cl(Y)\) so

\(Y\subseteq cl(Y)\setminus(X\setminus Z)\)

\(X\setminus Z\) is closed, so \(cl(Y)\setminus(X\setminus Z)\) is closed as well, then \(cl(Y)\setminus(X\setminus Z) \subseteq cl(Y)\) that is \(X\setminus Z=\emptyset\) ,\(Z=X\) . Therefore \(X\setminus (cl(Y)\setminus Y)\) dense.

Corollary 1: \(V\) is a safety property if and only if \(safe(V)=V\) .

Proof:

By proposition 6, \(V\) is safety property if and only if \(V\) closed, so \(V=cl(V)\overset{\mathrm{def}}{=}safe(V)\) .

Corollary 2: for any \(V\subseteq\Sigma^{\overrightarrow{\infty}}\), \(safe(V)\) is a safety property.

Proof:

\(safe(V)\overset{\mathrm{def}}{=}cl(V)\) is closed. By proposition 6, \(safe(V)\) is a safety property.

Corollary 3: \(V\) is a liveness property if and only if \(live(V)=V\) .

Proof:

By proposition 7, \(V\) is a liveness property if and only if \(V\) dense, so \(cl(V)=\Sigma^{\overrightarrow{\infty}}\) \(live(V)\overset{\mathrm{def}}{=}\Sigma^{\overrightarrow{\infty}}\setminus \left( cl(V)\setminus V \right)=\Sigma^{\overrightarrow{\infty}}\setminus \left( \Sigma^{\overrightarrow{\infty}}\setminus V \right)=V\) .

Corollary 4: for any \(V\subseteq\Sigma^{\overrightarrow{\infty}}\), \(live(V)\) is a liveness property.

Proof:

\(live(V)\overset{\mathrm{def}}{=}\Sigma^{\overrightarrow{\infty}}\setminus \left( cl(V)\setminus V \right)\). By lemma 2, \(live(V)\) is dense, and by proposition 7, \(live(V)\) is a liveness property.

Lemma 3: \((X,\tau)\) is a Topology space, \(Y\subseteq X\) then

\(Y=cl(Y)\cap(X\setminus (cl(Y)\setminus Y))\)

Proof:

\begin{align*} cl(Y)\cap(X\setminus (cl(Y)\setminus Y))&=(X\cap cl(Y))\setminus ((cl(Y)\setminus Y)\cap cl(Y))\\ &=cl(Y)\setminus (cl(Y)\setminus Y)\\ &=Y \end{align*}

Theorem 1: property decomposition

For any property \(P\) , It can be decomposed into the intersection of its safety component and its liveness component.

\(P=safe(P)\cap live(P)\)

Proof:

\begin{align*} P&=safe(P)\cap live(P)\\ &\overset{\mathrm{def}}{=}cl(P)\cap\left(\Sigma^{\overrightarrow{\infty}}\setminus (cl(P)\setminus P)\right)\\ &=P\quad\text{[lemma 3]} \end{align*}

An example:

program total correctness can be decomposed into partial correctness(safety component) and termination(liveness component).

\(\Upsilon\subseteq\Sigma\) is initial state.
\(\Omega\subseteq\Sigma\) is termination state.
\(\Psi\subseteq\Upsilon\times\Omega\) is partial correctness relation.
\(\Phi\overset{\mathrm{def}}{=}\left\{ (s,s^{‘})\;|\;(s\in\Upsilon) \Rightarrow((s\to^{*}s^{‘})\wedge (s^{‘}\in\Omega)\wedge (s,s^{‘})\in\Psi)\right\}\)is total correctness relation.
partial correctness:

\(\forall s,s^{‘}\in\Sigma:\left((s\to^{*}s^{‘})\wedge (s\in\Upsilon)\wedge (s^{‘}\in\Omega))\right)\Rightarrow \left( (s,s^{‘})\in\Psi \right)\)

termination:

\(\forall \sigma\in\Sigma^{\overrightarrow{*}}:\left( \sigma_0 \in\Upsilon \right)\Rightarrow\left(\exists l=|\sigma|:\sigma_l\in\Omega\right)\)

total correctness:

\(\forall \sigma\in\Sigma^{\overrightarrow{*}}:\left(\exists l=|\sigma|:(\sigma_1,\sigma_l)\in\Phi\right)\)

Proof:

\begin{align*} &\forall \sigma\in\Sigma^{\overrightarrow{*}}:\left( \sigma_0 \in\Upsilon \right)&\text{[initial states]}\\ \Rightarrow\;&\sigma_0 \in\Upsilon\wedge\exists l=|\sigma|:\sigma_l\in\Omega&\text{[termination]}\\ \Rightarrow\;&(\sigma_0, \sigma_l)\in\Psi&\text{[partial correctness]}\\ \Rightarrow\;&(\sigma_0, \sigma_l)\in\Phi&\text{[proving total correctness]}\\ \end{align*}

Leave a Reply

Your email address will not be published. Required fields are marked *