Temporal logics are formal tools for specifications and verification of computer systems. The success of these logics is mainly due to their elegant syntax and intuitive semantics that simplify the represen- tation of system’s properties that change over time. From automata based solvers to tableaux methods, several approaches are developed based on these formalisms. However, these logics remain limited when modeling and reasoning about certain aspects of computer systems. Indeed, computer systems are not guaranteed to be totally safe, and the properties one wishes to verify may have trivial and tolerable ex- ceptions, or on the contrary, exceptions that must be carefully handled to guarantee the general reliability of the system. Similarly, the expected behaviour of a system may not be correct for every possible execution, but rather for its most “normal” or plausible executions. Non-monotonic logic is a field of research that captures defeasible modes of reasoning which accu- rately represent common sense reasoning more than the deductive reasoning of classical logic. Moreover, it allows for reasoning with exceptions. The main objective of this work is to integrate non-monotonic approaches to temporal logics to better represent the behavior of exception-tolerant systems. The formalism presented in this memoir is called defeasible linear temporal logic. This logic com- bines the syntax and semantics of LTL with the preferential KLM approach to conditional statements. The syntax contains a defeasible version of temporal operators, which express specifications similar to their classical counterparts, but are more lenient when time points may have exceptions during execu- tions. Defeasible LTL extends temporal interpretations with a preference relation that nuances the degree of importance between time points. We have studied the decidability of the satisfiability problem for defeasible LTL sentences. In this setting, we have considered two fragments of the language, which are L1 and L⋆. We proved that the satisfiability of L1 sentences is an NP-complete problem. As for the fragment L⋆, we showed the decidability of the problem for a class of interpretations called state-dependent interpretations. We have proved that the bounded-model property holds for both of these fragments. Thanks to these properties, we have introduced structures and methods for solving the satisfiability problem. We have developed also a tableau method for L1 by adapting the recently proposed one-pass tree- shaped tableaux for classical LTL. The novelty of our approach is to show how KLM’s preferential semantics work in a tableau for defeasible LTL. We have defined a set of static rules for different opera- tors, as well as a set of dynamic rules for checking the correctness of branches at the same time of their expansion. We have proved that the method is sound and complete. Finally, we investigate future work relating to defeasible LTL. We also plan to integrate preferential semantics to other temporal formalisms, namely CTL and CTL*.