Fixing Zeno Gaps

in: Universität Augsburg Technical Report, Institute of Computer Science, University of Augsburg, October 2010

Abstract:
In computer science fixpoints play a crucial role. Most often least and greatest fixpoints are sufficient. However there are situations where other ones are needed. In this paper we study, on an algebraic base, a special fixpoint of the function f(x) = ax that describes infinite iteration of an element $a$. We show that the greatest fixpoint 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 fixpoint that captures these phenomena in a precise way. The theory is presented and motivated using an example from hybrid system analysis. 

Downloads:

• tr2010-11  -  (tr2010-11.pdf, 0 KB)