Description and semantics of program graphs

I'm working on a question which gives me a program graph and tells me to give a mathematical description of it. I'm aware that a program graph PG is a tuple

$(Loc, Act, Effect, \rightarrow, Loc_0, g_0)$

This is the question I'm trying to answer:

So far for $PG_1$ (one of the 2 transition systems) I have:

$Loc = \{k_1, k_2, k_3\},$ with $Loc_0 = \{k_1\}$

$Act = \{\alpha_1, \beta_1, \gamma_1\}$

$Effects = \{Effect(\alpha_1, \eta) = \eta[x := x + 1]$,
$Effect(\beta_1, \eta) = \eta[y := y - 1]$,
$Effect(\gamma_1, \eta = \eta[y := y + 2]\}$

$\rightarrow = \{(k_1, \alpha_1, k_2), (k_2, \beta_1, k_3), (k_3, \gamma_1, k_1)\}$

$g_0 = $ ?

I'm aware that $g_0$ is the starting condition, but I'm not sure what it is in this case? Also for $\rightarrow$ I assumed this was done the same was it is in Transition Systems, if somebody could clarify whether or not this is the correct way to do it I would be really grateful.

Thanks in advance for any help.

Definitions

From "Principle of Model Checking" By Joost-Pieter Katoen and Christel baier:


A program graph over a set Var of typed variables is a tuple $(Loc, Act, >Effect, \rightarrow, Loc_0, g_0)$ where:

• $Loc$ is a set of locations

• $Effect: Act \times Eval(Var) \to Eval(Var)$ is the effect function

• $\rightarrow \subseteq Loc \times Cond(Var) \times Act \times Loc$ is the condition transition relation

• $Loc_0 \subseteq Loc$ is a set of initial locations

• $g_0 \in Cond(Var)$ is the initial condition

It is further noted that:


$Eval(Var)$
denote the set of (variable) evaluations that assign values to variables


$Cond(Var)$ is the
set of Boolean conditions over Var

Given these definitions, your definitions of $Loc$, $Act$ and $Effect$ are correct

Transitions

So, according to these definition the conditional transition relation must be:

$\rightarrow =\{(k1,α1, ? ,k2),(k2,β1, ?, k3),(k3,γ1, ?, k1)\}$

where each questionmark is a tautology, ie something always true (as there are no conditions in the figure). As the authors note,


If the guard is a tautology ... we simply write $(l, \alpha, l') \in \rightarrow$.

So in conclusion your definition of $\rightarrow$ is correct

Furthermore, $Cond(Var)$ must consist of tautologies.

Initial Condition

To me it seems that there are no given initial conditions on the variables $x,y$ so $g_0$ must simply be a tautology as $g_0 \in Cond(Var)$. It seems undefined what specific tautology $g_0$ must be, but any tautology will do, if you apply the Structural Operational Semantics given in the book, as any location satisfies any tautology.

Execution and Traces

Both concepts are defined in the context of Transition Systems.

Executions:


Executions are alternating sequences consisting of states
and actions

And traces:


Thus, rather
than having an execution of the form $s_0
\rightarrow^{a_0} s_1
\rightarrow^{a_1} s2$ . . . we consider sequences of the
form $L(s_0)L(s_1)L(s_2)$ . . . that register the (set of) atomic propositions that are valid along
the execution. Such sequences are called traces.

For reasoning about executions and traces you thus need to look at the transition system induced from the program graph (by the structural operational semantics given in the book).

StackExchange Computer Science Q#41147, answer score: 3