Modeling and verification analysis of ecological systems via a first order logic approach

This paper addresses the modeling and verification analysis of the mutual relationships among plants, animals, and their environment. We start our study of mathematical ecology by considering the interaction of two species, one of which the predators eat the preys thereby affecting each other, such pairs exist throughout nature: fish and sharks, lions and gazelles, birds and insects, to mention some. Not all species form predator-prey relationships, we can also have the case of a two-species ecosystem in which both species compete for the same limited source of nutrients. If two competitors try to occupy the same realized niche, one species will try to eliminate the other. Therefore, two instances are worth to be considered. On the one hand, there is a need to cooperate sharing part of the resource so that both organisms will benefit from it. On the other hand, if one of the two species is stronger than the other, there will be no cooperation and the strongest species will impose its conditions. In this work, the ecological interaction system between species is modeled as a formula of the first order logic. Then, using the concept of logic implication, and transforming this logical implication relation into a set of clauses, called Skolem standard form, qualitative methods for verification as well as performance issues, for some queries, are applied.