Definition of "Zeno"

It is therefore important to be able to determine if a model is Zeno and in applicable cases remove Zenoness.

2000, J. Zhang et al., “Dynamical Systems Revisted: Hybrid Systems with Zeno Executions”, in Hybrid Systems: Computation and Control, page 458

While this system is not Zeno, it can nevertheless not be considered implementable; thus, the boundedness of activity seems to be a more appropriate abstract concept of implementability of a system with respect to the amount of activity in finite intervals of time.

2005, Heinrich Rust, “Chapter 3”, in Operational Semantics for Timed Systems: A Non-standard Approach to Uniform Modeling of Timed and Hybrid Systems, page 17

That is, it is necessary to check whether a run is Zeno so as to avoid presenting Zeno runs as counterexamples.

2013, Y. Si et al., “Improving Model Checking Stateful Timed CSP with non-Zenoness through Clock-Symmetry Reduction”, in Formal Methods and Software Engineering : 15th International Conference on Formal Engineering Methods, ICFEM 2013, page 183