live abstraction 一种特定类型的抽象/上近似。满足两个条件： simulation: 在原状态空间可行的转移，在抽象域中同样可行。（上近似的定义） upward termination: 终止的状态，在抽象域中对应的抽象状态同样是终止的。（所谓终止的状态，即在转移关系中没有后继的状态，对应程序的终止）