a spécification et la vérification des propriétés des systèmes multi-agents se heurte à des barrières de complexité, voire même d’indécidabilité, car le problème de model-checking pour beaucoup de logiques de stratégies multi-agents est soit indécidable, soit nonélementaire. Les travaux dans ce thème se concentrent en conséquence, d’une part, sur l’identification des fragments de la logique SL qui ont un problème de model-checkign décidable en temps élémentaire, et d’autre part, sur des techniques de réduction de l’espace d’états qui préservent les propriétés stratégiques.