Récemment, un des nouveaux aspects de la vérification de programmes ou de systèmes est l'étude des causes d'une validation ou d'une falsification d'une propriété logique. Extraire les causes permet d' expliquer à l'utilisateur les contraintes qui jouent dans le résultat/l'évaluation d'un test donné (par exemple Model checking, satisfiabilité), ou plus simplement de trouver la partie du programme qui correspond à une certaine propriété requise par l'utilisateur. Plus généralement, comprendre les causes est aussi très utile pour produire des résolveurs de contraintes efficaces (en logique propositionnelle, SatModuloTheory). De plus, comprendre les causes a été reconnues nécessaires dans les logiques non monotones (par ex. logique défaisable) ou la gestion de bases de connaissances. Enfin, comprendre les causes d'une vérification est la pierre d'échoppe de toute théorie de réutilisation/décomposition de programmes, processus métier ou systèmes de manière à ce que cette décomposition soit faite en fonction des propriétés vérifiées. Comment fournir un programme plus simple si l'utilisateur souhaite uniquement que telle partie du contrat soit vérifiée et plus nécessairement les autres parties du contrat? Ce problème n'est pas si simple car les propriétés peuvent recouvrir une grande partie du programme sans respecter la structure des composants.
Alors que beaucoup de travaux existent dans le cas de la logique propositionnelle, voire aussi dans le cas de Sat Modulo Theory, peu d'études analysent les causes dans les logiques modales comme la logique déontique ou temporelle. Ces logiques ont l'intérêt d'exprimer relativement bien les contraintes 'intuitives', 'humaines' que l'on souhaiteraient que le système vérifie( ex: contrats).
Dans cette thèse nous nous adressons aux problèmes d'extraction de noyaux minimaux non satisfaisables pour la logique temporelle.
Nous appliquerons nos résultats théoriques et pratiques à la décomposition (basée sur la conformité/les contrats) de processus métier/programmes.
Ces résultats théoriques et pratiques ont une forte application pour les systèmes agiles (Processus métier, (web) services (métiers) ), la théorie des familles de lignes de produits, la théorie des composant de programmes et la théorie de synthèse de programmes. Nous appliquons aussi nos résultats pour détailler la nature des conflits devant être gérés dans les résolveurs de la logique temporelle (linéaire).

Intérêt: Database, temporal logic, deontic logic, contract, causes, Sat solvers, reverse engineering, theorem proving, Service Oriented Computing, Business Processes