Algebraic Neighbourhood Logic

Abstract:
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.