PUMA
Istituto di Scienza e Tecnologie dell'Informazione     
Ciancia V., Latella D., Loreti M., Massink M. Specifying and verifying properties of space. QUANTICOL Technical Report TR-QC-06-2014. Technical report, 2014.
 
 
Abstract
(English)
The interplay between process behaviour and spatial aspects of computation has become more and more relevant in Computer Science, especially in the eld of collective adaptive systems, but also, more generally, when dealing with systems distributed in physical space. Traditional veri ca- tion techniques are well suited to analyse the temporal evolution of programs; however, properties of space are typically not explicitly taken into account. We propose a methodology to verify prop- erties depending upon physical space. We de ne 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 de nitions to the more general setting of closure spaces, also encompassing discrete, graph-based structures. We further extend the frame- work with a spatial until operator, and de ne an ecient model checking procedure, implemented in a proof-of-concept tool.
Subject Model logics
Spatial Logics
Topological Spaces
F.3.1 LOGICS AND MEANINGS OF PROGRAMS . Specifying and Verifying and Reasoning about Programs
F.4.1 MATHEMATICAL LOGIC AND FORMAL LANGUAGES. Mathematical Logic
D.2.4 SOFTWARE ENGINEERING. Software/Program Verification
03B70 Logic in computer science
03B45 Modal logic (including the logic of norms)


Icona documento 1) Download Document PDF


Icona documento Open access Icona documento Restricted Icona documento Private

 


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional