Verificación Automatizada Eficiente de Sistemas Concurrentes Especificando Sus Propiedades con Fórmalus de una Lógica de Intervalos.