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 des interprétations synchrones et asynchrones de ces logiques, interprétées sur des réseaux d'automates étendus qui effectuent des mouvements synchrone ou synchrone via des actions jointes. Plusieurs séquences d'information sont considérées : imparfaite (i) et parfaite (I), et révélée : imparfaite (r) et parfaite (R).