Factorisation de Syst`emes 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 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 Sistema Dinamico finito a tempo Discreto (SDD) è costituito da un insieme finito X, chiamato insieme degli stati, e da una funzione f che associa a uno stato v lo stato f(v). I SDD sono uno modello formale per rappresentare fenomeni che compaiono in Fisica, Matematica, Biologia e, naturalmente, in Informatica. Sebbene la formalizzazione matematica e i risultati ottenuti fino ad oggi siano eleganti e significativi, spesso non sono molto adatti nella pratica a causa del loro elevato costo computazionale. In letteratura è noto che i SDD, dotati di opportune operazioni di somma e prodotto, formano un semianello commutativo. Questa struttura algebrica permette di scrivere equazioni polinomiali in cui i coefficienti e le incognite sono SDD. In particolare, se siamo interessati a una dinamica derivata da dati sperimentali, possiamo scrivere un'equazione con la dinamica come termine destro costante e le ipotesi sulla funzione f (o sulle sue proprietà) in un termine polinomiale a sinistra. La ricerca di soluzioni a questa equazione permette di comprendere meglio il fenomeno e le sue proprietà. Questo approccio è interessante, ma presenta importanti limitazioni dal punto di vista computazionale. La soluzione di un'equazione polinomiale (con diverse variabili) è, in generale, indecidibile e, anche se ci concentriamo sul caso della validazione delle ipotesi, il costo computazionale rimane elevato. L'idea è quindi quella di cercare approssimazioni che diano informazioni rilevanti sulle soluzioni dell'equazione originale. È possibile introdurre tre astrazioni (equazioni più semplici) per identificare: il numero di stati delle variabili, il comportamento asintotico o il comportamento transitorio (ciò che accade prima che il sistema si stabilizzi). Ognuna di esse è costruita da un punto di vista teorico e algoritmico per introdurre un metodo per eseguire la validazione delle ipotesi sui SDD. In questa tesi si dimostra che, attraverso trasformazioni algebriche, è possibile enumerare le soluzioni di un'equazione polinomiale con un termine costante enumerando le soluzioni di un numero finito di equazioni più semplici. Infine, viene esplorata la connessione tra queste equazioni semplici e il problema della cancellazione (noto nella teoria dei grafi). Inoltre, questo permette di trovare un limite superiore lineare al numero di soluzioni.