AS 93 du RTP 23
|
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