-Modèles discrets -Modèles temporisés, paramètrés et à coût -Verification, Synthèse de paramètres, Synthèses de stratégies