On the expressive power of temporal logic (Q2366686)

The expressive powers of propositional linear temporal logic (PTL) and of a restriction of temporal logic (RTL), obtained by considering only the operators ``next'' and ``eventually'', are studied. Temporal logics are interpreted on finite words, i.e., a temporal logic formula defines a set of words and the problem is to determine which formal language can be specified in this way. The transparent proof of the fact that a formal language is expressible in PTL if and only if its syntactic semigroup is finite and aperiodic is presented. This gives an effective algorithm to decide whether a given rational language is expressible. The main result of the paper states a similar condition for RTL. A language is RTL expressible if and only if its syntactic semigroup is finite and it satisfies a certain simple algebraic condition. This leads to a polynomial algorithm to check whether the formal language accepted by an \(n\)-state deterministic automaton is RTL-expressible. Also, another (non- effective) description of RTL-definable languages is given: these form the smallest Boolean algebra of formal languages containing the language \(aA^*\) and closed under the operations \(L\to aL\) and \(L\to A^* L\) for every letter \(a\).