Describir: Especificación, verificación y cálculo de estrategias en juegos no cooperativos usando verificación de modelos