Algebraic Neighbourhood Logic
P. Höfner, B. Möller
We present an algebraic embedding of Neighbourhood Logic (NL) into the framework of semirings which yields various
simplifications. For example, some of the NL axioms can be dropped, since they are theorems in our framework, and Galois
connections produce properties for free. A further simplification is achieved, since the semiring methods used are easy and fairly
standard. Moreover, this embedding allows us to reuse knowledge from Neighbourhood Logic in other areas of Computer Science.
Since in its original axiomatisation the logic cannot handle intervals of infinite length and therefore not fully model and specify
reactive and hybrid systems, using lazy semirings we introduce an extension of NL to intervals of finite and infinite length.
Furthermore, we discuss connections between the (extended) logic and other application areas, like Allen’s thirteen relations
between intervals, the branching time temporal logic CTL* and hybrid systems.