An Adequate First Order Interval Logic

The paper uses left and right neighbourhoods as primitive interval modalities to define other unary and binary modalities of intervals in a first order logic with interval length. A complete first order logic for the neighbourhood modalities is presented. The paper demonstrates how the logic can support formal specification and verification of liveness and fairness, and also of various notions of real analysis. 1 Introduction Interval temporal logics, based on ITL [11], have shown to be useful for the specification and verification of safety properties of real-time systems. In these logics one can succinctly express properties like: "for all intervals of a given size, OE must hold", and "if OE holds for an interval, then there is a subinterval where / holds", and so on. However, these logics cannot express more abstract liveness properties like "eventually there is an interval where OE holds" and "OE will hold infinitely often in the future". The reason for this limitation is that the..