Méthode formelle de commande sous contraintes de temps dans les dioïdes

Nous considérons dans ce papier, une classe de graphes d'événements temporisés contrôlés soumis à des contraintes temporelles. Ces graphes sont déterministes, dans le sens où leur comportement dépend seulement de leur marquage initial et des entrées de commande qu'on leur a appliquées. Le comportement de ces graphes peut être modélisé par des équations aux différences qui sont linéaires dans l'algèbre Min-Plus. Les contraintes temporelles sont traduites par des inéquations, qui sont également linéaires dans l'algèbre Min-Plus. Nous proposons alors une méthode pour la synthèse de commande qui garantit le respect des contraintes temporelles. Nous explicitons une loi de commande, qui, si deux conditions sont satisfaites, assure la validité des contraintes temporelles. La commande est un retour d'état causal impliquant des retards. La méthode est illustrée sur un exemple réel de processus de production.