
\documentclass[french]{article}
\usepackage{lmodern}
\usepackage{array}
\usepackage{babel}

\makeatletter
\newcommand\justify{%
  \let\\\@centercr
  \rightskip\z@skip
  \leftskip\z@skip}
\makeatother

\begin{document}
\thispagestyle{empty}

\begin{tabular}{|l>{\justify}p{5cm}|}
\hline
LTL & Logique du temps linéaire : cette logique
      permet d'exprimer des propriétés sur une
      exécution du système. \\
      Le model checking et la satisfaisabilité
      sont alors PSPACE-complets.
      \tabularnewline[3mm]
CTL & Logique du temps arborescent : cette logique
      exprime des propriétés sur l'arbre de
      toutes les exécutions possibles. \\
      Le model checking est P-complet, mais la
      satisfaisabilité est EXPTIME-complète.
      \tabularnewline
\hline
\end{tabular}
\end{document}
