PUMA
Istituto di Scienza e Tecnologie dell'Informazione     
Ciancia V., Grilletti G., Latella D., Loreti M., Massink M. A spatio-temporal model-checker. QUANTICOL Technical Report TR-QC-10-2014. Technical report, 2014.
 
 
Abstract
(English)
We define a spatio-temporal logic, the Spatio-temporal Logic of Closure Spaces (STLCS). The logic is interpreted on Kripke models, in which each state has an associated closure space. The logic extends CTL with spatial operators, in the spirit of topological modal logic. More specifically, we add to CTL the operators of the Spatial Logic of Closure Spaces, including the spatial until operator, with its intended meaning of a point being surrounded by entities satisfying a specific property. The interplay of space and time permits one to define complex spatio-temporal properties. We present a simple model-checking algorithm for STLCS, which has been implemented in a prototype tool.
Subject Modal Logics
Spatial Logics
Temporal Logics
Model-checking
F.3.1 LOGICS AND MEANINGS OF PROGRAMS. Specifying and Verifying and Reasoning about Programs
03B70 Logic in computer science


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