Temporal Logic with Past is Exponentially More Succinct

Abstract: The old question whether temporal logic with past-time modalities is exponentially more succinct than pure-future temporal logic has recently been answered positively [LMS02].

What is temporal logic with past?

It is temporal logic where future-time modalities, such as F ("sometimes in the future"), G ("always in the future"), U ("until"), ... are complemented with their past-time 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 past-time 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 linear-time temporal property expressed using past-time 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, mu-calculus+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 counter-free 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₁ <=> F^-1G^-1 p₁) & ... & (p_n <=> F^-1G^-1 p_n)] =>`
		`(p₀ <=> F^-1G^-1 p₀)_}`

have size 2^Ω(n).

Formulas (A_n) state that

all future states that agree with the initial state on propositions p₁, p₂, ..., p_n, also agree on proposition p₀

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₁, p₂, ..., p_n, also agree about proposition p₀.

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₀a₁...a_2ⁿ-1 be a sequence containing exactly one occurence of each element of {0,1}^{(p₁,...,p_n)}. With each subset K of {0,1,...,2ⁿ-1}, we associate the word w_K=b₀b₁...b_2ⁿ-1 such that b_i=a_i if i belongs to K, and b_i=a_i + {p₀} 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ⁿ-th state of π_K and π_K', respectively. If q=q' then we could « plug » the 2ⁿ-th suffix of π_K to the 2ⁿ-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ⁿ-1}, namely 2^2ⁿ. [EVW97]

References

[EVW97]	K. Etessami, M. Vardi, and Th. Wilke. First-Order Logic with Two Variables and Unary Temporal Logic. In Proc. 12th IEEE Symp. Logic in Computer Science (LICS'1997), Warsaw, Poland, June 1997, pages 228-235. 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 409-448. Springer-Verlag, 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 163-173. 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 383-392. IEEE Comp. Soc. Press, 2002. (download this paper)