Regular Linear Temporal Logic with Past

César Sánchez and Martin Leucker
This paper upgrades Regular Linear Temporal Logic (\RLTL) with past operators and complementation. \RLTL is a temporal logic that extends the expressive power of linear temporal logic (\LTL) to all $\omega$-regular languages. The syntax of \RLTL consists of an algebraic signature from which expressions are built. In particular, \RLTL does not need or expose fix-point binders (like linear time $\mu$-calculus), or automata to build and instantiate operators (like \ETLstar).

Past operators are easily introduced in \RLTL via a single previous-step operator for basic state formulas. The satisfiability and model checking problems for \RLTL are PSPACE-complete, which is optimal for extensions of \LTL. This result is shown using a novel linear size translation of \RLTL expressions into $2$-way alternating parity automata on words.

Unlike previous automata-theoretic approaches to \LTL, this construction is compositional (bottom-up). As alternating parity automata can easily be complemented, the treatment of negation is simple and does not require an upfront transformation of formulas into any normal form.

In Proceedings of the Eleventh International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'10), vol. 5944 of Lecture Notes of Computer Science, pp295-311. Springer-Verlag, 2010.
Download: BIB PDF