Regular Linear Temporal Logic with Past
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.
To appear In the Eleventh International Conference on
Verification, Model Checking, and Abstract Interpretation (VMCAI'10),
Lecture Notes of Computer Science. Springer-Verlag, 2010.
