Istituto di Scienza e Tecnologie dell'Informazione     
Ciancia V., Latella D., Loreti M., Massink M. Model checking spatial logics for closure spaces - Extended Version. QUANTICOL Technical Report TR-QC-03-2016. Technical report, 2016.
Spatial aspects of computation are becoming increasingly relevant in Computer Science, es- pecially in the eld of collective adaptive systems and when dealing with systems distributed in physical space. Traditional formal veri cation techniques are well suited to analyse the temporal evolution of programs; however, properties of space are typically not taken into account explic- itly. We present a topology-based approach to formal veri cation of spatial properties 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 extend the framework with a spa- tial surrounded operator, a propagation operator and with some collective operators. The latter are interpreted over arbitrary sets of points instead of individual points in space. We de ne ecient model checking procedures, both for the individual and the collective spatial fragments of the logic and provide a proof-of-concept tool.
Subject Model logics
Spatial Logics
F.3.1 LOGICS AND MEANINGS OF PROGRAMS. Specifying and Verifying and Reasoning about Programs

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