Automaton-Based Characterisations of Temporal Logics
Timotej Šujan · Digital Repository (National Repository of Grey Literature) · 2025
We characterise the expressive power of temporal logics of the form TL[V], where V is a pseudovariety of finite semigroups. This class includes, as a prominent example, propositional dynamic logic, corresponding to the case where V is the pseudovariety of all finite semigroups. Specifically, we prove a semantic equivalence between TL[V] and a class of finite-state tree automata. These automata operate over infinite trees with unbounded branching and are defined using a monotone transition logic E1[Q], subject to joint discreteness and joint co-discreteness conditions that allow the acceptance parity games of the automaton to be encoded by word languages. The main result establishes that a tree language is definable in TL[V] if and only if it is recognized by an E1-automaton in normal form whose automaton languages, that is, the word languages governing its transitions, are recognized in V; both directions of the equivalence are given by explicit constructions.