The Community for Technology Leaders
2010 17th International Symposium on Temporal Representation and Reasoning (TIME 2010) (2010)
Paris
Sept. 6, 2010 to Sept. 8, 2010
ISSN: 1530-1311
ISBN: 978-1-4244-8014-2
pp: 3-5
ABSTRACT
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 !-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.
INDEX TERMS
formal languages, formal verification, temporal logic
CITATION

M. Leucker and C. Sanchez, "Regular Linear-Time Temporal Logic," 2010 17th International Symposium on Temporal Representation and Reasoning (TIME 2010)(TIME), Paris, 2010, pp. 3-5.
doi:10.1109/TIME.2010.29
94 ms
(Ver 3.3 (11022016))