# 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. 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

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.

### Un exemple

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 Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « http://localhost:6011/fr.wikipedia.org/v1/ » :): {\displaystyle s} indique que l'horloge Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « http://localhost:6011/fr.wikipedia.org/v1/ » :): {\displaystyle y} peut valoir au plus 5. Quand elle est au moins égale à 3, la transition vers l'état Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « http://localhost:6011/fr.wikipedia.org/v1/ » :): {\displaystyle t} peut être effectuée. Cette transition entraîne que la réinitialisation de l’horloge Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « http://localhost:6011/fr.wikipedia.org/v1/ » :): {\displaystyle y} , i.e. l'horloge Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « http://localhost:6011/fr.wikipedia.org/v1/ » :): {\displaystyle y} est remise à zéro.
L'invariant de l'état Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « http://localhost:6011/fr.wikipedia.org/v1/ » :): {\displaystyle t} porte sur les deux horloges : Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « http://localhost:6011/fr.wikipedia.org/v1/ » :): {\displaystyle x} doit être au plus 8 et Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « http://localhost:6011/fr.wikipedia.org/v1/ » :): {\displaystyle y} au plus 10. La transition vers l'état Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « http://localhost:6011/fr.wikipedia.org/v1/ » :): {\displaystyle s} est possible quand Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « http://localhost:6011/fr.wikipedia.org/v1/ » :): {\displaystyle x} est plus grand que 6 et Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « http://localhost:6011/fr.wikipedia.org/v1/ » :): {\displaystyle y} plus grand que 4, et entraîne que la réinitialisation de 'horloge Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « http://localhost:6011/fr.wikipedia.org/v1/ » :): {\displaystyle 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 :
    Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « http://localhost:6011/fr.wikipedia.org/v1/ » :): {\displaystyle (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 Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « http://localhost:6011/fr.wikipedia.org/v1/ » :): {\displaystyle x} et la troisième coordonnée, celle de l'horloge Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « http://localhost:6011/fr.wikipedia.org/v1/ » :): {\displaystyle y} .
On voit aussi l'écriture plus ramassée
    Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « http://localhost:6011/fr.wikipedia.org/v1/ » :): {\displaystyle (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
    Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « http://localhost:6011/fr.wikipedia.org/v1/ » :): {\displaystyle (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 Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « http://localhost:6011/fr.wikipedia.org/v1/ » :): {\displaystyle x} a atteint 8, qui est la valeur maximale autorisée par l'invariant de l'état Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « http://localhost:6011/fr.wikipedia.org/v1/ » :): {\displaystyle t} , et d'autre part la garde de la transition de Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « http://localhost:6011/fr.wikipedia.org/v1/ » :): {\displaystyle t} vers Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « http://localhost:6011/fr.wikipedia.org/v1/ » :): {\displaystyle s} , qui demande Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « http://localhost:6011/fr.wikipedia.org/v1/ » :): {\displaystyle y\ge4} , n'est pas vérifiée puisque Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « http://localhost:6011/fr.wikipedia.org/v1/ » :): {\displaystyle y} vaut 3.

## Définition formelle

Formellement, un automate temporisé Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « http://localhost:6011/fr.wikipedia.org/v1/ » :): {\displaystyle \mathcal{A}=(Q, \Sigma, C, E, q_0, F)} est composé des éléments suivants :
* Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « http://localhost:6011/fr.wikipedia.org/v1/ » :): {\displaystyle Q}  : un ensemble fini, dont les éléments sont appelés les états, les nœuds ou les places ;
* Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « http://localhost:6011/fr.wikipedia.org/v1/ » :): {\displaystyle \Sigma}  : un ensemble fini appelé l'alphabet ou ensemble d'actions ;
* Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « http://localhost:6011/fr.wikipedia.org/v1/ » :): {\displaystyle C}  : un ensemble fini, aussi noté Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « http://localhost:6011/fr.wikipedia.org/v1/ » :): {\displaystyle X} , dont les éléments sont appelés les horloges ;
* Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « http://localhost:6011/fr.wikipedia.org/v1/ » :): {\displaystyle E\subset Q\times\Sigma\times \mathbb{B}(C)\times \mathfrak{P(C)}\times Q}  : un ensemble de transitions ; ici :
** Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « http://localhost:6011/fr.wikipedia.org/v1/ » :): {\displaystyle \mathbb{B}(C)} est l'ensemble des contraintes booléennes des horloges de Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « http://localhost:6011/fr.wikipedia.org/v1/ » :): {\displaystyle C} ,
** Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « http://localhost:6011/fr.wikipedia.org/v1/ » :): {\displaystyle \mathfrak{P}(C)} est l'ensemble des parties Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « http://localhost:6011/fr.wikipedia.org/v1/ » :): {\displaystyle C}  ;
* Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « http://localhost:6011/fr.wikipedia.org/v1/ » :): {\displaystyle q_0}  : un élément de Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « http://localhost:6011/fr.wikipedia.org/v1/ » :): {\displaystyle Q} appelé l'état initial. On autorise parfois un ensemble d'états initiaux Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « http://localhost:6011/fr.wikipedia.org/v1/ » :): {\displaystyle Q_0\subset Q}  ;
* Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « http://localhost:6011/fr.wikipedia.org/v1/ » :): {\displaystyle F}  : une partie de Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « http://localhost:6011/fr.wikipedia.org/v1/ » :): {\displaystyle Q} dont les éléments sont appelés les états finals.
Un élément Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « http://localhost:6011/fr.wikipedia.org/v1/ » :): {\displaystyle (q,a,g,r,q')} de Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « http://localhost:6011/fr.wikipedia.org/v1/ » :): {\displaystyle E} est une transition de l'état Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « http://localhost:6011/fr.wikipedia.org/v1/ » :): {\displaystyle q} à l'état Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « http://localhost:6011/fr.wikipedia.org/v1/ » :): {\displaystyle q'} avec l'action Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « http://localhost:6011/fr.wikipedia.org/v1/ » :): {\displaystyle a} , la garde Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « http://localhost:6011/fr.wikipedia.org/v1/ » :): {\displaystyle g} et les horloges de Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « http://localhost:6011/fr.wikipedia.org/v1/ » :): {\displaystyle 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 Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « http://localhost:6011/fr.wikipedia.org/v1/ » :): {\displaystyle x<c} ,Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « http://localhost:6011/fr.wikipedia.org/v1/ » :): {\displaystyle x\le c} , Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « http://localhost:6011/fr.wikipedia.org/v1/ » :): {\displaystyle x>c} ou Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « http://localhost:6011/fr.wikipedia.org/v1/ » :): {\displaystyle x\ge c} , où Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « http://localhost:6011/fr.wikipedia.org/v1/ » :): {\displaystyle x} est une horloge et Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « http://localhost:6011/fr.wikipedia.org/v1/ » :): {\displaystyle c} est une constante rationnelle. Un ensemble de contraintes est une conjonction d'un ensemble fini de contraintes.

## Propriétés

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. Le problème de l'accessibilité est décidable pour les automates temporisés. 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.

## Implémentation

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

Les automates temporisées ont été étendues avec des coûts. 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.