What is temporal logic with past?
It is temporal logic where futuretime modalities, such as
F ("sometimes in the future"),
G ("always in the future"),
U ("until"), ...
are complemented with their pasttime counterparts
(P or F^{1} for "once in the past",
H or G^{1} for "always in the past",
S or U^{1} for "since", ...).

Is it useful?
Yes. Indeed, specifications expressed in natural language often use references to events
that occured in the past.
One finds it natural to express
that "every request is eventually granted" by
(1) 
G(request => F grant)

Thus we woud like to express that "every grant is preceeded by
a request" by the formula
(2) 
G(grant => F^{1} request)


Is it really useful?
It is possible to express the property of formula (2) without pasttime modalities, and write
(3) 
¬((¬ request) U (grant ∧ ¬ request))

Formula (3) only uses future modalities, and is equivalent to formula (2) when interpreted
at the beginning of a path.
This is a general pattern.
Gabbay [GPSS80,Gab87]
proved that any lineartime temporal property expressed using
pasttime modalities can be
translated into an equivalent (when evaluated at the beginning of the path) pure future formula.
In other words, LTL+Past is not more expressive than LTL. This result extends to other temporal logics,
such as CTL^{*}+Past, mucalculus+Past, ...

The succinctness conjecture.
However, it is not known if LTL+Past formulas have succinct LTL equivalents.
Gabbay's translation algorithm yields a formula whose size is assumed
to be non elementary in the size of the initial formula.
Another algorithm is possible, with a detour through counterfree Büchi automata,
giving an elementary (triple exponential) translation.
Since [GPSS80], no lower bound on the size of the
pure future equivalent formula was known. Some kind of succinctness gap was conjectured, though.
[LMS02, section 3]
proves that this conjecture holds.
Namely, we have the following theorem:
Theorem:
LTL formulas equivalent to the following LTL+Past formulas:
(A_{n}) 
G_{{}[(p_{1} <=>
F^{1}G^{1} p_{1}) & ... & (p_{n} <=>
F^{1}G^{1} p_{n})] =>

 
(p_{0} <=> F^{1}G^{1}
p_{0})_{}} 
have size 2^{Ω(n)}.


Formulas (A_{n}) state that
all future states that agree with the initial
state on propositions p_{1}, p_{2}, ..., p_{n},
also agree on proposition p_{0}

The theorem expresses that there is an exponentiel succinctness gap between LTL+Past and LTL.

The proof
Let A_{n} be the above PLTL formula, and B_{n} be a pure future equivalent formula.
Since B_{n} only deals with future states, the formula G B_{n}
expresses that
any two future states that agree
about propositions p_{1}, p_{2}, ..., p_{n},
also agree about proposition p_{0}.

But any LTL (or PLTL) formula expressing that property necessarily has size at least
2^{Ω(n)}.
Indeed, we know that any PLTL formula B_{n} can be translated into an equivalent Buchi
automaton whose size is at most exponential in the size of B_{n}.
Let a_{0}a_{1}...a_{2n1} be a sequence containing exactly one
occurence of each element of {0,1}^{(p1,...,pn)}. With each subset
K of {0,1,...,2^{n}1}, we associate the word
w_{K}=b_{0}b_{1}...b_{2n1} such that
b_{i}=a_{i} if i belongs to K, and
b_{i}=a_{i} + {p_{0}} otherwise.
Given two distinct subsets K and K',
w_{K}^{ω}
and
w_{K'}^{ω}
should be
accepted by the Buchi automaton, but
w_{K'}w_{K}^{ω} should not
since K and K' are distinct.
Let π_{K} be a path accepting w_{K}^{ω},
and π_{K'} be a path accepting w_{K'}^{ω}.
Let q and q' be the 2^{n}th state of π_{K}
and
π_{K'}, respectively. If q=q' then we could « plug » the
2^{n}th suffix of π_{K} to the 2^{n}th
prefix of π_{K'}, and get an accepting path for
w_{K'}w_{K}^{ω}.
Thus, there are at least as many states as words w_{K}, thus as many states as
subsets of {0,1,...,2^{n}1}, namely 2^{2n}.
[EVW97]

References
[EVW97] 
K. Etessami, M. Vardi, and Th. Wilke.
FirstOrder Logic with Two Variables and Unary Temporal Logic.
In Proc. 12th IEEE Symp. Logic in Computer Science (LICS'1997),
Warsaw, Poland, June 1997, pages 228235. IEEE Comp. Soc. Press, 1997.

[Gab87] 
D. Gabbay.
The Declarative Past and Imperative Future: Executable Temporal Logic for Interactive Systems.
In Proc. 1st Conf. on Temporal Logic in Specification (TLS'1987),
Altrincham, UK, April 1987, volume 398 of Lecture Notes in Computer Science,
pages 409448. SpringerVerlag, 1987.

[GPSS80] 
D. Gabbay, A. Pnueli, S. Shelah, and J. Stavi.
On the Temporal Analysis of Fairness.
In Proc. 7th ACM Symp. on Principles of Programming Languages (POPL'1980)
Las Vegas, Nevada, January 1980, pages 163173. ACM Press, 1980.

[LMS02] 
F. Laroussinie, N. Markey, and Ph. Schnoebelen.
Temporal logic with forgettable past.
In Proc. 17th IEEE Symp. Logic in Computer Science (LICS'2002),
Copenhagen, Denmark, July 2002, pages 383392. IEEE Comp. Soc. Press, 2002.
(download this paper)

