Programme

Les automates temporisés représentent un formalisme puissant, permettant de spécifier et vérifier des systèmes concurrents soumis à des contraintes temporelles. Situés à la frontière de la décidabilité et de l'indécidabilité, ils peuvent être utilisés comme formalisme de spécification pour effectuer du model checking à l'aide de logiques temporelles temporisées, et ainsi déterminer si un système satisfait une propriété donnée. Les automates temporisés paramétrés permettent d'augmenter l'expressivité des automates temporisés en s'attaquant à un problème plus complexe : déterminer pour quelles valeurs des constantes temporelles (dans le modèle et/ou la propriété) le système satisfait une propriété donnée. Cette forte expressivité s'obtient au détriment de la décidabilité, mais les automates temporisés paramétrés ont néanmoins pu récemment résoudre des problèmes concrets dans le domaine de l'ordonnancement temps-réel.