% TeX root = ../main.tex

\begin{tikzpicture}[program,initial above,font=\scriptsize, 
    every state/.append style={rectangle,rounded corners=10},
    ]
    \node[state,initial]  (l0t)                       {$\langle \ell_0, \texttt{true} \rangle$};
    \node[state]          (l1t) [below=2cm of l0t]    {$\langle \ell_1, \texttt{true} \rangle$};
    \node[state]          (l2t) [below=2cm of l1t]    {$\langle \ell_2, \texttt{true} \rangle$};
    \node[state,grun]          (l1p134) [right=4cm of l1t]    {$\langle \ell_1, \lbrace \psi_1, \psi_3, \psi_4 \rbrace \rangle$};
    \node[state,grun]          (l1p124) [right=4cm of l2t]    {$\langle \ell_1, \lbrace \psi_1, \psi_2, \psi_4 \rbrace \rangle$};

    % Transitions
    \path[->]   
        (l0t) edge[] node (t0) { $t_{0}$ } (l1t)
        (l1t) edge[bend left=20] node (t1) { $t_{2}$ } (l2t)
        (l2t) edge[bend left=20] node (t2) { $t_{3}$ } (l1t)
        (l1t) edge[grun, bend left=10] node (t1a1) { $t_{1a,1}$ } (l1p134)
        (l1t) edge[grun, bend left=10] node[pos=0.35] (t1b1) { $t_{1b,1}$ } (l1p124)
        (l1p134) edge[rot, bend left=10] node[pos=0.65] (t21) { $t_{2,1}$ } (l2t)
        (l1p124) edge[rot, bend left=10] node (t22) { $t_{2,2}$ } (l2t)
        (l1p134) edge[rot,loop above] node (t1a2) { $t_{1a,2}$ } ()
        (l1p124) edge[rot,loop below] node (t1b3) { $t_{1b,3}$ } ()
        (l1p134) edge[rot, bend right=20,transform canvas={xshift=5mm}] node[swap] (t1b2) { $t_{1b,2}$ } (l1p124)
        (l1p124) edge[rot, bend right=20,transform canvas={xshift=5mm}] node[swap] (t1a3) { $t_{1a,3}$ } (l1p134)
        ;

    % General transitions
    \node[] [below right=1cm of l0t] {$G_0$};
    \node[grun] [above left=1cm of l1p134] {$G_1$};
    \node[rot] [below right=2cm of l1p134] {$G_2$};
\end{tikzpicture}