Fixing Zeno Gaps
P. Höfner, B. Möller
In computer science ﬁxpoints play a crucial role. Most often least and greatest ﬁxpoints are suﬃcient. However there are situations where other ones are needed. In this paper we study, on an algebraic base, a special ﬁxpoint of the function f (x) = a · x that describes inﬁnite iteration of an element a. We show that the greatest ﬁxpoint is too imprecise. Special problems arise if the iterated element contains the possibility of stepping on the spot (e.g. skip in a programming language) or if it allows Zeno behaviour. We present a construction for a ﬁxpoint that captures these phenomena in a precise way. The theory is presented and motivated using an example from hybrid system analysis.