Gabbay's separation theorem

In mathematical logic and computer science, Gabbay's separation theorem states that any formula in linear temporal logic (LTL) with past operators can be rewritten as a boolean combination of formulas that are only concerned with the past, present, or future. This theorem was stated and proven by Dov Gabbay.

Applications

Expressive Completeness

A formula is separated if it is a boolean combination of formulas that are only concerned with the past, present, or future. An arbitrary temporal logic has the separation property if each formula is equivalent to a separated formula. Gabbay shows that a temporal logic that can express the future operator $\mathbf {F}$ and the past operator $\mathbf {P}$ of LTL has the separation property if and only if the logic is expressively complete. Here, a logic is expressively complete if it is expressively equivalent to the monadic first-order logic of order. Separation was first used to prove Kamp's theorem. Before, the only known method to prove expressive completeness was a pure syntactic argument.

An example of a logic without the separation property is LTL restricted to the operators $\mathbf {F}$ and $\mathbf {P}$. The formula $\mathbf {F} (a\land \neg \mathbf {P} \neg b)$ cannot be separated, where $a,b$ are atomic propositions. LTL restricted to the next operator $\mathbf {X}$ and the yesterday operator $\mathbf {Y}$ has the separation property, but is not expressively complete as it cannot express $\mathbf {F}$.

Expressiveness of Past Operators

Gabbay showed that LTL formulas can be separated. When evaluating a formula over the natural numbers at time 0, formulas only concerning the past are trivial as there is no past at time 0. Thus, every LTL formula using past operators has an equivalent form without past operators at time 0. That is, the addition of past operators do not increase the expressive power of LTL. A corollary is that CTL* with past operators has the same expressive power as CTL* over rooted trees. Hodkinson and Reynolds suggest that this is the reason researchers tend to use future-only versions of LTL, CTL, and CTL*. While LTL with past and LTL have the same expressive power, the inclusion of past operators can make formulas exponentially more succinct.

Normal Forms

The separation theorem is used to prove various normal forms for temporal formulas.

Safety-Liveness Form

Lichtenstein et al. gives us the safety-liveness form, where every formula in LTL is equivalent to a formula of the following form, where $a_{i},b_{i}$ are boolean combinations of atomic propositions:

$\bigvee _{i=1}^{n}(\mathbf {G} \mathbf {F} a_{i})\land (\mathbf {F} \mathbf {G} b_{i})$

Separated Normal Form

Fisher gives us the separated normal form, where each formula in LTL can be written in the following form, such that each $P_{i}$ is only concerned with the past, and $F_{i}$ is only concerned with the future:

$\mathbf {G} \left(\bigwedge _{i=1}^{n}P_{i}\to F_{i}\right)$

This form has been used for specifications in executable temporal logic, where $F_{i}$ can be executed when the current history satisfies $P_{i}$. MetateM is an example of a language that uses this paradigm.