En este trabajo introducimos la lógica temporal con fluentes contadores, una extensión de la
lógica temporal con fluentes que complementa la noción de fluente proposicional con el concepto de fluente contador. A diferencia de los anteriores, los fluentes contadores son variables numéricas que enumeran ocurrencias de eventos, permitiendo caracterizar de una manera más natural e intuitiva propiedades en las cuales el número de veces que ocurren ciertos eventos del sistema es relevante. Si bien esta extensión es indecidible y estrictamente más expresiva que la lógica temporal lineal con fluentes, desarrollamos una técnica correcta pero incompleta para verificar propiedades de modelos de sistemas reactivos.
Esta técnica, que reduce la verificación a la verificación que implementa LTSA, permite verificar automáticamente propiedades con presencia de estos fluentes contadores bajo ciertas cotas impuestas a los mismos. Destacamos las ventajas de contar con esta lógica para especificar propiedades de sistemas basados en eventos, entre ellas, la de contar con fórmulas mas concisas y fáciles de manipular y modificar. Para ello abordamos varios ejemplos relevantes de la literatura, comparando las especificaciones de propiedades con ambas lógicas.