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

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.
File in questo prodotto:
Non ci sono file associati a questo prodotto.

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

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11581/405022
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 22
  • ???jsp.display-item.citation.isi??? 14
social impact