Program Graph

A program graph \(\texttt{PG} = (Q, \{ q_{\vartriangleright}, q_{\blacktriangleleft} \}, \texttt{Act}, \texttt{E})\) consists of the following:

• \(Q\) a finite set of Nodes.
• \(q_{\vartriangleright}, q_{\blacktriangleleft} \in Q\) two nodes called the initial node and the final node, respectively.
• \(\texttt{Act}\): a set of actions.
• \(\texttt{E} \subseteq Q \times \texttt{Act} \times Q\), a finite set of edges.

An edge \((q_\circ, \alpha, q_\bullet)\) has source node \(q_\circ\) and target node \(q_\bullet\), and it is labelled with the action 𝛼.

We shall require that the initial and final nodes are distinct and that there are no edges with source \(q_\bullet\). (Nielson and Nielson 2019, 2)

The edge labels of represent the computational "actions" that take place once the program reaches a certain state, there is no semantics behind the edges in this defiition (which is why the \(\texttt{Act}\) has a generic definition). For a semantic-based formalism look at Kripke Structures.

A program graph \(\texttt{PG}\) over set \(\texttt{Var}\) of typed variables is a tuple \((\texttt{Loc}, \texttt{Act}, \texttt{Effect}, \longrightarrow, \texttt{Loc}_0, g_0)\) where:

• \(\texttt{Loc}\) is a set of locations and \(\texttt{Act}\) is a set of actions.
• \(\texttt{Effect} : \texttt{Act} \times \texttt{Eval}(\texttt{Var}) \rightarrow \texttt{Eval}(\texttt{Var})\) is the effect function, which indicates how the evaluation \(\eta\) of variables is changed by performing an action.
• \(\longrightarrow \subseteq \texttt{Loc} \times \texttt{Cond}(\texttt{Var}) \times \texttt{Act} \times \texttt{Loc}\) is the conditional transition relation.
• \(\texttt{Loc}_0 \subseteq \texttt{Loc}\) is a set of initial locations.
• \(g_0 \in \texttt{Cond}(\texttt{Var})\) is the initial condition.

(Baier and Katoen 2008, 32 chap.2 part.2.1.2)

The following conventions are also useful:

• \(l \xrightarrow{g:\alpha} l^\prime\) is a notation for \((l, g, \alpha, l^\prime) \in \longrightarrow\).
• The condition \(g\) is also called the guard of the conditional transition \(l \xrightarrow{g:a} l^\prime\).
• If the guard is a tautology (e.g., \(g = \texttt{true} \, \lor g = (x < 1) \lor (x \geq 1)\)), the the transition is shortened to \(l \xrightarrow{a} l^\prime\).

To better understand the \(\texttt{Effect}\) function. Given an \(\alpha\) that denotes action \(x := y + 5\), with \(\eta\) being a valuation of both \(x\) and \(y\), such that \(\eta(x) = 17 \land \eta(y) = -2\), then:

\begin{align*} \texttt{Effect}(\alpha, \eta)(x) &= \eta(y) + 5 = -2 + 5 = 3 \\ \texttt{Effect}(\alpha, \eta)(y) &= \eta(y) + 5 = -2 \end{align*}

Thus, \(\texttt{Effect}(\alpha, \eta)\) is the evaluation that assigns 3 to x and −2 to y, this means \(l \in \texttt{Loc}\) depends on the current valuation of \(\eta\). Given a transition \(l \xrightarrow{g:a} l^\prime\), a nondeterministic choice is made to satisfy a condition \(g\) in \(\eta\) (\(\eta \models g\)).

The execution of action \(\alpha\) changes the valuation of variables according to \(\texttt{Effect}(\alpha, \cdot)\), thus the systems moves to location \(l^\prime\). If no such transition is possible, the system stops.

• Formal Methods
• Model Checking