Fixing Zeno gaps (Q549197): Difference between revisions

From the text: ``We study, on an algebraic base, a special fixpoint of the function \(f(x)=_{df} a\cdot x\) that describes infinite iteration of an element \(a\). Here, \(a\) abstractly stands for a set of transitions which may be discrete or continuous, and \(\cdot\) denotes sequential composition. Frequently, the least fixpoint of \(f\) is the element \(0\) that represents the empty behaviour and hence is uninteresting. Therefore the greatest fixpoint \(a^\omega\) of \(f\) was studied. However, in may cases \(a^\omega\) is too large and imprecise, admitting behaviour that is not wanted. For instance, if the iterated element \(a\) contains the possibility of stepping on the spot (e.g. \texttt{skip} in a programming language), then \(a^\omega\) coincides with the greatest element \(\top\) of the underlying lattice, which represents the completely unrestricted behaviour that sometimes is called \texttt{chaos}. ``Stepping on the spot is a special case of \textit{Zeno} behaviour in which an infinite number of sufficiently short transitions add up to a finite overall duration. This, at least conceptually, may for instance occur in hybrid systems, that is, in heterogeneous systems characterised by the interaction of discrete and continuous dynamics. The investigations of the present paper originate in an algebraic setting for describing hybrid systems [the first author, Algebraic calculi for hybrid systems. Norderstedt: Books on Demand GmbH (2009)] and [the authors, J. Log. Algebr. Program. 78, No. 2, 74--97 (2009; Zbl 1161.68032)]. As special cases of that model, streams [...] and omega-regular expressions occur. It turns out that in the case of Zeno behaviour, the description using the greatest fixpoint \(a^\omega\) for describing infinite iteration is again way too imprecise, since it allows arbitrary behaviour `after' a Zeno effect, whereas actually nothing should be observable any more after such an occurrence. Therefore a fixpoint between the two extremes -- the least and the greatest fixpoint -- is interesting and useful. The present paper is about such a more precise fixpoint. To the best of our knowledge, such a fixpoint has not been studied by other authors. We have introduced this fixpoint already in [the authors, loc. cit.], however, by a very concrete definition that does not lend itself easily to proofs of further properties of the operator and is not in a form that can be tackled in a general, more abstract algebraic setting. An improved presentation was given in the dissertation [the first author, loc. cit.]. This is the basis for the treatment here, which eventually leads to an abstract algebraic axiomatisaton.''