Semiring Neighbours: An Algebraic Embedding and Extension of Neighbourhood Logic

In J. Romijn, G. Smith, J. van de Pol (eds.): IFM 2005 Doctoral Symposium on Integrated Formal Methods (IFM 2005).
CS-Report 05-29, pp. 6-13, 2005.

Abstract:
In 1996 Zhou and Hansen proposed a first-order interval logic called Neighbourhood Logic (NL) 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 them 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. At the end of the paper we shortly present some possible applications for neighbours beyond intervals. Here we discuss for example reachability in graphs and applications for hybrid systems.

The CS-Report can be found at technical university of Eindhoven.