Ce projet fournit une sémantique de réécriture logique pour les automates temporels paramétriques avec variables globales (PTAV) et démontre que l'analyse de portée symbolique utilisant Maude-with-SMT est sound et complete pour le problème de portée des automates temporels. La théorie de réécriture peut également être utilisée pour la synthèse de paramètres.