Factorisation de systèmes dynamiques discrets

A Finite Discrete-time Dynamical System (DDS) consists of a finite set X , called state space, and a function f, called next-state map (which associates to a state v the state f(v)). DDS are a formal tool for modelling phenomena that appear in Physics, Mathematics, Biology, and, of course, in Computer Science. While the mathematical formalisation and the results that have been found up to nowadays are elegant and meaningful, often they are not very suitable in practice because of their high computational cost. In the literature, it is known that DDS equipped with appropriate sum and product operations form a commutative semiring. This algebraic structure allows us to write polynomial equations in which the coefficients and unknowns are DDS. In particular, if we are interested in some dynamics derived from experimental data, we can write an equation with this as a constant right-hand term and model assumptions about the function f (or its properties) in a polynomial left-hand term. Finding solutions to this equation allow us to better understand the phenomenon and its properties. This approach is interesting but it has important limitations from a computational point of view. Solving a polynomial equation (with several variables) is, in general, undecidable, and even if we focus on the case of hypothesis validation, the computational cost remains high. The idea is then to look for approximations that give relevant information about the solutions of the original equation. It is possible to introduce three abstractions (simpler equations) to identify: the number of states of the variables, the asymptotic behaviour, or the transient behaviour (what happens before the system stabilises). Each one is built from a theoretical and algorithmic point of view to introduce a method to perform hypothesis validation on DDS. In this thesis, it is shown that through algebraic transformations, it is possible to enumerate the solutions of a polynomial equation with a constant term by enumerating a finite number of simpler equations. Finally, the connection between the solution of these simple equations and the cancellation problem known in graph theory is explored. This allowed us to find a linear upper bound on the number of solutions.Un Système Dynamique Fini à temps Discret (SDD) est constitué d'un ensemble fini X, dit espace des états, et d'une fonction f, dite fonction de mise à jour (associant à un état v l'état f(v)). Les SDD sont un outil formel pour modéliser de nombreux phénomènes en physique, en mathématique, en biologie, et, bien sûr en informatique. Si la formalisation mathématique et les résultats qui en découlent sont élégants et parlants, souvent, ces résultats sont peu applicables en pratique à cause de leur coût computationnel élevé. Dans la littérature, il est connu que les SDD équipés d'opérations de somme et de produit appropriées forment un semi-anneau commutatif. Cette structure algébrique nous permet d'écrire des équations polynomiales dans lesquelles les coefficients et les inconnues sont des SDD. En particulier, si nous sommes intéressés par une certaine dynamique dérivée de données expérimentales, nous pouvons écrire une équation avec celle-ci comme terme de droite constant et modéliser des hypothèses sur la fonction f (ou ses propriétés) dans un terme de gauche polynomial. Trouver des solutions à cette équation permet de mieux comprendre le phénomène et ses propriétés. Cette approche est intéressante mais pose des limites computationnelles importantes. En effet, résoudre une équation polynomiale (à plusieurs variables) est, en général, indécidable et même en se concentrant sur le cas de la validation des hypothèses, le coût computationnel reste élevé. L'idée est alors de chercher des approximations donnant des informations pertinentes sur les solutions de l'équation originale. Trois abstractions (équations plus simples) sont introduites afin d'identifier : le nombre d'états des variables, le comportement asymptotique ou le comportement transient (comportement avant que le système se stabilise). Chaque abstraction est construite d'un point de vue théorique et algorithmique dans le but d'introduire une méthode pour effectuer la validation d'hypothèses sur SDD. Dans cette thèse, il est montré qu'au moyen de transformations algébriques, il est possible d'énumérer les solutions d'une équation polynomiale avec un terme droit constant par l'énumération d'un nombre fini d'équations plus simples. Enfin, le lien entre la résolution ces équations simples et le problème de la cancellation connu en théorie des graphes est exploré. Cela a permis de trouver une borne supérieure linéaire sur le nombre de solutions