is of the form: $$\label{equ:quantum}
\textsc{ while} \quad (\textit{Mea}[\rho]=0)\quad
  \left\{
   \begin{aligned}
   \rho &\coloneqq \mathcal{E}_1(\rho);  \\
   \parallel\quad \rho &\coloneqq \mathcal{E}_2(\rho);  \\
   &\vdots\\
   \parallel\quad \rho &\coloneqq \mathcal{E}_{l-1}(\rho); \\
   \parallel\quad \rho &\coloneqq \mathcal{E}_l(\rho);
    \end{aligned}
   \right\}.$$ where

1.  $\rho\in\mathbb{C}^{d^2}$ is a $d\times d$ density matrix.

2.  $\textit{Mea}=\{M_0,M_1\}$ is a two-outcome quantum measurement, where $M_0$ and $M_1$ are $d\times d$ complex matrices.

3.  $\mathcal{E}_i$ are quantum super-operators, which are linear transformations over $\mathbb{C}^{d^2}$.

In this example, ${\pmb{x}}=\rho$, $G({\pmb{x}})={\rm tr}(M_0\rho M_0^\dagger)$ and ${\pmb{A}}_i=\mathcal{E}_i$, where ${\rm tr}(M)$ is the trace of a matrix $M$, and $M^\dagger=(M^T)^*$ is the complex conjugate of the transpose of $M$. Clearly, it is a multi-path linear program over $\mathbb{C}^{d^2}$. In [@LY14], the non-terminating inputs of this program plays a key role in deciding the termination of quantum programs.

Execution of MPPs
-----------------

Given an input ${\pmb{x}}$, the behavior of MPP (\[equ:mpp\]) is determined by the choices of ${\pmb{A}}_i\ (1\leq i\leq l)$ nondeterministically, and all the possible executions form a tree.

The execution tree of MPP (\[equ:mpp\]) for an input ${\pmb{x}}\in {\mathbb{K}}^d$ is defined inductively as follows:

1.  the root is the input value of ${\pmb{x}}$;

2.  for any node $ \widetilde{{\pmb{x}}}$, it is a leaf node if $ G(\widetilde{{\pmb{x}}})\neq 0$; otherwise, $\widetilde{{\pmb{x}}}$ 