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

Problem Detail: 

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.

Asked By : Deyaa

Answered By : hengxin

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

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/36027