Model of Computation
A system is a set \(S\) of states, a set \(init\) of initial states,
a set \(actions\) of
actions and a state-transition relation \(\rightarrow\) which is a
subset of \(S \times actions \times S\). The notation \(s
\stackrel{a}{\rightarrow} s'\) means that the execution of action
\(a\) can cause a transtion from state \(s\) to state \(s'\).
Every action can be executed in every state: For all actions \(a\)
and all states \(s\) there is at least one state \(s'\) such that
\(s \stackrel{a}{\rightarrow} s'\). A transition can be a state back
to itself. When a transition \(s \stackrel{a}{\rightarrow} s'\)
exists in a system we shall say that execution of action \(a\) in
state \(s\) can take the system to state \(s'\).
There can be more than one transition from a state \(s\) when an
action \(a\) is executed. For example a system may have transitions
\(s \stackrel{a}{\rightarrow} s'\) and \(s \stackrel{a}{\rightarrow}
s''\) where \(s'\) and \(s''\) are different.
This module introduces all the concepts that we use in this
course to prove that systems are safe. These concepts are
described in terms of
directed graphs.
Representing a System by a Graph
We represent the states and state transitions of a system by a
directed graph
in which vertices represent states and edges
represent transitions. A system trajectory is a path through the
graph.
When we design algorithms we will prove that the system always
remains in safe states.
Prove that a system is
safe by showing that all
paths from vertices representing initial states
only visit vertices representing safe states.
Of course, we require that initial states are safe.
Graphs
Let \(G = (V, \rightarrow) \) be a directed graph where \(V\) is the
set of vertices and \(\rightarrow \) is a binary
relation on vertices that specifies the set of
edges:
\(v \rightarrow w\) indicates that there
is an edge from vertex \(v\) to vertex \(w\) in
the graph.
We use the notation
\(\stackrel{*}{\rightarrow}\)
to denote the transitive closure of
\(\rightarrow\).
So, \(v \stackrel{*}{\rightarrow} w\) holds exactly
when there exists a path from \(v\) to \(w\) in
the graph. We assume that there exists a path, with zero hops, from each
vertex to itself.
\(\forall v: \; v \rightarrow v \)
We use upper case \(P, Q, R, X, Y\) to refer to sets of vertices,
and lower case \(u, v, w \) to refer to individual
vertices.
All formulae containing these terms are
implicitly universally qualified.
Relations between Vertex Sets
\(P \rightarrow Q\)
We extend the relation \(\rightarrow\)
to sets of vertices as follows.
\(P \rightarrow Q\) holds exactly when every edge from every vertex in
\(P\) ends at a vertex in \(Q\).
\(
\forall v \in P: (v \rightarrow w) \; \Rightarrow \; (w \in Q)
\)
>
Fig.2 - Illustration of \(P \rightarrow Q\)
The diagram illustrates \(P \rightarrow Q\). The diagram shows that
there may be vertices in \(Q\), such as vertex \(x\), for which
there is no edge from \(P\).
Example of \(P \rightarrow Q\)
\(
\{2, 3\} \rightarrow \{4, 5, 6\}
\)
Explanation: All outgoing edges from vertices \(2\) and \(3\)
terminate at vertices in \(\{4, 5, 6\}\).
\(P \stackrel{*}{\rightarrow} Q\)
We extend the relation \(\stackrel{*}{\rightarrow}\)
to sets of vertices in the same way.
\(P \stackrel{*}{\rightarrow} Q\) holds exactly when every path
from every vertex in \(P\) ends at a vertex in \(Q\).
\(
\forall v \in P: (v \stackrel{*}{\rightarrow} w) \; \Rightarrow \; (w \in Q)
\)
Therefore
\(P \stackrel{*}{\rightarrow} Q\) holds exactly when all paths from
\(P\) lie entirely in \(Q\), i.e., all vertices on all paths from
\(P\) are in \(Q\).
>
Fig.3 - Illustration of \(P \stackrel{*}{\rightarrow} Q\)
In the diagram, all the vertices in the outer circle are in
\(Q\). Both vertices in the green area and the yellow area are in
\(Q\). The vertices in the yellow area are in \(P\).
\(P \stackrel{*}{\rightarrow} Q\) holds when all paths from vertices
in \(P\) are in \(Q\). The graph shows that no path from the yellow
area can escape the outer circle.
\(P\) lies entirely within \(Q\) because there are zero-length paths
from each vertex in \(P\) back to itself (and so \(P
\stackrel{*}{\rightarrow} P\)) and these paths must lie
inside \(Q\).
There may be a vertex \(w\) in \(Q\)
which has an edge to a vertex outside \(Q\). Then there can be no
path to \(w\) from \(P\) because, in that case, there would be a path from \(P\)
to outside \(Q\).
Example of \(P \stackrel{*}{\rightarrow}
Q\)
\(
\{1, 2\} \rightarrow \{1, 2, 4, 5, 6, 7\}
\)
Explanation: There is a zero-hop path from vertex \(1\) back to
itself, and from vertex \(2\) back to itself. There are paths from
\(2\) to \(4\) and \(5\), and there are paths from \(1\) to \(6\) and
\(7\). There are no paths from \(1\) or \(2\) to \(0\) or \(3\).
Safety Proof Obligation
Let \(init\) be the set of initial vertices and \(safe\) be the set of
safe vertices.
To prove that a system is safe, we must show
that:
Equation 1: \(init \stackrel{*}{\rightarrow} safe\)
Stable
stable is a function from sets of vertices to the Booleans.
\(stable(P)\) holds exactly when every edge from a vertex in \(P\) is
to a vertex in \(P\).
\(
stable(P) \; \equiv \; (P \rightarrow P)
\)
>
Fig.4 - Paths from a stable set remain in the set
There are no paths from inside a stable set to outside the set because
there are no edges from inside to outside the set. One can think of
paths from a stable set as being trapped inside the set. There may,
however, be paths from outside a stable set into the set as shown in
the diagram.
From the definition, \(stable(P)\) holds exactly when all paths from vertices
in \(P\) are in \(P\).
\(
\textit{stable}(\{4, 5\})
\)
Explanation: Every outgoing edge from vertex \(4\) is to vertex \(5\)
which is in set \(\{4, 5\}\), and every
outgoing edge from vertex \(5\) is to vertex \(4\)
which is in set \(\{4, 5\}\).
How to Prove Safety: Invariant
We prove safety (equation 1: \(init \stackrel{*}{\rightarrow} safe\))
by finding a stable vertex set \(I\) such that:
equation 2:
\(
init \subseteq I \subseteq safe
\)
>
Fig.5 - Illustration of Invariant I
Any stable vertex set \(I\) that satisfies equation 2, \(init
\subseteq I \subseteq safe\), is called an invariant of the
graph. Because \(I\) is stable, all paths from \(I\) remain within
\(I\). So all paths from \(init\) remain within \(I\). Therefore,
all paths from \(init\) remain within \(safe\).
We discharge our safety proof obligation by finding an
invariant.
A system may have many invariants; all we have to do is find any one.
Next and Always
\(N\), read as "next", and \(A\), read as "always" are
functions from vertex sets to vertex sets.
\(v\) is in \(N(Y)\) exactly when every single hop from \(v\)
ends at a vertex in \(Y\).
\(v\) is in \(A(Y)\) exactly when every path from \(v\) ends at
a vertex in \(Y\).
\(
v \in N(Y) \; \equiv \; \forall w: (v \rightarrow w) \Rightarrow
( w \in Y)
\)
\(
v \in A(Y) \; \equiv \;
\forall w: (v \stackrel{*}{\rightarrow} w) \Rightarrow
( w \in Y)
\)
Diagram Illustrating Next
>
Fig.6 - Illustration of Next
In the diagram, all the vertices in the outer circle are in
\(Y\). Both vertices in the green area and the yellow area are in
\(Y\). The vertices in the yellow area are in \(N(Y)\). Why is
vertex \(1\) in \(N(Y)\)? Because all the edges from vertex \(1\) go to
vertices \(A\) and \(B\) which are in \(Y\). Vertices \(2, 3, 4\) are
in \(N(Y)\) for the same reason.
Vertex \(A\) is in \(Y\) but not in \(N(Y)\). Why? Because there is an
edge from \(A\) to \(C\) which is outside \(Y\).
Example of Next
\(
N(\{0, 1, 2, 3, 7\}) = \{0\}
\)
Explanation: Every edge from \(0\) terminates at vertices in \(\{0,
1, 2, 3, 7\}\), and so \(0\) is in \(N(\{0, 1, 2, 3\})\).
Likewise, every edge from \(1\) terminates at vertices in \(\{0,
1, 2, 3, 7\}\), and so \(1\) is in \(N(\{0, 1, 2, 3\})\).
Every vertex \(v\)
other than \(0\) and \(1\) has an outgoing edge that terminates at a vertex outside \(\{0,
1, 2, 3, 7\}\),
and so these vertices are not
in \(N(\{0, 1, 2, 3, 7\}\).
Example of Next
\(
N(\{3, 5\}) = \{\}
\)
Explanation: Vertex \(0\) is not in \(N(\{3, 5\})\) because there is
an edge from \(0\) to \(2\) which is not in \(\{3, 5\}\). Likewise, we
see that every vertex has an edge to a vertex outside \(\{3, 5\}\).
In the diagram, all the vertices in the outer circle are in
\(Y\). Both vertices in the green area and the yellow area are in
\(Y\). The vertices in the yellow area are in \(A(Y)\). All paths
from vertices in \(A(Y)\) - the yellow circle - remain inside \(Y\)
- the outer circle.
Note that all paths from the yellow circle remain inside the yellow
circle. Why do you think that is the case?
Example of Always
\(
A(\{0, 1, 3, 6, 7\}) = \{1, 6, 7\}
\)
Explanation: The only edge from vertex \(6\) is \(6 \rightarrow
6\). So, all paths from vertex \(6\) visit only vertex \(6\) which
is in the set \(\{0, 1, 3, 6, 7\}\). Therefore \(6\) is in
\(A(\{0, 1, 3, 6, 7\})\).
The only edge from vertex \(7\) is
\(7 \rightarrow 6\).
So, all paths from vertex \(7\) visit only vertices \(6\) and \(7\),
both of which
are in the set \(\{0, 1, 3, 6, 7\}\).
Therefore \(7\) is in
\(A(\{0, 1, 3, 6, 7\})\).
By the same argument, all paths from vertex \(1\) visit only
vertices \(1\), \(6\) and \(7\), all of which are in set \(\{0, 1,
3, 6, 7\}\), and so \(1\) is in \(A(\{0, 1, 3, 6, 7\})\).
Why isn't \(0\) in \(A(\{0, 1, 3, 6, 7\})\)? Because there is a path
from \(0\) to \(2\) which is not in \(\{0, 1, 3, 6, 7\}\).
Similarly \(3\) is not in \(A(\{0, 1, 3, 6, 7\})\) because of paths
from \(3\) to \(5\).
Every vertex \(v\) that is not in \(\{0, 1, 3, 6, 7\}\) has a path
from \(v\) to \(v\), and so these vertices are not in \(A(\{0, 1, 3,
6, 7\})\).
The safety proof obligation, in terms of always is:
\(init \subseteq A(safe)\)
Successors and Reachable
A vertex \(w\) is a successor of a vertex \(v\) exactly when
the edge \((v, w)\) exists.
A vertex \(w\) is reachable from a vertex \(v\) exactly when
there exists a path from \(v\) to \(w\).
We define functions, \(succesor\) and \(reachable\) from vertex sets
to vertex sets as follows:
\(successor(P)\) and \(reachable(P)\) are the set of successors
of vertices in \(P\) and the set of vertices reachable from vertices
in \(P\), respectively.
\(
w \in successor(P) \quad \equiv \quad
\exists v \in P: v \rightarrow w
\)
\(
w \in reachable(P) \quad \equiv \quad
\exists v \in P: v \stackrel{*}{\rightarrow} w
\)
Relations or Functions
You can use either \(\rightarrow\) or next or successor, because:
\(N(Q)\) and \(A(Q)\) are the weakest (largest) sets \(P\) such that
that \(P \rightarrow Q\) and \(P \stackrel{*}{\rightarrow} Q\), respectively,
hold. Likewise,
\(successor(P)\) and \(reachable(P)\) are the strongest (smallest) sets \(Q\) such that
that \(P \rightarrow Q\) and \(P \stackrel{*}{\rightarrow} Q\), respectively,
hold.
Whether you use the relations \(\rightarrow\) and
\(\stackrel{*}{\rightarrow}\) or the functions \(N\) and \(A\), or the
functions \(successor\) and \(reachable\), is a
matter of personal preference. In this course we use \(\rightarrow\) and
\(\stackrel{*}{\rightarrow}\).
Summary
This chapter describes all the concepts that we use to prove that
systems are safe. These concepts are \(\rightarrow\) and
\(\stackrel{*}{\rightarrow}\) (or equivalently
next and always), stable and invariant.
K. Mani Chandy,
Emeritus Simon Ramo Professor,
California Institute of Technology
>
>
>
>
>
>
>