In this work we present a spatial extension of the global model checking algorithm of the temporal logic CTL. This classical verification 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 satisfying a specific property. The interplay of space and time permits one to define complex spatio-temporal properties. The model checking algorithm 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 verification in the field of collective adaptive systems.

An experimental spatio-temporal model checker / Ciancia, Vincenzo; Grilletti, Gianluca; Latella, Diego; Loreti, Michele; Massink, Mieke. - STAMPA. - (2015), pp. 297-311. [10.1007/978-3-662-49224-6_24]

An experimental spatio-temporal model checker

LORETI, MICHELE;
2015

Abstract

In this work we present a spatial extension of the global model checking algorithm of the temporal logic CTL. This classical verification 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 satisfying a specific property. The interplay of space and time permits one to define complex spatio-temporal properties. The model checking algorithm 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 verification in the field of collective adaptive systems.
2015
9783662492239
9783662492239
Software Engineering and Formal Methods - SEFM 2015 Collocated Workshops: ATSE, HOFM, MoKMaSD, and VERY*SCART, York, UK, September 7-8, 2015, Revised Selected Papers, Lecture Notes in Computer Science, Vol. 9509.
297
311
Ciancia, Vincenzo; Grilletti, Gianluca; Latella, Diego; Loreti, Michele; Massink, Mieke
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in FLORE sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificatore per citare o creare un link a questa risorsa: https://hdl.handle.net/2158/1039232
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 28
  • ???jsp.display-item.citation.isi??? 23
social impact