Résumé
Cette thèse présente des méthodes formelles pour la modélisation d'écosystèmes et l'analyse des graphes état-transition résultants à l'aide de model-checking. Tout d'abord, nous introduisons le concept de graphe état-transition d'écosystème qui, bien qu'étant nouveau, capture une longue histoire de représentations disparates de la dynamique d'écosystèmes sous forme de graphes. Ensuite, nous proposons une méthode d'analyse basée sur le partitionnement des états grâce au model-checking, qui résulte en une représentation hybride explicite/symbolique appelée graphe de composantes. Cette méthodologie est implémentée dans ecco, une boite à outil développée en Python pour la modélisation et l'analyse formelle d'écosystèmes. Cette approche est illustrée par deux études de cas: les changements de végétation de la région du Borana en Éthiopie, et l'assemblage de communautés de protistes. Ces deux études de cas sont limitées par le fait que l'on voudrait que certains événements, par exemple des changements de scénarios de gestion ou des invasions d'espèces, ne se produisent que d'une manière contrôlée. Cette limitation peut être surmontée grâce à ARCTL, une extension de CTL qui permet de restreindre les actions autorisées au cours de la formule. Nous étendons ARCTL avec la notion d'équité, ce qui résulte en FARCTL, et nous fournissons un algorithme symbolique pour le model-checking de FARCTL qui est implémenté dans ecco. Enfin, nous appliquons FARCTL aux deux études de cas, pour examiner les conséquences des changements de scénarios de gestions, et les conséquences d'invasions d'espèces.