Technical Report, Institute of Computer Science, University of Augsburg, November 2005
In 1996 Zhou and Hansen proposed a first-order interval logic called Neighbourhood Logic
for specifying liveness and fairness of computing systems and also defining notions of real analysis in
terms of expanding modalities. After that, Roy and Zhou presented a sound and relatively complete
Duration Calculus as an extension of NL.
We present an embedding of NL into an idempotent semiring of intervals. This embedding allows us
to extend NL from single intervals to sets of intervals as well as to extend the approach to arbitrary
idempotent semirings. We show that most of the required properties follow directly from Galois
connections, hence we get the properties for free. As one important result we get that some of the
axioms which were postulated for NL can be dropped since they are theorems in our generalisation.
Furthermore, we present some possible interpretations for neighbours beyond intervals.
Here we discuss for example reachability in graphs and applications to hybrid systems.
At the end of the paper we add finite and infinite iteration to NL and extend idempotent semirigs to
Kleene algebras and omega algebras. These extensions are useful for formulating
repetitive properties and procedures like loops.