Data di Pubblicazione:
2022
Abstract:
We present two different extensions of the spatial logic for closure spaces (SLCS), and its spatio-temporal variant (?SLCS), with spa- tial quantification operators. The first concerns the existential quantifi- cation on individual points of a space. The second concerns the quantifi- cation on sets of points. The latter amounts to a form of quantification over atomic propositions, thus without the full power of second order logic. The spatial quantification operators are useful for reasoning about the existence of particular spatial objects in a space, their spatial rela- tion with respect to other spatial objects, and, in the spatio-temporal setting, to reason about the dynamic evolution of such spatial objects in time and space, including reasoning about newly introduced items. In this preliminary study we illustrate the expressiveness of the operators by means of several small, but representative, examples.
Tipologia CRIS:
04.01 Contributo in Atti di convegno
Keywords:
Closure spaces; Spatial logics; Spatio-temporal logics; Binding; Propositional quantifiers
Elenco autori:
Bussi, Laura; Massink, Mieke; Latella, Diego; Ciancia, Vincenzo
Link alla scheda completa:
Link al Full Text:
Titolo del libro:
Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles