This paper introduces 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. It is demonstrated how the logic can support formal specification and verification of liveness and fairness, and also of various notions of real analysis.
|Title of host publication||Compositionality: The Significant Difference|
|Publication status||Published - 1998|
|Event||Compositionality: The Significant Difference - |
Duration: 1 Jan 1998 → …
|Conference||Compositionality: The Significant Difference|
|Period||01/01/1998 → …|