Démonstration automatique en logique temporelle : application aux contraintes d'intégrité dynamiques
Institution:
Paris 11Disciplines:
Directors:
Abstract EN:
THE FIRST PART OF THIS WORK IS THE STUDY OF LINEAR TEMPORAL LOGIC OVER FINITE TINE FRAMES (LTL_fin ). WE SHOW THAT THE VALIDITY PROBLEM FOR SUCH A LOGIC IS NOT RECURSIVELY ENUMERABLE. THE PROOF IS A REDUCTION OF THE CO-HALTING PROBLEM OF TURING MACHINES TO THE VALIDITY PROBLEM OF LTL_fin FORMULAS. WE INTRODUCE THE NOTION OF BOUNDED VALIDITY, THE K-VALIDITY. A FORMULA IS DEFINED TO BE K-VALID IF IT IS TRUE IN ALL TEMPORAL MODELS WHOSE UNDERLYING TIME FRAME IS BOUNDED BY K. WE DEFINE A TABLEAU CALCULUS FOR LTL_fin. THIS CALCULUS IS SOUND WITH RESPECT TO STANDARD VALIDITY BUT EVIDENTLY NOT COMPLETE. HOWEVER, OUR SYSTEM IS SOUND AND COMPLETE WITH RESPECT TO BOUNDED VALIDITY. IN THE SECOND PART, WE ADDRESS THE PROBLEM OF STATICALLY PROVING, AT COMPILATION TIME, WHETHER THE EXECUTION OF A GIVEN UPDATE M IS SAFE WITH RESPECT TO A DYNAMICAL INTEGRITY CONSTRAINT IN THE FRAMEWORK OF OBJECT ORIENTED DATABASE SYSTEMS. TO DO SO, WE FORMALIZE THE DATABASE AND THE DYNAMICAL CONSTRAINTS IN FIRST ORDER LINEAR TEMPORAL LOGIC AND WE USE TWO PREDICATE TRANSFORMER "LA DIJKSTRA", COMBINED WITH THE TABLEAU CALCULUS WE DEFINED IN THE FIRST PART.
Abstract FR:
La première partie de ce travail consiste en l'étude de la logique temporelle linéaire du premier ordre avec temps fini (ltl_fin ). Nous montrons que le problème de la validité des formules de ltl_fin n'est pas semi décidable. La preuve est faite par réduction du problème du non arrêt des machines de turing au problème de la validité des formules de ltl_fin. Nous introduisons alors la notion de validité bornée, la k-validité, qui permet d'affirmer qu'une formule est vraie sur toutes les interprétations ayant un cadre temporel fini. Par la suite, nous présentons un système de preuve par tableaux pour ltl_fin. Notre système est correct pour la validité standard mais bien sur incomplet. Par contre, il correct et complet par rapport à la k-validité. Dans la deuxième partie, nous étudions le problème de vérifier statiquement, à la compilation, si l'exécution d'une mise à jour donnée m préserve une contrainte dintégrité dynamique donnée c, dans le contexte d'une base de données orientées objets. à cette fin, nous formalisons la base de données et les contraintes dynamiques en logique temporelle linéaire du premier ordre avec temps fini (ltl_fin ) et nous utilisons deux "transformateurs de prédicats" à la dijkstra, combinés avec le système de preuve par tableaux que nous avons défini dans la première partie.