Lost in Translation: from Linear Temporal Logic to Büchi Automata

In the automata-theoretic approach to languages, formulas from a domain-specific language (such as regular expressions over finite words or a temporal logic over infinite words) are translated to automata, which come equipped with their own semantics, algebraic properties, and supporting algorithms. In the process of translating from formulas to automata, it is possible to lose track of the algebra that exists in the world of formulas, making it harder to reason about semantics and perform optimizations. Recent work on symbolic derivatives for extended regular expressions shows that it is possible to leverage effective Boolean algebras to represent both infinite spaces of characters as well as transition functions/terms, enabling optimizations that apply simultaneously at the level of formula and automata.

We develop here a framework of transition terms modulo an effective Boolean algebra A that works over 𝜔-languages and over infinite alphabets in an algebraically well-defined and precise manner. Using this framework, we then define symbolic derivatives for linear temporal logic (LTL), and define symbolic alternating Büchi automata, based on a shared semantic representation that makes it simpler to reason about optimizations. We present several new optimizations, including one that allows locally eliminating alternation, which results in non-alternating or even deterministic Büchi automata for some classes of LTL. We believe there is a rich world of LTL rewriting rules for on-the-fly optimization of alternating Büchi automata to be discovered.