Regular Linear-Time Temporal Logic

Martin Leucker and César Sánchez
This extended abstract presents the main ideas behind regular linear-time temporal logic (RLTL), a logic that generalizes linear-time temporal logic (LTL) with the ability to use regular expressions arbitrarily as sub-expressions. Unlike LTL, RLTL can define all omega-regular languages and unlike previous approaches, RLTL is defined with an algebraic signature, does not depend on fix-points in its syntax, and provides past operators 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.
In Proceedings of the 17th International Symposium on Temporal Representation and Reasoning (TIME'10), Paris, France, 6-8 September 2010. pp3-5, IEEE Computer Society, 2010.
Download: BIB PDF