AS 93 du RTP 23

Département STIC


Automates, modèles distribués et temporisés

Responsable : Pascal Weil (LaBRI)

Démarrage : octobre 2002

Présentation      Membres    Réunion du 7-8 novembre 2002 (LaBRI)
Réunion du 10-11 mars 2003 (VERIMAG)


Membres

Participent à cette AS des membres des laboratoires LaBRI, LIAFA, LSV et VERIMAG.

Les listes qui suivent ne sont pas à prendre en un sens strict : elles contiennent implicitement les doctorants et jeunes docteurs associés aux personnes mentionnées, et les réunions de l'AS sont ouvertes à tous ceux qu'intéressent ses thématiques.

LaBRI : A. Arnold, J-M. Couvreur (en délégation CNRS au LSV, 2002-03), C. Dima, D. Janin, I. Walukiewicz, P. Weil

LIAFA : A. Bouajjani, P. Gastin, A. Muscholl, J.-E. Pin, M. Zeitoun, W. Zielonka

LSV :  B. Bérard, P. Bouyer, F. Laroussinie, A. Petit

VERIMAG : E. Asarin, O. Maler, S. Tripakis


Présentation

    La notion d'automate fini, introduite il y a maintenant près de 50 ans pour modéliser des comportements séquentiels, a donné lieu à une théorie, constamment développée, qui a atteint un haut degré de sophistication mathématique, et dont les applications sont innombrables en informatique, tant théorique que pratique – au point qu'on a pu comparer son statut à celui de l'algèbre linéaire en mathématiques.
    Au cœur de cette théorie, on trouve l'équivalence idéale, selon laquelle les langages (de mots finis) reconnus par un automate fini sont exactement ceux qui sont algébriquement reconnaissables, resp.  définissables en logique monadique du second ordre, exprimables par une expression rationnelle éventuellement étendue.
    Ces équivalences, c'est-à-dire la possibilité d'envisager les mêmes objets sous des formes différentes et facilement compréhensibles, entre lesquelles on peut passer de façon effective et souvent efficace, forment le socle sur lequel s'appuient de nombreuses applications concrètes : en algorithmique des textes (recherche de motifs, compression, etc), vérification, compilation, systèmes à événements discrets, bio-informatique (traitement des séquences génomiques), etc.

    Néanmoins, l'ensemble de ces résultats ne vaut que pour les mots, c'est-à-dire les séquences de symboles non temporisées.  Les dernières années ont vu la multiplication de propositions d'extensions des notions d'automate ou de reconnaissabilité pour traiter (modéliser, concevoir, analyser, valider) des structures plus riches.  Nous souhaitons nous concentrer sur deux de ces types de structures, dont l'importance en informatique n'est plus à démontrer : la représentation de comportements distribués, et celle de comportements temporisés.
    On trouve dans la littérature de nombreux modèles pour représenter ces comportements, et quelques très beaux théorèmes fondamentaux (comme le théorème de Zielonka).  Mais le socle théorique manque, et la littérature fourmille de démonstrations dans des cadres variés de fragments des équivalences vraies dans le cas des mots.  Certains des modèles utilisés (comportements, automates, formalisme logique, etc) sont à l'évidence très riches (en théorèmes) ou très parlants (donc utilisables par des usagers de la théorie des automates), d'autres sont sans doute promis à une vie plus courte.
Modèles : quelques mots clés --- langages d'ensembles partiellement ordonnés, langages de MSC, langages de traces, langages temporisés, langages de données, langages de signaux temporisés, etc.

Outils : quelques mots clés --- réseaux de Petri, automates branchants, automates temporisés, HMSC, automates à passage de messages, jeux, mu-calcul, logiques branchantes, logiques modales, logique monadique du second ordre, trace logics, etc.
    L'objectif que se proposent les participants de cette AS est, sur la base de ces constatations, de faire en un an un état des lieux des résultats partiels obtenus jusqu'à présent, puis de dégager des classes de modèles vraiment fondamentales, et de tracer quelques voies pour le futur.
    Le terme fondamental est sans doute vague, mais nous essaierons, plus concrètement, de repérer les extensions qui sont des variantes ou des cas particuliers les unes des autres, et de circonscrire celles qui possèdent à la fois de bonnes propriétés fondamentales (algébriques, combinatoires, logiques) et de bonnes propriétés d'ordre pratique (expressivité, simplicité de la représentation, efficacité des algorithmes d'analyse, etc).
    Un autre critère, encore peu exploré dans la littérature, sera le suivant.  La théorie des automates sur les mots finis a été beaucoup utilisée pour la classification effective des langages rationnels.  L'archétype en est la caractérisation des langages sans étoile (restriction sur le type d'expression rationnelle étendue) par l'apériodicité du monoïde syntaxique, par la définissabilité par une formule du premier ordre et par la définissabilité en logique temporelle.  Ainsi, pour décider si le langage accepté par un automate donné peut être décrit par une formule de la logique temporelle, on ne connaît pas d'autre méthode que de calculer, sous une forme ou sous une autre, le monoïde syntaxique de ce langage et d'en tester l'apériodicité ; c'est-à-dire que l'on se sert, pour cette procédure de décision, de toute la chaîne d'équivalences susdite.  Ce raffinement des notions de reconnaissabilité et de rationalité a été encore peu exploré dans le domaine des langages distribués ou temporisés, mais il constitue un bon test de robustesse des notions proposées.
    Cependant, ce genre de résultat est certainement difficile à obtenir, notamment parce qu'il suppose une bonne connaissance combinatoire et algébrique des modèles de comportements distribués ou temporisés, pour lesquelles les définitions fondamentales n'ont peut-être pas encore été dégagées.

    Notre objectif s'inscrit donc au sein de l'informatique théorique. En même temps, la multiplication de modèles évoquée répond à un besoin grandissant, de la recherche universitaire comme de la R&D des entreprises, de disposer d'outils formels adaptés aux nouvelles conditions d'exercice de l'industrie du logiciel, qui font nécessairement appel aujourd'hui à des modèles distribués et/ou temporisés.  Ainsi, nous apportons notre contribution – une clarification et un approfondissement des fondements mathématiques — à un effort de recherche qui dépasse largement le cadre de l'informatique théorique.


Pascal Weil