Practical Model Checking of LTL with Past