Ce projet définit des extensions de CTL et TCTL avec des opérateurs stratégiques, appelées Strategic CTL (SCTL) et Strategic TCTL (STCTL). Il fournit une sémantique synchrone et asynchrone pour chacune de ces logiques, interprétées sur des réseaux d'automates étendus qui effectuent des mouvements synchrones ou se synchronisent via des actions jointes. Le projet offre également un support pour la vérification de modèles à l'aide de l'outil IMITATOR.