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:

(An) G{[(p1 <=> F-1G-1 p1) & ... & (pn <=> F-1G-1 pn)] =>        
(p0 <=> F-1G-1 p0)}

have size 2Ω(n).

Formulas (An) state that

all future states that agree with the initial state on propositions p1, p2, ..., pn, also agree on proposition p0
The theorem expresses that there is an exponentiel succinctness gap between LTL+Past and LTL.

The proof

Let An be the above PLTL formula, and Bn be a pure future equivalent formula. Since Bn only deals with future states, the formula G Bn expresses that
any two future states that agree about propositions p1, p2, ..., pn, also agree about proposition p0.
But any LTL (or PLTL) formula expressing that property necessarily has size at least 2Ω(n).

Indeed, we know that any PLTL formula Bn can be translated into an equivalent Buchi automaton whose size is at most exponential in the size of Bn. Let a0a1...a2n-1 be a sequence containing exactly one occurence of each element of {0,1}(p1,...,pn). With each subset K of {0,1,...,2n-1}, we associate the word wK=b0b1...b2n-1 such that bi=ai if i belongs to K, and bi=ai + {p0} otherwise.

Given two distinct subsets K and K', wKω and wK'ω should be accepted by the Buchi automaton, but wK'wKω should not since K and K' are distinct. Let πK be a path accepting wKω, and πK' be a path accepting wK'ω. Let q and q' be the 2n-th state of πK and πK', respectively. If q=q' then we could « plug » the 2n-th suffix of πK to the 2n-th prefix of πK', and get an accepting path for wK'wKω. Thus, there are at least as many states as words wK, thus as many states as subsets of {0,1,...,2n-1}, namely 22n.  [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)

About LSV