Extension de la logique temporelle lineaire aux operations unitaires: Caracterisation algebrique (French text)

The framework of this study is to be located in what is referred to as “the extension of the first-order logic to group operators.” This type of extension arose due to problems related to the weaknesses of the power of expressiveness of the first-order logic. It also emerged in semantics of programming languages. In the latter case, the extension of the first-order propositional logic to the fixed point operators is usually known under the name of μ-calculus.; In our survey we are interested in a linear propositional temporal logic extended to operators able to express the regular group languages properties. These operators are interpreted by a well chosen “unitary” grammar, which gives place to the uPTL acronym allotted to the temporal logic thus obtained. Contrary to the combinatorics-oriented character of most previous work in this direction, we carry out our reasoning from the algebraic point of view underlain by the theory of Krohn-Rhodes.; Under mild technical hypotheses on classes of formulas, we prove that the tight relationship, already known in the context of the standard linear temporal logic, between the substitution and the semidirect product of finite semigroups is preserved. We are then able to define a hierarchy of temporal formulae given by the nesting depth of the new operators. From then on, we establish a one-to-one correspondence between the uPTL formulae hierarchy and the Krohn-Rhodes's hierarchy.; Finally, we reveal a significant fragment of uPTL where the new operators behave exactly like counters modulo an integer n. It is about the modular temporal logic (PTL+MOD). We prove that a language is expressible in PTL+MOD if and only if it is regular and its syntactic monoid is solvable, i.e., contains no nonsolvable group. Hence, expressibility of a language in PTL+MOD is decidable. Moreover, a tight correspondence exists between alternations of abelian groups and aperiodic semi-groups in Krohn-Rhodes's Decomposition Theorem on the one hand, and the nesting of “modular” operators within levels of the usual past temporal logic on the other.