Automate temporisé

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 Alonzo Church 2016 de l'European Association for Theoretical Computer Science.

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.

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]

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

L'invariant de l'état $t$ porte sur les deux horloges : $x$ doit être au plus 8 et $y$ au plus 10. La transition vers l'état $s$ est possible quand $x$ est plus grand que 6 et $y$ plus grand que 4, et entraîne que la réinitialisation de 'horloge $x$ à 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ée 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 :

(s,0,0){\xrightarrow[{3}]{}}(s,3,3){\xrightarrow {a}}(t,3,0){\xrightarrow[{4}]{}}(t,7,4){\xrightarrow {b}}(s,0,4){\xrightarrow[{1}]{}}(s,1,5)\cdots

Dans cette exécution, la première coordonnée est l'état dans lequel se trouve l'automate temporisée, la deuxième coordonnée est la valeur de l'horloge

x

et la troisième coordonnée, celle de l'horloge

y

.

On voit aussi l'écriture plus ramassée

(s,0,0){\xrightarrow[{3}]{a}}(t,3,0){\xrightarrow[{4}]{b}}(s,0,4){\xrightarrow[{1}]{}}(s,1,5)\cdots

Voici une autre trajectoire

(s,0,0){\xrightarrow[{5}]{a}}(t,5,0){\xrightarrow[{3}]{}}(t,8,3)

.

Ici, l'exécution est bloquée parce que, d'une part l'horloge $x$ a atteint 8, qui est la valeur maximale autorisée par l'invariant de l'état $t$ , et d'autre part la garde de la transition de $t$ vers $s$ , qui demande $y\geq 4$ , n'est pas vérifiée puisque $y$ vaut 3^[3].

Définition formelle[modifier | modifier le code]

Formellement, un automate temporisé ${\mathcal {A}}=(Q,\Sigma ,C,E,q_{0},F)$ est composé des éléments suivants :

$Q$ : un ensemble fini, dont les éléments sont appelés les états, les nœuds ou les places ;
$\Sigma$ : un ensemble fini appelé l'alphabet ou ensemble d'actions ;
$C$ : un ensemble fini, aussi noté $X$ , dont les éléments sont appelés les horloges ;
$E\subset Q\times \Sigma \times \mathbb {B} (C)\times {\mathfrak {P(C)}}\times Q$ $E\subset Q\times \Sigma \times \mathbb {B} (C)\times {\mathfrak {P(C)}}\times Q$ : un ensemble de transitions ; ici :
- $\mathbb {B} (C)$ est l'ensemble des contraintes booléennes des horloges de $C$ ,
- ${\mathfrak {P}}(C)$ est l'ensemble des parties $C$ ;
$q_{0}$ : un élément de $Q$ appelé l'état initial. On autorise parfois un ensemble d'états initiaux $Q_{0}\subset Q$ ;
$F$ : une partie de $Q$ dont les éléments sont appelés les états finals^{[N 1]}.

Un élément $(q,a,g,r,q')$ de $E$ est une transition de l'état $q$ à l'état $q'$ avec l'action $a$ , la garde $g$ et les horloges de $r$ réinitialisées.

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

Propriétés[modifier | modifier le code]

On peut définir des classes d'automates temporisés déterministe ou non déterministes, et comparer les 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é pour tester si le langage d'un automate temporisé non déterministe est vide, en espace polynomial. D'ailleurs, ce problème est PSPACE-complet^[1]. Le problème de l'accessibilité est décidable pour les automates temporisés^[1]. Des extensions ont été largement étudiées.

Le problème d'universalité (savoir si tous les mots sont acceptés par un automate temporisé non-déterministe) est indécidable. Il est décidable lorsqu'il n'y a qu'une seule horloge, bien que non primitif récursif^[4].

Implémentation[modifier | modifier le code]

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.

Extensions[modifier | modifier le code]

Les automates temporisées ont été étendues avec des coûts^[5]. On indique dans chaque état, le coût de rester dans cet état par unité de temps ; et pour chaque transition, on indique le coût de prendre cette transition. Ainsi, on peut associer un coût global à une exécution en sommant les coûts des délais dans chaque état et les coûts des transitions prises.

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

Notes[modifier | modifier le code]

↑ 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 1^er 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]

↑ ^{a b et c} Alur et Dill 1994.
↑ ^{a et b} Bournez, « Automates temporisés ».
↑ ^{a et b} Denis, « Introduction aux automates temporisés ».
↑ SƗawomir Lasota et Igor Walukiewicz, « Alternating Timed Automata », ACM Transactions on Computational Logic, vol. 9, n^o 2,‎ 2008, p. 1–26 (DOI 10.1145/1342991.1342994)
↑ (en) Rajeev Alur, Salvatore La Torre et George J. Pappas, « Optimal Paths in Weighted Timed Automata », Hybrid Systems: Computation and Control, Springer Berlin Heidelberg, lecture Notes in Computer Science,‎ 2001, p. 49–62 (ISBN 9783540453512, DOI 10.1007/3-540-45351-2_8, lire en ligne, consulté le 7 juillet 2019)

Bibliographie[modifier | modifier le code]

Articles

Rajeev Alur et David L. Dill, « A Theory of Timed Automata », Theoretical Computer Science, vol. 126, n^o 2,‎ avril 1994, p. 183-235 (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 » (n^o 1633), 1999 (ISBN 3-540-66202-2, lire en ligne), p. 8-22

Cours

Olivier Bournez, « Automates temporisés », Cours du DEA Model Checking, École polytechnique, Paris.
Bruno Denis, « Introduction aux automates temporisés », sur lurpa, ENS Cachan (consulté le 10 octobre 2016).

Articles liés[modifier | modifier le code]

Portail de l'informatique théorique

[4] 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 1^er 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). ».

[AD-1] {a b et c} Alur et Dill 1994.

[OB-2] {a et b} Bournez, « Automates temporisés ».

[BD-3] {a et b} Denis, « Introduction aux automates temporisés ».

[Alternating_timed_automata-5] SƗawomir Lasota et Igor Walukiewicz, « Alternating Timed Automata », ACM Transactions on Computational Logic, vol. 9, n^o 2,‎ 2008, p. 1–26 (DOI 10.1145/1342991.1342994)

[6] (en) Rajeev Alur, Salvatore La Torre et George J. Pappas, « Optimal Paths in Weighted Timed Automata », Hybrid Systems: Computation and Control, Springer Berlin Heidelberg, lecture Notes in Computer Science,‎ 2001, p. 49–62 (ISBN 9783540453512, DOI 10.1007/3-540-45351-2_8, lire en ligne, consulté le 7 juillet 2019)

[1]

[2]

[3]

[N 1]

[4]

[5]

v · m Automates finis et langages réguliers
Articles généraux	Théorie des automates Automate fini Machine abstraite
Automates finis	Automate fini déterministe Automate fini inambigu Automate fini non déterministe Construction par sous-ensembles Automate sur les mots infinis
Automates finis particuliers	Automate alternant Automate bidirectionnel Automate pondéré Automate probabiliste Automate quantique Automate temporisé Automate de Büchi Automate de Muller Modèle de Markov caché Système de transition d'états Structure de Kripke Machine à états abstraits Machine de Mealy Machine de Moore Transducteur fini Automate séquentiel
Langages réguliers	Langage rationnel Langage sans étoile Langage local Langage congruentiel Langage stochastique Lemme de l'étoile Lemme d'Arden ω-langage rationnel
Des automates aux langages	Expression régulière Algorithme de Conway Algorithme de McNaughton et Yamada Méthode de Brzozowski et McCluskey
Des langages aux automates	Dérivée de Brzozowski Algorithme de Thompson Construction de Glushkov Complexité en états
Minimisation	Théorème de Myhill-Nerode Équivalence de Nerode Minimisation d'un automate fini déterministe Algorithme de Moore Algorithme de Brzozowski Algorithme de Hopcroft
Équivalences	Théorème de Kleene Étoile de Kleene Monoïde syntaxique Théorème des variétés d'Eilenberg

v · m Informatique théorique
Codage	Codage de l'information Compression de données Chiffrement Cryptanalyse Cryptographie Théorie de l'information
Modèles de calcul	Calculabilité Décidabilité et indécidabilité Ensemble récursif Problème de l'arrêt Ensemble récursivement énumérable Machine de Turing Thèse de Church Automate cellulaire Réseau de neurones artificiels Réduction polynomiale Problème NP-complet Principe de Church-Turing-Deutsch
Algorithmique	Algorithmique Algorithme glouton Algorithme probabiliste Algorithme génétique Complexité algorithmique Analyse d'algorithme Diviser pour régner Heuristique Programmation dynamique Géométrie algorithmique Algorithmes de tri Algorithmique du texte Exploration de données Science des données Apprentissage profond Test de primalité Structure de données Arbre enraciné Concurrence Parallélisme
Syntaxe	Réécriture Compilation Expression régulière Grammaire formelle Langage rationnel Ensemble rationnel Théorie des langages Théorie des automates Automate fini Automate sur les mots infinis Automate d'arbres Automate à pile Hiérarchie de Chomsky Linguistique informatique
Sémantique	Interprétation abstraite Méthodes formelles Vérification de modèles Sémantique des langages de programmation Sémantique dénotationnelle Sémantique axiomatique Sémantique opérationnelle
Logique mathématique	Assistant de preuve Calcul des prédicats Correspondance de Curry-Howard Fonction récursive Lambda-calcul Théorèmes d'incomplétude de Gödel Théorie des types
Mathématiques discrètes	Combinatoire Algorithme du simplexe Optimisation combinatoire Théorie des graphes Algorithmes de la théorie des graphes Recherche opérationnelle Théorie de la décision Analyse numérique