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. © Springer-Verlag Berlin Heidelberg 2007.
CITATION STYLE
Leucker, M., & Sánchez, C. (2007). Regular linear temporal logic. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4711 LNCS, pp. 291–305). Springer Verlag. https://doi.org/10.1007/978-3-540-75292-9_20
Mendeley helps you to discover research relevant for your work.