Séminaire du 11 octobre 2019

Lieu

LSV , ENS Paris-Saclay, (accès ici). salle Condorcet, 1er étage du bâtiment d'Alembert

Programme

14h00-15h00: Franck Pommereau (IBISC, Évry) collaboration avec Cédric Gaucherel, William Atger, Colin Thomas Formal modelling and analysis of ecosystems

Abstract : Several concepts have recently been proposed to understand long-term ecosystem dynamics. These include basins of attraction expressing resilience and tipping points expressing sharp changes in ecosystem’s behavior, which are increasingly being used in ecology. Yet these temporal features remain difficult to identify and quantify, as models usually focus on part of the ecosystem behaviour only. We propose an original family of models designed to comprehensively characterize ecosystem dynamics over the long term. Such models are based on discrete systems borrowed from theoretical computer sciences. We developed a qualitative model based on Petri nets, made up of a relational graph (interaction network) which was then rigorously handled with transition rules. Unlike traditional models and graph theory approaches, such rules may strongly modify the graph structure (i.e. a dynamical topology). We illustrated such Petri nets in a theoretical ecosystem chosen as an insect (termite) colony to show their added values. This ecosystem, made of abiotic and biotic components and processes, was explored in all its possible trajectories and then analyzed. Several temporal features were easily detected and quantified, such as basins (i.e. strongly connected states), tipping points (critical transitions along trajectories) and various kinds of collapses (functioning systems whose structures were nevertheless frozen). It is expected that Petri nets developed for more realistic ecosystems would provide original insights into their overall behavior.

15h00-15h30 : Samir Tigane (LIP6/LINFI) Reconfiguration in Stochastic Petri nets


Abstract : Although Petri nets (PNs), low- or high-level, are a powerful and expressive tool, they are unable to specify/verify, in a natural way, advanced systems having dynamic structures. Indeed, systems supporting volatile environments, continuous variations, and reconfigurable structures expected to be extremely complex. To overcome this issue, researchers enrich PNs with reconfigurability. Nevertheless, increasing the modeling power of a formalism decreases its decision power. In fact, several properties become undecidable. Therefore, extensions proposed in the literature introducing reconfigurability to PNs try to find a compromise between modeling and verification. From this perspective, we can distinguish three main directions. On one hand, researchers develop pre-processing techniques that encode, unfold or compile graphs and transformation rules into existing formalisms in order to exploit the panoply of their tools. Although they can model the reconfigurations in a natural way, these approaches did not increase the modeling power, since they depend on target formalisms expressiveness and in particular do not allow to model infinite graphs. On the other hand, some techniques execute graph transformation systems and compute directly the reachability graph, nevertheless an upper artificial threshold is still needed. Other approaches offer mechanisms that preserve particular properties of PNs after each reconfiguration. These properties are therefor decidable regardless of the number of obtained configurations, i.e., the modeled systems can be structurally unbounded. In this thesis, we extend generalized stochastic Petri nets to a reconfigurable formalism, while maintaining verifiability with reduced complexity. The proposed approach identifies a set of properties that are preserved after each reconfiguration. Hence, these properties are decidable with reduced time and space complexity. As well, we define an algorithm that transforms a reconfigurable GSPN to an equivalent basic GSPN, if the former is structurally bounded. This transformation allows to verify reconfigurable GSPN properties using existing approaches applied to its equivalent GSPN.

15h30-16h00: pause café

16h00-16h30: vie du groupe