Separation-Past, Present and Future
Mark A Reynolds, Ian Hodkinson · UWA Profiles and Research Repository (UWA) · 2005
Separation is a remarkable concept, invented by Dov Gabbay in [Gabbay, 1981a], and elaborated in [Gabbay, 1989; Gabbay et al., 1994]. Roughly, a temporal logic has the separation property if its formulas can be equivalently rewritten as a boolean combination of formulas, each of which depends only on the past, present, or future. This seemingly innocent and technical definition has had some far-reaching consequences, and has taken on a life of its own. Surprisingly, separation is closely connected to the important topic of expressive completeness, and is one of the main methods for proving expressive completeness. Separation has applications in executable temporal logic, and parts of this have been implemented. Separation has found recent uses in simplifying normal form theorems and axiomatising Ockhamist branching time logic, and in analysing the W3C language XPath.