Un cas remarquable de systèmes linéaires : les systèmes monotones : résolution et application à la vérification formelle de programmes
Institution:
Cachan, Ecole normale supérieureDisciplines:
Directors:
Abstract EN:
"Deciding whether or not a linear system of inequalities has integer solutions is an important sub-problem occurring in many case studies. It is well known that such a question of diophantine nature can be a formidable source of combinatorial difficulties. In this thesis, we focus on a class of integer linear problems than can be solved without enumeration (either directly or iteratively, if the problem is bounded)- their relaxation giving here an exact solution. This "polynomial" class is characterized by a remarkable confluence of syntactic and geometric properties (matrices having at most one postivie entry per now, concording with solutions sets forming a semi-lattice). We show that local consistency techniques based on interval narrowing are complete for that class (when the domains are bounded). This stems from the fact that one particular solution is a global maximum (or minimum). The systems under study encompass questions ranging from the satisfiability problem for Horn propositional clauses to the computation of shortest paths on a graph. By comparatively studying their solution algorithms, we are able to establish connections between the classical procedures of variable elimination and discrete optimization, and the more recent interval (or finite domains) approximation solving techniques. A more elaborate application, requiring the power of contraint logic programming, deals with reachability analysis on discrete state machines. Our implementations, using either the linear solver of Prolog III or the interval solver Prolog IV, enable us to prove several program properties automatically, on examples taken from the field of formal verification. "
Abstract FR:
"Savoir décider si oui ou non un système d'inégalités linéaires admet une solution entière est un sous-problème important dans beaucoup d'études de cas. Il est bien connu que cette question, de nature diophantienne, peut être source de difficultés combinatoires. Nous exhumons, dans ce travail, une classe particulière de problèmes linéaires à variables entières dont la résolution exacte peut s'obtenir sans énumération, à partir d'une relaxation continue (soit directement, soit itérativement sur des problèmes bornés). Cette classe "polynômiale" se caractérise par une concordance remarquable entre des propriétés syntaxiques (matrices ayant au plus un coefficient strictement positif par ligne) et des propriétés géométriques (ensemble des solutions formant un demi-treillis). Nous montrons que les techniques de filtrage opérant localement par réduction d'intervalles sont complètes pour cette classe (lorsque les domaines sont bornés), du fait de l'existance d'une solution particulière qui est un extrêmum global. Les systèmes étudiés recouvrent des problèmes aussi variés que la satisfaction de clauses de Horn en logique propositionnelle ou la recherche de plus courts chemins sur un graphe. En abordant leur résolution de manière comparée, nous établissons des ponts entre les procédures classiques d'élimination de variables et d'optimisation discrète et les techniques plus récentes d'approximation par intervalles. Une application plus élaborée concerne l'analyse, en programmation logique avec contraintes, de l'accessiblité dans des machines à états discrets. Les implantations réalisées avec le solveur linéaire de Prolog II ou le solveur d'intervalles de Prolog IV nous permettent de prouver automatiquement plusieurs propriétés, sur des exemples tirés du domaine de la vérification formelle de programmes"