Automate temporisé

Un article de Wikipédia, l'encyclopédie libre.
Aller à : navigation, rechercher

En théorie des automates, un automate temporisé est un automate fini doté d'un ensemble fini d'horloges à valeurs réelles. Au cours d'un calcul de l'automate, les valeurs des horloges augmentent toutes à la même vitesse. Dans les transitions de l'automate, les valeurs d'horloges sont comparées à des entiers. Ces comparaisons constituent des gardes qui activent ou inhibent les transitions et imposent ainsi des contraintes aux comportements de l'automate. Les horloges peuvent être réinitialisées. Les automates temporisés ont été introduits par Alur et Dill en 1994[1]. Les auteurs ont reçu, pour cet article, le prix prix Alonzo Church 2016 de l'European Association for Theoretical Computer Science.

Présentation[modifier | modifier le code]

Les automates temporisées peuvent être utilisés pour modéliser et analyser le comportement temporel de systèmes informatiques, par exemple, des systèmes ou des réseaux opérant en temps réel. Des méthodes pour vérifier les propriétés de sûreté et de vivacité ont été développées et étudiées depuis l'introduction des automates temporisées en 1994.

Un automate temporisé accepte des mots temporisés — des suites infinies où une valeur réelle de moment d'occurrence est associé à chaque symbole. On peut définir des classes d'automates temporisés déterministe ou non déterministes, et comparer le conditions d'acceptation de Büchi ou de Muller. Les langages acceptés par des automates temporisés non déterministes sont fermés pour l'union et l'intersection, mais pas par complémentation ; au contraire, les langages acceptés par des automates temporisés de Muller sont fermés pour toutes les opérations booléennes. Il existe un algorithme de complexité PSPACE pour tester si le langage d'un automate temporisé non déterministe est vide. Le problème de l'accessibilité est décidable pour les automates temporisés[1]. Des extensions ont été largement étudiées. Il existe une variété de outils de recherche pour la saisie et l'analyse d'automates temporisés et de leurs extensions, parmi lesquels les model checkers  UPPAAL, Kronos, et l'analyseur d'ordonnancement TIMES.

Description[modifier | modifier le code]

Un automate temporisé possède un nombre fini de places ou états. Les transitions entre états sont instantanées. Dans chaque place, le temps peut s’écouler: à tout instant, la valeur d’une horloge x est le temps écoulé depuis la dernière mise à zéro de x. Les transitions entre états sont conditionnées par des contraintes sur les horloges, appelés gardes, et peuvent remettre certaines horloges à zéro. À chaque place est associée une contrainte sur les horloges, appelée invariant[2].

Un exemple[modifier | modifier le code]

Un automate temporisé[3],[2].

L'automate temporisé ci-contre est composé de deux états et , et de deux transitions étiquetées respectivement par les lettres d'entrée et . L'automate a aussi deux horloges et . L'invariant de l'état indique que l'horloge peut valoir au plus 5. Quand elle est au moins égale à 3, la transition vers l'état peut être effectuée. Cette transition entraîne que l’horloge est remise à zéro.

L'invariant de l'état porte sur les deux horloges : doit être au plus 8 et d'au plus 10. Une transition vers l'état entraîne que l'horloge est mise à zéro.

Une trajectoire est une exécution de l'automate. Un automate peut rester dans un état tant que son invariant est satisfait. Il doit quitter l'état avant que l’invariant soit invalide. Pour franchir une transition, il faut que sa garde soit vraie et que l'invariant de l’état d'arrivé soit valide. Voici un exemple d'exécution, où on a séparé la progression du temps dans un état du franchissement de la transition :

On voit aussi l'écriture plus ramassée

Voici une autre trajectoire

.

Ici, l'exécution est bloquée parce que la garde de la transition n'est pas vérifiée[3].

Définition formelle[modifier | modifier le code]

Formellement, un automate temporisé  est composé des éléments suivants:

  •  : un ensemble fini, dont les éléments sont appelés les états, les nœuds ou les places ;
  •  : un ensemble fini appelé l'alphabet ou ensemble d'actions ;
  •  : un ensemble fini, aussi noté , dont les éléments sont appelés les horloges ;
  •  : un ensemble de transitions ; ici :
    • est l'ensemble des contraintes booléennes des horloges de ,
    • est l'ensemble des parties  ;
  •  : un élément de appelé l'état initial. On autorise parfois un ensemble d'états initiaux  ;
  •  : une partie de dont les éléments sont appelés les état finals[N 1].

Un élément de est une transition de l'état à l'état avec l'action , la garde et les horloges de réinitialisées.

Une horloge est une variable à valeurs réelles positives ou nulles. Une contrainte d'horloge est de l'une des formes ,, ou , où est une horloge et est une constante rationnelle. Un ensemble de contraintes est une conjonction d'un ensemble fini de contraintes.

Notes et références[modifier | modifier le code]

Notes[modifier | modifier le code]

  1. Pluriel conseillé (plutôt que finaux) en cette acception ; voir par exemple le CNRTL [lire en ligne] : « En fait, il y a flottement entre finals et finaux : le 1er semble être le plur. de la lang. cour. et des écrivains, le second celui des linguistes et des économistes ; ex. : des b, d, g finaux, les résultats finaux (cf. Dupré 1972, pp. 1 011-1 012). ».

Références[modifier | modifier le code]

Bibliographie[modifier | modifier le code]

Articles
  • Rajeev Alur et David L. Dill, « A Theory of Timed Automata », Theoretical Computer Science, vol. 126, no 2,‎ (lire en ligne) — Article premier
  • Rajeev Alur, « Timed Automata », dans N. Halbwachs et D. Peled (éditeurs), Computer Aided Verification, 11th International Conference, CAV '99, Proceedings, Springer, coll. « Lecture Notes in Computer Science » (no 1633), (ISBN 3-540-66202-2, lire en ligne), p. 8-22
Cours

Articles liés[modifier | modifier le code]