Re: Linear temporal logic with only past

Christophe Jacquet schrieb:
Hello,

Gabbay has shown that LTL+Past has no increased expressive power over
LTL (i.e. LTL with future operators only). There even seems to be a
translation algorithm from LTL+Past to "future" LTL.

Looks like in peano arithmetic, where you can defined
predecessor, based on successor.

pred(X)=Y :<=> succ(Y)=X

This can be adapted to some modal expressions. Let
F denote one step in the future, P denote one step
in the past. I assume we have then:

B -> F A <=> F (P B -> A)

So you can move out the F operator. In the end
you will go from:

A to F^n A'

For some n. Now if the time is Z (the positive and negative
integers) then:

|- F^n 'A <=> |- 'A

Because |- makes an universal closure I assume.

Easy...

Bye
.