5
$\begingroup$

I would like to ask if anybody is aware of a paper comparing the expressiveness of past time LTL and that of (future time) LTL.

$\endgroup$
  • 2
    $\begingroup$ They are expressively the same, though past operators make LTL exponentially more succinct. You can start here. $\endgroup$ – Shaull Feb 10 '15 at 20:24
  • $\begingroup$ @Shaull: Turn your comment into an answer! $\endgroup$ – cody Feb 11 '15 at 1:17
15
$\begingroup$

The quick summary is that LTL with only past and no future modalities defines properties expressed over finite-words and these are the star-free subset of the regular languages. Standard LTL when extended with past-time modalities does not have more logical expressive power than LTL with only future modalities but properties can be defined in an exponentially succinct manner.

For a more detailed answer, there are at least three logics one can consider in answering your question and at least three different notions of expressiveness.

  1. Standard Linear Temporal Logic (LTL), which has the standard modalities next and until and is interpreted over traces that have a finite history and an infinite future.
  2. Past-time Linear Temporal Logic (ptLTL), which has the modalities "previously" instead of "next" and "since" instead of until and is interpreted over finite traces, or at some point in an infinite trace but refers to the history of the trace.
  3. Temporal logic with past and future modalities (sometimes abbreviated to TL), which has the modalities of LTL and ptLTL and is interpreted either over infinite traces or over finite and infinite traces.

The three notions of expressiveness are to ask (i) what languages (of finite or infinite words) each logic can define, (ii) what first-order structures these logics define, and (iii) what the complexity of defining a given language (or first-order structure) in each logic is. A more refined vocabulary for comparing expressiveness is provided by the notion of hierarchies, which are briefly mentioned at the bottom.

First-Order Structures definable by temporal languages

Kamp in 1968 studied an until modality that is slightly different from the notion commonly used in computer science today. I will write it as $\mathit{Until}_+$ for because a formula $p ~Until_+~ q$ is true at time instant i if $q$ is true at some $j > i$ and if $p$ holds at all $i < j' < j$. Note that the orders are strict. The temporal-dual is the modality $Since_+$. Kamp compared temporal logics to the Monadic First-Order Logic of Order (MLO, sometimes MFLO or FMLO). MLO formulae contain unary predicate symbols and a relation $<$ and are interpreted over linear orders.

Kamp's theorem shows that a logic with only $Until_+$ and $Since_+$ modalities is expressively equivalent to MLO when both logics are interpreted over the naturals or over the non-negative reals. In fact, Kamp's theorem applies to a family of structures called Dedekind-complete chains (which notably does not include the non-negative rationals). Stavi's theorem shows that a temporal logic with standard since and until and a special since and until modality is expressively-equivalent to the first-order monadic logic of order over every linear order. The notion of expressiveness in these results is "definability of first-order structures".

Gabbay, Pnueli, Shelah and Stavi considered a family of MLO formulae called future formulae, which intuitively only refer to future points in time. They showed that on a family of models called discrete, complete orders, which includes the naturals, future MLO formulae have the same expressive power as temporal logic with the $Until_+$ modality, a next and previously modality. So these results relate certain temporal and first-order logics on certain structures.

Relating languages to first-order logic, McNaughton and Papert showed that first-order definable languages are star-free and regular, which in conjunction with Kamp's theorem shows that all the logics above only define subsets of regular languages. Adding the next and previous modalities does not change what you can define and a proof that the third logic above still defines only the star-free regular languages is due to Zuck and Pnueli, I believe.

Comparative expressive power of temporal languages

Kamp was also one of the first to study how the properties one can express changes with the modalities in a temporal logic. He showed that the $Until_+$ modality cannot be expressed in a logic with the Eventually, Next and more modalities. This difference in expressive power led him to study the $Until_+$ and $Since_+$ modalities.

Gabbay, Pnueli, Shelah and Stavi proved what is called a separation theorem. They showed that a formula that involves $Until_+$ and $Since_+$ can be written as a Boolean combination of formulae that involve either only $Until_+$ or only $Since_+$. (The story goes that when Kamp heard of a form of this separation theorem from Gabbay, he went out and bought Gabbay a cake.) This paper and separation result is sometimes cited as the reason for not including past modalities in temporal logics. It follows from their results that for a formula with $Until_+$ and $Since_+$, there exists a formula involving only $Until_+$ such that at time instant $0$, either both are true or both or false. It follows from this result that a temporal logic with the standard $Next$, $Until$, $Since$ and $Prev$ modalities, when interpreted over time indexed by the natural numbers (the standard semantics in computer science) has the same expressive power as LTL with only $Next$ and $Until$.

Unfortunately the only algorithm known to compute the separation above non-elementary complexity. Moreover, not every temporal logic has the separation property. In particular, if you only have an eventually and previously modality, separation does not hold. Lichtenstein, Pnueli and Zuck did show that every formula in LTL with past modalities is equivalent to a formula with the form below.

$\bigvee_1^n (GF~\varphi_i) \land (FG~\psi_i)$, where $\varphi_i$ and $\psi_i$ do not contain standard $Until$ or $X$.

Complexity

In terms of complexity, it is known that temporal logic with past-time modalities is exponentially more succinct than LTL with only future-time modalities. Nonetheless, a result of Sistla and Clarke (1985) shows that the model checking problem for both is in PSpace. The actual complexity issues are a bit more complicated because one can ask for lower-bounds for expressiveness in both logics involved in a comparison. I recommend consulting the references below for more on this.

  1. Vince Bárány's temporal logic course has all the reading material in one place.
  2. Temporal Logic with Past is Exponentially More Succinct, Laroussinie, Markey, and Schnoebelen has recent results on a logic with a now modality and a forgettable notion of past.
  3. The Glory of the Past, by Lichtenstein, Pnueli and Zuck is the definite starting point for reading on complexity differences between LTL with and without past-time modalities.
  4. Lenore Zuck's PhD thesis is a good place to read about background on past and future modalities, in particular Chapters 2 and 3. Chapter 5 has the main results on expressiveness of the logic with past and regular languages.
  5. Propositional temporal logics: decidability and completeness, Lichtenstein and Pnueli, 2000. Studies decidability and completeness of LTL with past and future modalities and has surveys the history of these logics.
  6. Separation - past, present and future, Hodkinson and Reynolds, is a survey of many different logics using the notions of until and since from Kamp, and which discusses these issues from the perspective of the separation theorem.
  7. Expressive Power of Temporal Logics, Rabivonich, 2002 discusses several other notions for comparing expressiveness such as dot-depth, quantifier alternation and basis for a temporal logic.
  8. Efficient Monitoring of Safety Properties, Havelund and Rosu studies an application of ptLTL, and is a place to find a definition of the logic.
  9. The Rise and Fall of LTL by Vardi is a talk that covers most of this and much more from a high level.
  10. Specification in CTL+Past for Verification in CTL, Laroussinie and Schnoebelen, 2000, will answer the questions you haven't yet asked about what happens if you have past-time modalities in a branching-time logic.
$\endgroup$
  • $\begingroup$ Thank you very much. Could you please finish your sentence in number 3: "Chapters 2 and 3. Chapter 5 shows that temporal logic with"... Maybe my English is bad, but I do not understand this sentence. $\endgroup$ – qsp Feb 11 '15 at 19:57
7
$\begingroup$

The logics are expressively the same, though past operators make LTL exponentially more succinct.

You can start here, from which there are references.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.