Regular Linear Temporal Logic

We present regular linear temporal logic (RLTL), a logic that generalizes linear temporal logic with the ability to use regular expressions arbitrarily as sub-expressions. Every LTL operator can be defined as a context in regular linear temporal logic. This implies that there is a (linear) translation from LTL to RLTL. Unlike LTL, regular linear temporal logic can define all ω-regular languages, while still keeping the satisfiability problem in PSPACE. Unlike the extended temporal logics ETL∗, RLTL is defined with an algebraic signature. In contrast to the linear time µ-calculus, RLTL does not depend on fix-points in its syntax.

• Type: Conference
• Year: 2007
• Where: ICTAC
• Authors: Martin Leucker, César Sánchez
• Keywords: Extended Temporal Logics, ICTAC 2007, Linear Temporal Logic, Regular Linear