2
$\begingroup$

As the above question says.

I'm wondering if a transition system is the same as a program graph or they are two different things?

Thank you.

$\endgroup$

closed as unclear what you're asking by Luke Mathieson, D.W., Juho, David Richerby, Rick Decker Jan 12 '15 at 16:50

Please clarify your specific problem or add additional details to highlight exactly what you need. As it's currently written, it’s hard to tell exactly what you're asking. See the How to Ask page for help clarifying this question. If this question can be reworded to fit the rules in the help center, please edit the question.

  • 1
    $\begingroup$ Where have you looked to understand this? The answer is, it depends, but in general they are different. This should be described in many resources on software model checking. What resources have you looked at? $\endgroup$ – D.W. Jan 7 '15 at 1:31
  • $\begingroup$ @D.W. Thanks for replying, i have looked at the book "Principles of Model Checking" by Christel Baier and Joost-Pieter Katoen (The MIT Press). $\endgroup$ – Deyaa Jan 7 '15 at 11:57
3
$\begingroup$

You did not provide any particular resources for neither transition system nor program graph. My answer below is based on the book "Principles of Model Checking" by Christel Baier and Joost-Pieter Katoen (The MIT Press).

For completeness, I first present the definitions of both transition system and program graph in this book. (Keep the numbering of the definitions in the book.)

Definition of transition system:

Definition 2.1 (Transition System $TS$)

A transition system $TS$ is a tuple $(S, Act, \to, I, AP, L)$ where

  • $S$ is a set of states,
  • $Act$ is a set of actions,
  • $\to \subseteq S \times Act \times S$ is a transition relation,
  • $I \subseteq S$ is a set of initial states,
  • $AP$ is a set of atomic propositions, and
  • $L : S \to 2^{AP}$ is a labeling function.

Definition of program graph:

Definition 2.13. (Program Graph $PG$)

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

  • $Loc$ is a set of locations and $Act$ is a set of actions,
  • $Effect : Act \times Eval(Var) \to Eval(Var)$ is the effect function,
  • $\hookrightarrow \subseteq Loc \times Cond(Var) \times Act \times Loc$ is the conditional transition relation,
  • $Loc0 \subseteq Loc$ is a set of initial locations,
  • $g_0 \in Cond(Var)$ is the initial condition.

First of all, the program graph consisting of locations as nodes and conditional transitions as edges is not a transition system, since the edges are provided with conditions.

However, each program graph can be interpreted as a transition system. Particular, the underlying transition system of a program graph results from unfolding: a state of the transition system is composed of a location $l$ of the program graph and an evaluation $\eta$ of the variables. Formally,

Definition 2.15. Transition System Semantics of a Program Graph

The transition system $TS(PG)$ of program graph $PG = (Loc, Act, Effect, \hookrightarrow, Loc_0, g_0)$ over set $Var$ of variables is the tuple $(S, Act, \to, I, AP, L)$ where

  • $S = Loc \times Eval(Var)$
  • $\to \subseteq S \times Act \times S$ is defined by the rule $$\frac{l \hookrightarrow^{g:\alpha} l' \land \eta \models g}{\langle l, \eta \rangle \to^{\alpha} \langle l', Effect(\alpha, \eta) \rangle}$$
  • $I = \{ \langle l, \eta \rangle \mid l \in Loc_0, \eta \models g_0 \}$
  • $AP = Loc \cup Cond(Var)$
  • $L (\langle l, \eta \rangle ) = \{ l \} \cup \{ g \in Cond(Var) \mid \eta \models g \}$.
$\endgroup$
  • $\begingroup$ Thanks for replying i appreciate it. So, Is the product of two transition system going to be the same as doing the product between a program graph and a transition system? $\endgroup$ – Deyaa Jan 7 '15 at 11:59
  • $\begingroup$ @Deyaa Based on the definitions in the "POMC" book, I am not aware of how to do product between a program graph and a transition system directly. However, product (or called interleaving) of two program graphs is stated in Definition 2.21 (Page 40). $\endgroup$ – hengxin Jan 7 '15 at 12:19
  • $\begingroup$ I also saw these definitions in the book but what wasn't clear to me is how you actually construct the T.S. from the program graph - do you have to execute all paths of the program graph (computationally expensive even for finite state systems, impossible for infinite state) to construct the T.S.? Or are there other ways e.g doing some kind of symbolic execution using SAT/SMT solvers? $\endgroup$ – S.N. Sep 20 at 17:54

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