Specifying event-based systems with a counting fluent temporal logic
Fluent linear temporal logic is a formalism for specifying properties of event-based systems, based on propositions called fluents, defined in terms of activating and deactivating events. In this paper, we propose complementing the notion of fluent by the related concept of counting fluent. As oppos...
Guardado en:
| Publicado: |
2015
|
|---|---|
| Materias: | |
| Acceso en línea: | https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_02705257_v1_n_p733_Regis http://hdl.handle.net/20.500.12110/paper_02705257_v1_n_p733_Regis |
| Aporte de: |
| id |
paper:paper_02705257_v1_n_p733_Regis |
|---|---|
| record_format |
dspace |
| spelling |
paper:paper_02705257_v1_n_p733_Regis2023-06-08T15:24:37Z Specifying event-based systems with a counting fluent temporal logic Software architecture Software engineering Specifications Temporal logic Event-based system Fluents Linear temporal logic Logic model checking Numerical values Reactive system Temporal logic specifications Model checking Fluent linear temporal logic is a formalism for specifying properties of event-based systems, based on propositions called fluents, defined in terms of activating and deactivating events. In this paper, we propose complementing the notion of fluent by the related concept of counting fluent. As opposed to the boolean nature of fluents, counting fluents are numerical values, that enumerate event occurrences, and allow us to specify naturally some properties of reactive systems. Although by extending fluent linear temporal logic with counting fluents we obtain an undecidable, strictly more expressive formalism, we develop a sound (but incomplete) model checking approach for the logic, that reduces to traditional temporal logic model checking, and allows us to automatically analyse properties involving counting fluents, on finite event-based systems. Our experiments, based on relevant models taken from the literature, show that: (i) counting fluent temporal logic is better suited than traditional temporal logic for expressing properties in which the number of occurrences of certain events is relevant, and (ii) our model checking approach on counting fluent specifications is more efficient and scales better than model checking equivalent fluent temporal logic specifications. © 2015 IEEE. 2015 https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_02705257_v1_n_p733_Regis http://hdl.handle.net/20.500.12110/paper_02705257_v1_n_p733_Regis |
| institution |
Universidad de Buenos Aires |
| institution_str |
I-28 |
| repository_str |
R-134 |
| collection |
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) |
| topic |
Software architecture Software engineering Specifications Temporal logic Event-based system Fluents Linear temporal logic Logic model checking Numerical values Reactive system Temporal logic specifications Model checking |
| spellingShingle |
Software architecture Software engineering Specifications Temporal logic Event-based system Fluents Linear temporal logic Logic model checking Numerical values Reactive system Temporal logic specifications Model checking Specifying event-based systems with a counting fluent temporal logic |
| topic_facet |
Software architecture Software engineering Specifications Temporal logic Event-based system Fluents Linear temporal logic Logic model checking Numerical values Reactive system Temporal logic specifications Model checking |
| description |
Fluent linear temporal logic is a formalism for specifying properties of event-based systems, based on propositions called fluents, defined in terms of activating and deactivating events. In this paper, we propose complementing the notion of fluent by the related concept of counting fluent. As opposed to the boolean nature of fluents, counting fluents are numerical values, that enumerate event occurrences, and allow us to specify naturally some properties of reactive systems. Although by extending fluent linear temporal logic with counting fluents we obtain an undecidable, strictly more expressive formalism, we develop a sound (but incomplete) model checking approach for the logic, that reduces to traditional temporal logic model checking, and allows us to automatically analyse properties involving counting fluents, on finite event-based systems. Our experiments, based on relevant models taken from the literature, show that: (i) counting fluent temporal logic is better suited than traditional temporal logic for expressing properties in which the number of occurrences of certain events is relevant, and (ii) our model checking approach on counting fluent specifications is more efficient and scales better than model checking equivalent fluent temporal logic specifications. © 2015 IEEE. |
| title |
Specifying event-based systems with a counting fluent temporal logic |
| title_short |
Specifying event-based systems with a counting fluent temporal logic |
| title_full |
Specifying event-based systems with a counting fluent temporal logic |
| title_fullStr |
Specifying event-based systems with a counting fluent temporal logic |
| title_full_unstemmed |
Specifying event-based systems with a counting fluent temporal logic |
| title_sort |
specifying event-based systems with a counting fluent temporal logic |
| publishDate |
2015 |
| url |
https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_02705257_v1_n_p733_Regis http://hdl.handle.net/20.500.12110/paper_02705257_v1_n_p733_Regis |
| _version_ |
1768543132669968384 |