Bounded Model Checking for past LTL