Transition Systems
From Termination-Portal.org
Jump to navigationJump to search
Semantics
We define a (global) transition relation <math>\mathit{next}</math> as follows: <math>
\begin{array}[t]{@{}l@{}} ((x \cdot \mathit{xs}), (y \cdot \mathit{ys})) \in \mathit{next} \text{ iff } \\[\jot] \qquad\qquad \exists p \in \mathit{Proc} : \begin{array}[t]{@{}r@{}l@{}} &\mathit{step}_p(x, y) \land \mathit{xs} = \mathit{ys} \\[\jot] \mathrel{\lor}& \exists q \in \mathit{Proc}: \begin{array}[t]{@{}r@{}l@{}} &\mathit{call}^p_q(x, y) \land (x \cdot \mathit{xs}) = \mathit{ys} \\[\jot] \mathrel{\lor} &\mathit{return}^p_q(x, z, y) \land \mathit{xs} = (z \cdot \mathit{ys}) \end{array} \end{array} \end{array}
</math>