Practical Model Checking of LTL with Past

LTL (Linear Temporal Logic) has become the standard language for linear-time model checking. LTL has only future operators, while it is widely accepted that many specifications are easier, shorter and more intuitive when also past operators are allowed. Moreover, adding past operators does not increase the complexity of LTL model checking, which is still PSPACE-complete. However, model checking past formulae is not very easy in practice, and it is not clear how to efficiently reuse existing model checkers like SPIN. In this paper, we propose a reasonably efficient approach to model (and satisfiability) checking of LTL-with-past formulae in a quasi-separate normal form, which occurs very often in applications.