Specifying and Verifying Properties of Space (Contributo in atti di convegno)

Type

• Prodotto della ricerca (Classe)
• Contributo in atti di convegno (Classe)

Label

• Specifying and Verifying Properties of Space (Contributo in atti di convegno) (literal)

Anno

• 2014-01-01T00:00:00+01:00 (literal)

Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#doi

• 10.1007/978-3-662-44602-7_18 (literal)

Alternative label

• Ciancia V.; Latella D.; Loreti M.; Massink M. (2014)
  Specifying and Verifying Properties of Space
  in Theoretical Computer Science, Roma, 1-3 Settembre 2014
  (literal)

Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#autori

• Ciancia V.; Latella D.; Loreti M.; Massink M. (literal)

Pagina inizio

• 222 (literal)

Pagina fine

• 235 (literal)

Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#altreInformazioni

• Progetto: A Quantitative Approach to Management and Design of Collective and Adaptive Behaviours Acronimo: QUANTICOL Grant agreement: 600708 Tipo Progetto: EU_FP7 (literal)

Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#url

• http://www.scopus.com/inward/record.url?eid=2-s2.0-84906768718&partnerID=q2rCbXpz (literal)

Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#numeroVolume

• 8705 LNCS (literal)

Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#volumeInCollana

• 8705 LNCS (literal)

Rivista

• Lecture notes in computer science (Rivista)

Note

• Scopu (literal)
• PuMa (literal)

Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#affiliazioni

• Istituto di Scienza e Tecnologie dell'Informazione 'A. Faedo', CNR, Italy; Università di Firenze, Italy (literal)

Titolo

• Specifying and Verifying Properties of Space (literal)

Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#isbn

• 978-3-662-44601-0 (literal)

Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#curatoriVolume

• Josep Diaz, Ivan Lanese, Davide Sangiorgi (literal)

Abstract

• 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. (literal)

Editore

• Springer (Editore)

Prodotto di

• Istituto di scienza e tecnologie dell'informazione \"Alessandro Faedo\" (ISTI) (Istituto)
• Metodi e Strumenti per la Progettazione di Sistemi Software-Intensive ad Elevata Complessità (ICT.P09.008.002) (Modulo)

Autore CNR

• DIEGO LATELLA (Unità di personale interno)
• VINCENZO CIANCIA (Persona)
• MIEKE MASSINK (Unità di personale interno)

Insieme di parole chiave

• Parole chiave di "Specifying and Verifying Properties of Space" (Insieme di parole chiave)

Incoming links:

Autore CNR di

• MIEKE MASSINK (Unità di personale interno)
• DIEGO LATELLA (Unità di personale interno)
• VINCENZO CIANCIA (Persona)

Prodotto

• Istituto di scienza e tecnologie dell'informazione \"Alessandro Faedo\" (ISTI) (Istituto)
• Metodi e Strumenti per la Progettazione di Sistemi Software-Intensive ad Elevata Complessità (ICT.P09.008.002) (Modulo)

Editore di

• Springer (Editore)

Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#rivistaDi

• Lecture notes in computer science (Rivista)

Insieme di parole chiave di

• Parole chiave di "Specifying and Verifying Properties of Space" (Insieme di parole chiave)