Une Technique de Validation de Protocoles basée sur une Exploration avec Retour arrière des Automates Complexes.