Para comprobar si un algoritmo concurrente es correcto hace falta un formalismo que es capaz de incluir los efectos que un proceso puede causar en el estado de otro proceso a lo largo del tiempo.
La lógica temporal es una extensión de la lógica clásica que incluye en sus formulas el tiempo y proporciona una técnica formal de comprobar propriedades de programas concurrentes.
Entro los operadores se suele encontrar: ahora (now), después (next), hasta (until), antes (previous), desde (since) y adicionalmente finalmente (eventually) y a-partir-de-ahora-en-adelante (henceforth).
Con estos operadores se puede producir, p.e., sentencias como
donde p y q son variables que describen el estado del programa.