Recently, one of the new trends in Model-Checking/sat research is the study of the causes of verification/falsification of a given temporal logic property. Extracting the causes enables the end user to understand which constraints contributes to the assessed result(Model checking, satisfiability). More simply, it can be useful to find which part of the program/system corresponds to such part of a contract and not necessarily to another part of the contract. Understanding the cause is the backbone of a sound development of a theory of compliance-based decomposition of program/system/business processes. How to provide a simpler program if the contract is changed and `lightened'. How to reuse it ? Since contract-based properties to check usually crosses cut the whole structure of the program (covering many components...) this problem is challenging. Although much work exist for extracting causes in the propositional case (and sat modulo theory), few work address this issue in modal logic such as deontic or temporal logic. Such latter logics get the advantage to express intuitive and 'human' constraints that the program, the business process or the system should checked (e.g., contracts, legal rules). In this Phd Thesis we handle theoretical and practical issue for computing these causes in Linear Temporal Logic. We apply our result to the compliance based decomposition of program and data-centric business processes. Our application target is the agile systems ((Business) (web) services, Business process), the theory of product line family, component based theory and synthesis of program/system. We describe also the flavor of the conflicts that any Linear Temporal Logic solver should handle. Topic : Database, temporal logic, deontic logic, Contracts, Cause, Sat solvers, reverse engineering, theorem proving, Service Oriented Computing, Business Process