nontermination overapproximation

基于上近似，进行closed recurrence set的显式综合的nontermination analysis

在Disproving termination with overapproximation中, live abstraction被用于和closed recurrence set一起证明程序的非终止性。文章证明，如果在上近似P’中找到closed recurrence set G’，且原程序存在一个初始状态 $s_{0}$ ，满足 $A F (s_{0}) \in G^{'}$ 且 $A F (s_{0})$ 是抽象域中的初始状态，则原程序P也存在closed recurrence set，即 $G = {s ∣ \exists a . G^{'} (a) \land A F (s) = a}$ 。G隐含了recurrent set，从而证明非终止性。