Temporal logic with past is exponentially more succinct, Concurrency Column.
Nicolas Markey · Bulletin of the European Association for Theoretical Computer Science · 2003
We positively answer the old question whether temporal logic with past is more succinct than pure-future temporal logic. Surprisingly, the proof is quite simple and elementary, although the question has been open for twenty years.