3
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ What book/other source is the question from? $\endgroup$ – User Apr 8 '15 at 18:55
  • $\begingroup$ The question is from an assignment I had in December (which I didn't score very well on). The exam is in 3 weeks so I'm making sure I can answer all of the questions comfortably. The book we use for this module is Principles of Model Checking by Joost-Pieter Katoen and some other dude. $\endgroup$ – eyes enberg Apr 8 '15 at 19:24
  • $\begingroup$ I really do not hope Christel Baier is a dude :) $\endgroup$ – User Apr 8 '15 at 19:26
  • 2
    $\begingroup$ Lol my bad, I naturally assume any author that's related to computer science is a guy. $\endgroup$ – eyes enberg Apr 8 '15 at 19:32
  • $\begingroup$ @eyesenberg, it's understandable; many people do. However, assumptions like that have some unfortunate effects -- they they can affect female computer scientists and ultimately our entire field. Not trying to call you out, just using this as an opportunity to remind us all of the downsides of stereotypes and reflect on how we as a community can act to counter them. $\endgroup$ – D.W. Apr 9 '15 at 16:07
3
$\begingroup$

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

$\endgroup$
  • $\begingroup$ Perfect, thanks a lot. Would I be right in saying that $k_1 a_1 k_2 b_1 k_3 k_1$ is an execution of $PG_1$? Not quite sure what a trace is and how it's different to an execution. $\endgroup$ – eyes enberg Apr 8 '15 at 20:23
  • $\begingroup$ Take a look at page 34 in the book. It provides the semantics for a given program graph in terms of a transition system $(S, Act, \rightarrow, I, AP, L)$. A state in S is on the form $s = (l, \eta)$ where $l \in Loc$ and $\eta \in Eval(Var)$. Use this together with the transition rule and the labelling function $L$ to create executions. $\endgroup$ – User Apr 8 '15 at 20:29
  • $\begingroup$ very useful, cheers. $\endgroup$ – eyes enberg Apr 9 '15 at 10:14

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.