Istituto di Scienza e Tecnologie dell'Informazione     
Ciancia V., Latella D., Loreti M., Massink M. Spatial logic and spatial model checking for closure spaces. Bernardo M., De Nicola R., Hillston J (eds.). (Lecture Notes in Computer Science, vol. 9700). Germania: Springer, 2016.
Spatial aspects of computation are increasingly relevant in Computer Science, especially in the field of collective adaptive systems and when dealing with systems distributed in physical space. Traditional formal verification techniques are well suited to analyse the temporal evolution of concurrent systems; however, properties of space are typically not explicitly taken into account. This tutorial provides an introduction to recent work on a topology-inspired approach to formal verification of spatial properties depending upon (physical) space. A logic is presented, stemming from the tradition of topological interpretations of modal logics, dating back to earlier logicians such as Tarski, where modalities describe neighbourhood. These topological definitions are lifted to the more general setting of closure spaces, also encompassing discrete, graph-based structures. The present tutorial illustrates the extension of the framework with a spatial surrounded operator, leading to the spatial logic for closure spaces SLCS, and its combination with the temporal logic CTL, leading to STLCS. The interplay of space and time permits one to define complex spatio-temporal properties. Both for the spatial and the spatio-temporal fragment efficient model-checking algorithms have been developed and their use on a number of case studies and examples is illustrated.
URL: http://link.springer.com/chapter/10.1007/978-3-319-34096-8_6
DOI: 10.1007/978-3-319-34096-8_6
Subject Modal Logics
Model Checking
Topological Spaces
Closure Spaces
F.4.1 Mathematical Logic
D.2.4 Software/Program Verification
03B45 Modal logic
68Q60 Specification and verification
54A05 Topological spaces and generalizations

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