Efficient Regular Linear Temporal Logic Using Dualization and Stratification

Abstract

We study efficient translations of Regular Linear Temporal Logic (RLTL) into automata on infinite words. RLTL is a temporal logic that fuses Linear Temporal Logic (LTL) with regular expressions, extending its expressive power to all w-regular languages. The first contribution of this paper is a novel bottom up translation from RLTL into alternating parity automata of linear size that requires only colors 0, 1 and 2. Moreover, the resulting automata enjoy the stratified internal structure of hesitant automata. Our translation is defined inductively for every operator, and does not require an upfront transformation of the expression into a normal form. Our construction builds at every step two automata: one equivalent to the formula and another to its complement. Inspired by this construction, our second contribution is to extend RLTL with new operators, including universal sequential composition, that enrich the logic with duality laws and negation normal forms. The third contribution is a ranking translation of the resulting alternating automata into non-deterministic Buchi automata. To provide this efficient translation we introduce the notion of stratified rankings, and show how the translation is optimal for the LTL fragment of the logic.