The Transformation Logics
Alessandro Ronca
TL;DR
The Transformation Logics paper introduces a broad framework of temporal logics built around transformation operators, including a flip-flop monoid as a prime building block and finite semigrouplike operators derived from semigroups and finite simple groups. The authors establish a rich expressivity ladder: flip-flop yields star-free languages, augmenting with cyclic solvable groups expands to broader fragments of regular languages, and prime operators eventually capture all regular languages, with formal decompositions inspired by Krohn–Rhodes theory. They also provide substantial complexity results, showing polynomial-time evaluation for finite polytime operators, with precise data- and circuit-class characterizations (AC^0, ACC^0, NC^1) depending on operator families, and they prove Past LTL can be translated into the core logic L(F). Together, these results yield a versatile, AI-relevant temporal-logic toolkit that can be tailored to application-specific expressivity/efficiency needs, while offering a principled algebraic understanding of the trade-offs involved.
Abstract
We introduce a new family of temporal logics designed to finely balance the trade-off between expressivity and complexity. Their key feature is the possibility of defining operators of a new kind that we call transformation operators. Some of them subsume existing temporal operators, while others are entirely novel. Of particular interest are transformation operators based on semigroups. They enable logics to harness the richness of semigroup theory, and we show them to yield logics capable of creating hierarchies of increasing expressivity and complexity which are non-trivial to characterise in existing logics. The result is a genuinely novel and yet unexplored landscape of temporal logics, each of them with the potential of matching the trade-off between expressivity and complexity required by specific applications.