I will talk about regular linear temporal logic (RLTL), a logic that generalizes linear temporal logic with the ability to use regular expressions arbitrarily as sub-expressions.

The main result about RLT is that 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 w-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 mu-Calculus, RLTL does not depend on fix-points in its syntax.

I will try to follow a very “pedagogic” style, elaborating on the concepts of verification, linear temporal logic, PSPACE complexity, verification, etc… as much as demanded. No previous knowledge on these topics beyond the basic level of theoretical computer science is assumed.

This is joint work with Martin Leucker, from T.U. Munich.