Document - Specifying and Verifying Properties of Space

2014

Conference article Open Access

Specifying and Verifying Properties of Space

Ciancia V., Latella D., Loreti M., Massink M.

Modal Logics [INFO]Computer Science [cs] Specifying and verifying and reasoning about programs soggetto Model Checking Closure Spaces Spatial logics Topological Spaces Mathematical logic Model logics Software/Program verification Topological spaces

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.

Source: Theoretical Computer Science, pp. 222–235, Roma, 1-3 Settembre 2014

Publisher: Springer, Berlin Heidelberg, DEU

Citations

M. Aiello. Spatial Reasoning: Theory and Practice. PhD thesis, Institute of Logic, Language and Computation, University of Amsterdam, 2002.
M. Aiello, I. Pratt-Hartmann, and J. van Benthem, editors. Handbook of Spatial Logics. Springer, 2007.
C. Baier and J.P. Katoen. Principles of model checking. MIT Press, 2008.
M. Bojanczyk, B. Klin, and S. Lasota. Automata with group actions. In LICS, pages 355{364. IEEE Computer Society, 2011.
L. Bortolussi, J. Hillston, D. Latella, and M. Massink. Continuous approximation of collective system behaviour: A tutorial. Perform. Eval., 70(5):317 { 349, 2013.
L. Caires and L. Cardelli. A spatial logic for concurrency (part I). Information and Computation, 186(2):194{235, 2003.
L. Cardelli, P. Gardner, and G. Ghelli. A spatial logic for querying graphs. In ICALP, volume 2380 of LNCS, pages 597{610. Springer, 2002.
L. Cardelli and A.D. Gordon. Anytime, anywhere: Modal logics for mobile ambients. In POPL, pages 365{377. ACM, 2000.
A. Chaintreau, J. Le Boudec, and N. Ristanovic. The age of gossip: Spatial mean eld regime. SIGMETRICS, pages 109{120, New York, NY, USA, 2009. ACM.
Vincenzo Ciancia, Diego Latella, Michele Loreti, and Mieke Massink. Specifying and verifying properties of space - extended version. CoRR, abs/1406.6393, 2014.
R. De Nicola, G.L. Ferrari, and R. Pugliese. Klaim: A kernel language for agents interaction and mobility. IEEE Trans. Software Eng., 24(5):315{330, 1998.
A. Del Bimbo, E. Vicario, and D. Zingoni. Symbolic description and visual querying of image sequences using spatio-temporal logic. IEEE Trans. Knowl. Data Eng., 7(4):609{622, 1995.
M.P. Fiore and S. Staton. Comparing operational models of name-passing process calculi. Information and Computation, 204(4):524{560, 2006.
M.J. Gabbay and V. Ciancia. Freshness and name-restriction in sets of traces with names. In FOSSACS, volume 6604 of LNCS, pages 365{380. Springer, 2011.
F. Gadducci and A. Lluch-Lafuente. Graphical encoding of a spatial logic for the pi -calculus. In CALCO, volume 4624 of LNCS, pages 209{225. Springer, 2007.
A. Galton. The mereotopology of discrete space. In COSIT, volume 1661 of LNCS, pages 251{266. Springer, 1999.
A. Galton. A generalized topological view of motion in discrete space. Theoretical Computer Science, 305(1{3):111 { 134, 2003.
R. Kontchakov, A. Kurucz, F. Wolter, and M. Zakharyaschev. Spatial logic + temporal logic = ? In Aiello et al. [2], pages 497{564.
V.A. Kovalevsky. Geometry of Locally Finite Spaces: Computer Agreeable Topology and Algorithms for Computer Imagery. House Dr. Baerbel Kovalevski, 2008.
P. Kremer and G. Mints. Dynamic topological logic. In Aiello et al. [2], pages 565{606.
A. Kurz, T. Suzuki, and E. Tuosto. On nominal regular languages with binders. In FoSSaCS, volume 7213 of LNCS, pages 255{269. Springer, 2012.
A. Rosenfeld. Digital topology. The American Mathematical Monthly, 86(8):621{ 630, 1979.
M.B. Smyth and J. Webster. Discrete spatial models. In Aiello et al. [2], pages 713{798.
J. van Benthem and G. Bezhanishvili. Modal logics of space. In Handbook of Spatial Logics, pages 217{298. 2007.
T. Yung Kong and A. Rosenfeld. Digital topology: Introduction and survey. Computer Vision, Graphics, and Image Processing, 48(3):357{393, 1989.

Metrics

Back to previous page

Cite as

BibTeX entry

@inproceedings{oai:it.cnr:prodotti:284128,
	title = {Specifying and Verifying Properties of Space},
	author = {Ciancia V. and Latella D. and Loreti M. and Massink M.},
	publisher = {Springer, Berlin Heidelberg, DEU},
	doi = {10.1007/978-3-662-44602-7_18},
	booktitle = {Theoretical Computer Science, pp. 222–235, Roma, 1-3 Settembre 2014},
	year = {2014}
}