1. Transition systems

A transition system (S,T,I)(S, T, I) is defined as follows:

  • a set of SS;
  • a transition relation T:SST: S \rightarrow S;
  • a set of initial states ISI \subseteq S.

A program is modelled as a transition system. Each state of the program is an evaluation of all variables in the program. Each state may has many possible successors, i.e., the transition relation is non-deterministic.

Example1 : S={a,b,c}S = \{a,b,c\}, I={a}I = \{a\} and T={a,b,b,b,b,c}T = \{ \langle a,b\rangle, \langle b,b\rangle, \langle b,c\rangle\}

example 1

2. Semantics

2.1 maximal trace semantics

The program can be modelled as a transition system. Thus, en execution of the program is a sequence of states $\langle s_0,s_1,…,s_n\rangle $. The execution can go on forever or ends at some state sks_k ( sks_k has no successors) or an error state Ω\Omega . There be many executions due to the non-determinism.

The set of execution traces spawned by a transition system with initial states II and the transition relation T:SST: S \rightarrow S is denoted as Δ\Delta and it is called maximal trace semantics .

Δ={s0...snn0s0I(i[0,n)si,si+1T)\Delta = \{ \langle s_0...s_n \rangle | n \geq 0 \land s_0 \in I \land ( \forall i \in [0,n) \cdot \langle s_i,s_{i+1} \rangle \in T) \land

       (sSsn,sT)}.{s0...s0Ii>0si,si+1t}\ \ \ \ \ \ \ (\forall s' \in S \cdot \langle s_n, s'\rangle \notin T) \}. \cup \{ \langle s_0 ...\rangle | s_0 \in I \land \forall i > 0 \cdot \langle s_i, s_{i+1} \rangle \in t \}

Δ\Delta is the set of maximal sequences of states starting from an initial state, either ending in some final state or infinite and satisfying the transition relation.

In practice, the maximal trace semantics of the program is not computable and not observable since it could be infinite.

To check some safety properties, ie., nothing bad happens, we can observe the finite parts of the program executions (finite or infinite).

However, this will prevents us from reasoning about program termination and liveness properties. (something good happens)

Example1 :
$ \Delta = { \langle ab…c \rangle, \langle ab …\rangle } $

2.2 collecting semantics

2.2.1 prefix trace semantics

We can define finite observation of program execution PP.

$P = { \langle s_0 … s_n\rangle | n \geq 0 \land s_0 \in I \land \forall i \in [0,n)\cdot \langle s_i, s_{i+1} \in T\rangle } \subseteq S^* $.

(SS^* is the set of finite sequences of states form SS).

PP is called the finite prefix trace semantics can it is as an collecting semantics.

Example1: In our finite transition system example, the prefix trace semantics is P={a,ab...b,ab...c}P = \{\langle a\rangle,\langle ab . . . b\rangle,\langle ab . . . c \rangle\}. It contains the one element trace a, as well as traces starting in a followed by a finite sequence of b and ending in b, and traces starting in a followed by a finite (non-empty) sequence of b and ending in c. An example of safety property would be that c cannot occur unless b has occurred before during the execution. The property can be checked by considering only PP, and it is not necessary to consider Δ\Delta. However, observing PP only, it is impossible to deduce whether the program always terminates or not, as any finite trace in PP may actually be the beginning of a longer (possibly infinite) trace.

Now, by computing prefix trace semantics, we can ideally answer all safety questions. Unfortunately, this is not possible: although each trace is now finite and can, individually, be checked automatically, the prefix trace semantics may contain an infinite (or impracticably large) number of such finite traces. Hence, we will use further abstractions of this semantics to provide sound but incomplete answers. The choice of the program properties of interest, hence of the collecting semantics, is problem dependent. It depends on the level of observation of program behaviors required to solve the problem. We illustrate this point with another example of collecting semantics.

2.2.2 reachability semantics

If we only interest in invariance properties, a possible collecting semantics would be the reachability semantics.
R={ssIs,st}SR = \{ s' | \exists s \in I\cdot \langle s, s'\rangle \in t^* \} \subseteq S
where the reflexive transitive closure tS×St^* \subseteq S \times S of a relation tS×St \subseteq S \times S is defined classically:
t={s,sn0s0...sns0=si[0,n)si,si+1tsn=s}t^* = \{ \langle s,s'\rangle | \exists n \geq 0 \cdot \exists s_0...s_n \cdot s_0 = s \land \forall i \in [0,n) \cdot \langle s_i, s_{i+1}\rangle \in t \land s_n = s' \}

As an invariance property is defined as a set of states in which all program executions must stay, computing the reachability semantics is indeed sufficient to check the property. It reduces to checking that RR is included in the state set of the property. The reachability semantics is more abstract than the prefix trace semantics since, although we know exactly which states can be reached during execution, we no longer know in which order. This is a basic example of abstraction.

Assume we are asked the question “does state s1 always appear before state s2 in all executions” and we only know the reachability semantics RR. If s1Rs_1\in R or s2Rs_2 \in R, then we can answer “no” for sure. Otherwise s1,s2Rs_1, s_2 \in R, so, we can only answer “I don’t know,” which is an example of incompleteness which is inherent to reachability with respect to the prefix trace semantics.

Example1: The reachable states of the example 1 is R={a,b,c}R = \{ a,b,c \}

2.2.3 fixpoint semantics

Define a identify relation: idS={s,ssS}id_S = \{ \langle s, s \rangle | s \in S\}

t:SSt : S \rightarrow S
Composition \circ of relations:
tr={s,ss:s,sts,sr}t \circ r = \{ \langle s, s'' \rangle | \exists s': \langle s, s' \rangle \in t \land \langle s',s'' \rangle \in r \}

A fixpoint of a function F:SSF: S\rightarrow S is any element x satisfying F(x)=xF(x) = x.

The least fixpoint of FF, denoted by lplp, satisfying two conditions:

  1. F(lp)=F(lp) = $ \texttt{lp}$, itself is a fixpoint
  2. x,F(x)=x\forall x,F(x)= x such that $ \texttt{lp} \sqsubseteq x$, it is smaller than any other fixpoint

If the least fixpoint exists, it is unique.

The reachable states RR is the fixpoint of function:
FR(X)=I{ssXs,sT}F_R(X) = I \cup \{s'| \exists s\in X \cdot \langle s,s' \rangle \in T \}.

Example1: We iterate FRF_R from \emptyset and get

X0=FR()=I={a}X^0 = F_R (\emptyset) = I = \{ a \}

X1=FR(X0)={a,b}X^1 = F_R(X^0) = \{ a, b\}

X2=FR(X1)={a,b,c}X^2 = F_R(X^1) = \{a,b,c\}

X3=FR(X2)={a,b,c}=X2X^3 = F_R(X^2) = \{ a,b,c\} = X^2

Xn=X2,n2X ^n = X ^2, n\geq2

3. abstraction functions

We defined several semantics we can construct the relation between them by notion of abstractionabstraction. An abstraction is a mathematical relationship between two semantics, a so-called concrete semantics (more precise) and s so-called abstract semantics (less precise).

Soundness of abstraction: any program property proved to hold in the abstract semantics also holds in the concrete one.

Generally, not all properties provable in the concrete semantics can be proved in the abstract semantics: this is incompleteness, which causes false alarms.

Another property of the abstract semantics is termination.

Example: Construction a correspondence between the (concrete) prefix trace semantics and the (abstract) reachability semantics. We denote by $S^* $ the states in prefix trace semantics which is the set of prefix trances. Thus, the abstraction function is defined as:

αR:Pow(S)Pow(S)\alpha_R: Pow(S^*) \rightarrow Pow(S) such that

αR(X)={s  s0...sn}X:s=sn}\alpha_R(X) = \{ s\ |\ \exists \langle s_0...s_n \rangle \}\in X : s=s_n\}.

Given a set of finite sequences in Pow(S)Pow(S^*) as input, it outputs the set of states in Pow(S)Pow(S) that can appear at the last position of the sequence.

The prefix trance semantics collects all finite observations of a program execution and store the last state of every such finite observation, it collects the whole set set of stets reached along all (finite and infinite) executions. The abstraction records the reachable states but no longer the order in which these states appear during execution.

The abstraction function α\alpha is monotonic, i.e., we have that XYX \subseteq Y implies αR(X)αR(Y)\alpha_R(X) \subseteq \alpha_R(Y).

4. Concretisation functions

An abstraction function converts a semantic information from a more concrete semantic world to a more abstract semantic world. We can also consider a reverse function, called concretization function, to convert from an abstract world back to a concrete one.

The counterpart of the abstract function α\alpha is the concretization function:
γR:Pow(S)Pow(S)\gamma_R: Pow(S) \rightarrow Pow(S^*) such that
γR(X)={s0...snXi[0,n]:siX}\gamma_R(X) = \{ \langle s_0...s_n \rangle \in X | \forall i \in [0,n]: s_i \in X\},
given a set of states in Pow(S)Pow(S) outputs a set of finite sequences of states in Pow(S)Pow(S^*).

The concretization rebuilds the prefix execution traces from the reachable states, but considers that they can appear in any order since the order of appearance has been abstracted away.

  1. Soundness: R=αR(P)R = \alpha_R(P)
  2. Incompleteness: $P \subseteq \gamma_R ( R ) $, γR(R)\gamma_R (R) has more possible program bahaviours than the concrete PP.

Example 1: Recall the example represented above, we have reachable states: R={a,b,c}R = \{ a,b,c\}, and prefix trance semantics: P={a,ab...b,ab...c}P = \{ \langle a\rangle,\langle ab . . . b\rangle,\langle ab . . . c \rangle \}

We can check that αR(P)=R\alpha_R(P) = R,
S={,{a},{b},{c},{a,b},{a,c},{b,c},{a,b,c}}S=\{ \emptyset, \{a\},\{b\},\{c\},\{a,b\},\{a,c\},\{b,c\},\{a,b,c\} \}
$\gamma( R ) = S^* $
Property: no cc can occur in an execution without a bb occurring before.
The property is true in prefix trance semantics PP, but not in γ(R)\gamma(R).

5. Galois connections

Intuitively, the abstraction and the concretization functions are “inverse” of one another. This intuition is formalized by the notion of Galois connection α,γ\langle \alpha, \gamma \rangle. Formally, a Galois
connection α,γ\langle \alpha, \gamma \rangle is a pair of functions between two ordered sets: a
concrete set (C, ⊆) equipped with some partial order \subseteq, and an abstractset (A,A,\subseteq^{\sharp}), equipped with another partial order \subseteq^{\sharp}, such that:

  1. α:CA\alpha :C \rightarrow A converts a concrete element into an abstract one;

  2. γ:AC\gamma : A \rightarrow C converts an abstract element into a concrete one;

  3. xC,yA:α(x)y\forall x \in C,y \in A : \alpha(x) \subseteq^{\sharp} y if and only if xγ(y)x \subseteq \gamma ( y ), which is the core property of Galois connections.

6. Sound and complete abstract semantics

Given a concrete semantics SS and an abstraction specified by a concretization function γ\gamma (respectively, an abstraction function α\alpha), we are interested in an abstract semantics SS^{\sharp} which is sound in that Sγ(S)S \subseteq \gamma (S^{\sharp}) (respectively, α(S)S\alpha(S) \subseteq^{\sharp} S^{\sharp}, which is equivalent for Galois connections). This corresponds to the intuition that no concrete case is ever forgotten in the abstract (so there can be no false negative).