Cheap and Secure Web Hosting Provider : See Now

[Answers] Description and semantics of program graphs

, , No Comments
Problem Detail: 

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:

enter image description here

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.

Asked By : eyes enberg

Answered By : User


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


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 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).

Best Answer from StackOverflow

Question Source :

3.2K people like this

 Download Related Notes/Documents


Post a Comment

Let us know your responses and feedback