Anzeige
Erschienen in:
2014 | OriginalPaper | Buchkapitel
Specifying and Verifying Properties of Space
verfasst von : Vincenzo Ciancia, Diego Latella, Michele Loreti, Mieke Massink
Erschienen in: Theoretical Computer Science
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
The interplay between process behaviour and spatial aspects of computation has become more and more relevant in Computer Science, especially in the field of
collective adaptive systems
, but also, more generally, when dealing with systems distributed in physical space. Traditional verification techniques are well suited to analyse the temporal evolution of programs; properties of space are typically not explicitly taken into account. We propose a methodology to verify properties depending upon physical space. We define an appropriate logic, stemming from the tradition of topological interpretations of modal logics, dating back to earlier logicians such as Tarski, where modalities describe neighbourhood. We lift the topological definitions to a more general setting, also encompassing discrete, graph-based structures. We further extend the framework with a spatial
until
operator, and define an efficient model checking procedure, implemented in a proof-of-concept tool.