Especificando sistemas basados en eventos con una lógica temporal con fluentes contadores

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.Sociedad Argentina de Informática e Investigación Operativa (SADIO