Résumé : On étudie le pouvoir d'expression de
la logique temporelle propositionnelle interprétée sur les
mots finis. Nous donnons une preuve transparente du fait qu'un langage
formel est expressible dans cette logique si et seulement si son semigroupe
syntactique est fini et apériodique. Ceci donne un algorithme
effectif pour décider si un langage rationnel donné est
expressible dans cette logique. Notre résultat principal donne une
condition similaire pour la logique temporelle "restreinte" (RTL), obtenue
en laissant de côté l'opérateur Until. Un langage est
exprimable dans la logique RTL si et seulement si son semigroupe
syntactique est fini et vérifie une certaine condition
algébrique simple. Ceci conduit à un algorithme polynomial
pour tester si le langage accepté par un automate fini à
n états est expressible en logique RTL.
Abstract : We study the expressive power of linear propositional
temporal logic interpreted on finite sequences or words. We first give a
transparent proof of the fact that a formal language is expressible in this
logic if and only if its syntactic semigroup is finite and aperiodic. This
gives an effective algorithm to decide whether a given rational language is
expressible. Our main result states a similar condition for the
"restricted" temporal logic (RTL), obtained by discarding the until
operator. A formal language is RTL-expressible if and only if its syntactic
semigroup is finite and satisfies a certain simple algebraic condition.
This leads to a polynomial time algorithm to check whether the formal
language accepted by an n-state deterministic automaton is
RTL-expressible.