PUMA
Istituto di Scienza e Tecnologie dell'Informazione     
Ciancia V., Grilletti G., Latella D., Loreti M., Massink M. An experimental spatio-temporal model checker. Domenico Bianculli, Radu Calinescu, Bernhard Rumpe (eds.). (Lecture Notes in Computer Science, vol. 9509). York, UK: Springer, 2015.
 
 
Abstract
(English)
In this work we present a spatial extension of the global model checking algorithm of the temporal logic CTL. This classical veri- fication framework is augmented with ideas coming from the tradition of topological spatial logics. More precisely, we add to CTL the operators of the Spatial Logic of Closure Spaces, including the surrounded operator, with its intended meaning of a point being surrounded by entities sat- isfying a specific property. The interplay of space and time permits one to define complex spatio-temporal properties. The model checking algo- rithm that we propose features no particular efficiency optimisations, as it is meant to be a reference specification of a family of more efficient algorithms that are planned for future work. Its complexity depends on the product of temporal states and points of the space. Nevertheless, a prototype model checker has been implemented, made available, and used for experimentation of the application of spatio-temporal verifica- tion in the field of collective adaptive systems.
URL: http://link.springer.com/chapter/10.1007/978-3-662-49224-6_24
DOI: 10.1007/978-3-662-49224-6_24
Subject Modal Logics
Model Checking
Simulation
Closure Spaces
F.4.1 Mathematical Logic
D.2.4 Software/Program Verification


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