
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\).
Specification and verification (program logics, model checking, etc.), rational language, Computer Networks and Communications, Applied Mathematics, formal language, syntactic semigroup, Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.), Formal languages and automata, Automata and formal grammars in connection with logical questions, propositional linear temporal logic, Theoretical Computer Science, Computational Theory and Mathematics, linear logic, restriction of temporal logic, Modal logic (including the logic of norms), deterministic automaton
Specification and verification (program logics, model checking, etc.), rational language, Computer Networks and Communications, Applied Mathematics, formal language, syntactic semigroup, Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.), Formal languages and automata, Automata and formal grammars in connection with logical questions, propositional linear temporal logic, Theoretical Computer Science, Computational Theory and Mathematics, linear logic, restriction of temporal logic, Modal logic (including the logic of norms), deterministic automaton
| citations This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 58 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Top 10% | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Top 10% | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
