Specifying and Verifying Properties of Space

Abstract : The interplay between process behaviour and spatial aspects of computation has become more and more relevant in Computer Science, especially in the field of collective adaptive systems, but also, more generally, when dealing with systems distributed in physical space. Traditional verification techniques are well suited to analyse the temporal evolution of programs; properties of space are typically not explicitly taken into account. We propose a methodology to verify properties depending upon physical space. We define an appropriate logic, stemming from the tradition of topological interpretations of modal logics, dating back to earlier logicians such as Tarski, where modalities describe neighbourhood. We lift the topological definitions to a more general setting, also encompassing discrete, graph-based structures. We further extend the framework with a spatial until operator, and define an efficient model checking procedure, implemented in a proof-of-concept tool.
Type de document :
Communication dans un congrès
Josep Diaz; Ivan Lanese; Davide Sangiorgi. 8th IFIP International Conference on Theoretical Computer Science (TCS), Sep 2014, Rome, Italy. Springer, Lecture Notes in Computer Science, LNCS-8705, pp.222-235, 2014, Theoretical Computer Science. 〈10.1007/978-3-662-44602-7_18〉
Liste complète des métadonnées

Littérature citée [24 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01402045
Contributeur : Hal Ifip <>
Soumis le : jeudi 24 novembre 2016 - 10:51:47
Dernière modification le : mardi 31 juillet 2018 - 16:58:01
Document(s) archivé(s) le : mardi 21 mars 2017 - 03:40:10

Fichier

978-3-662-44602-7_18_Chapter.p...
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

Citation

Vincenzo Ciancia, Diego Latella, Michele Loreti, Mieke Massink. Specifying and Verifying Properties of Space. Josep Diaz; Ivan Lanese; Davide Sangiorgi. 8th IFIP International Conference on Theoretical Computer Science (TCS), Sep 2014, Rome, Italy. Springer, Lecture Notes in Computer Science, LNCS-8705, pp.222-235, 2014, Theoretical Computer Science. 〈10.1007/978-3-662-44602-7_18〉. 〈hal-01402045〉

Partager

Métriques

Consultations de la notice

48

Téléchargements de fichiers

56