Bounded Verification of Past LTL