non-ZenoAndAcceptingLocation

PATTERN系列的番外篇
对non-Zeno的概念进行了明晰

accepting：if infinitely often the same state

non-Zeno：if time diverges，which means (sum_{igeq20})(delta_{i}) ( ightarrow infin)

Abstract zone graphs again：

​ Extra(^{+}_{LU})

​ ( earrow) ( warrow)

​ Extra(^{+}_{M}) Extra(_{LU})

​ ( warrow) ( earrow)

​ Extra(_{M})

ZG^a(( mathcal{A} )) ：((q_0)(,) (Z_0))( ightarrow)((q_1)(,) (Z_1))( ightarrow) ((q_2)(,) (Z_2))( ightarrow)(cdots)

​ (mathcal{A})：((q_0)(,) (v_0))( ightarrow) ((q_1)(,) (v_1))( ightarrow) ((q_2)(,) (v_2))( ightarrow)(cdots)

（All the above abstractions preserve repeated state reachability）

其中(mathcal{A})中的每一个状态都是ZG^a(( mathcal{A} )) 中相应状态的元素，即 (forall igeq0) 有(v_i) (in) (Z_i)

Time progress criterion： (igwedge_{x in X})unbounded((x))(vee)fluctuating((x))

non-Zenoness： the time progress criterion is not sound on zones

note: Adding one clock leads to an exponential blowup in the zone graph!

​ exponential blowup：指数爆炸