prove nontermination 08

无近似，用约束求解方法进行recurrence set的显式综合

1. 提出了recurrence set的概念，证明程序非终止当且仅当有recurrence set.
2. 用synthesis的方法为 lasso 形、确定型的线性程序找recurrence set，实现于工具TNT中。其中用到了 Farkas’ Lemma 进行量词消去：

假设程序stem部分的变迁关系是ρ，loop部分的循环头是Px⩽g，循环体是x’=U x+u。要求解的RS表示为G(x)=Tx⩽t，则recurrence set的条件1表示为$\exists x,\exists x^{\prime },\rho (x,x^{\prime })\wedge T{x}^{\prime }⩽t$，条件2表示为如下的约束:

$\forall x,\exists x^{\prime },Tx⩽t\to Px⩽g\wedge x^{\prime }=Ux+u\wedge T{x}^{\prime }⩽t\Rightarrow$

$$\forall x,Tx⩽t\to Px⩽g\wedge T(Ux+u)⩽t\Rightarrow$$ $$\exists \Lambda ⩾0,\Lambda T=\left(\begin{array}{c}PTU\end{array}\right)\wedge \Lambda t⩽\left(\begin{array}{c}gt-Tu\end{array}\right)$$

参数T和t是recurrence set的template参数，大小可以迭代地调整。比如，约束不满足的情况下，可以添加更多的参数尝试求解。