[Solved]: What is the difference between a Transition System and a Program Graph? (model checking)

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 }$.