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.
Research partially funded by EU ASCENS (nr. 257414), EU QUANTICOL (nr. 600708), IT MIUR CINA and PAR FAS 2007-2013 Regione Toscana TRACE-IT.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Aiello, M.: Spatial Reasoning: Theory and Practice. PhD thesis, Institute of Logic, Language and Computation, University of Amsterdam (2002)
Aiello, M., Pratt-Hartmann, I., van Benthem, J. (eds.): Handbook of Spatial Logics. Springer (2007)
Baier, C., Katoen, J.P.: Principles of model checking. MIT Press (2008)
Bojanczyk, M., Klin, B., Lasota, S.: Automata with group actions. In: LICS, pp. 355–364. IEEE Computer Society Press (2011)
Bortolussi, L., Hillston, J., Latella, D., Massink, M.: Continuous approximation of collective system behaviour: A tutorial. Perform. Eval. 70(5), 317–349 (2013)
Caires, L., Cardelli, L.: A spatial logic for concurrency (part I). Information and Computation 186(2), 194–235 (2003)
Cardelli, L., Gardner, P., Ghelli, G.: A spatial logic for querying graphs. In: Widmayer, P., Triguero, F., Morales, R., Hennessy, M., Eidenbenz, S., Conejo, R. (eds.) ICALP 2002. LNCS, vol. 2380, pp. 597–610. Springer, Heidelberg (2002)
Cardelli, L., Gordon, A.D.: Anytime, anywhere: Modal logics for mobile ambients. In: POPL, pp. 365–377. ACM (2000)
Chaintreau, A., Le Boudec, J., Ristanovic, N.: The age of gossip: Spatial mean field regime. In: SIGMETRICS, pp. 109–120. ACM, New York (2009)
Ciancia, V., Latella, D., Loreti, M., Massink, M.: Specifying and verifying properties of space - extended version. CoRR, abs/1406.6393 (2014)
De Nicola, R., Ferrari, G.L., Pugliese, R.: Klaim: A kernel language for agents interaction and mobility. IEEE Trans. Software Eng. 24(5), 315–330 (1998)
Del Bimbo, A., Vicario, E., Zingoni, D.: Symbolic description and visual querying of image sequences using spatio-temporal logic. IEEE Trans. Knowl. Data Eng. 7(4), 609–622 (1995)
Fiore, M.P., Staton, S.: Comparing operational models of name-passing process calculi. Information and Computation 204(4), 524–560 (2006)
Gabbay, M.J., Ciancia, V.: Freshness and name-restriction in sets of traces with names. In: Hofmann, M. (ed.) FOSSACS 2011. LNCS, vol. 6604, pp. 365–380. Springer, Heidelberg (2011)
Gadducci, F., Lluch Lafuente, A.: Graphical encoding of a spatial logic for the π-calculus. In: Mossakowski, T., Montanari, U., Haveraaen, M. (eds.) CALCO 2007. LNCS, vol. 4624, pp. 209–225. Springer, Heidelberg (2007)
Galton, A.: The mereotopology of discrete space. In: Freksa, C., Mark, D.M. (eds.) COSIT 1999. LNCS, vol. 1661, pp. 251–266. Springer, Heidelberg (1999)
Galton, A.: A generalized topological view of motion in discrete space. Theoretical Computer Science 305(1-3), 111 (2003)
Kontchakov, R., Kurucz, A., Wolter, F., Zakharyaschev, M.: Spatial logic + temporal logic =? In: Aiello, et al. (eds.) [2], pp. 497–564
Kovalevsky, V.A.: Geometry of Locally Finite Spaces: Computer Agreeable Topology and Algorithms for Computer Imagery. House Dr. Baerbel Kovalevski (2008)
Kremer, P., Mints, G.: Dynamic topological logic. In: Aiello, et al. (eds.) [2], pp. 565–606
Kurz, A., Suzuki, T., Tuosto, E.: On nominal regular languages with binders. In: Birkedal, L. (ed.) FOSSACS 2012. LNCS, vol. 7213, pp. 255–269. Springer, Heidelberg (2012)
Rosenfeld, A.: Digital topology. The American Mathematical Monthly 86(8), 621–630 (1979)
Smyth, M.B., Webster, J.: Discrete spatial models. In: Aiello, et al. (eds.) [2], pp. 713–798
van Benthem, J., Bezhanishvili, G.: Modal logics of space. In: Handbook of Spatial Logics, pp. 217–298 (2007)
Yung Kong, T., Rosenfeld, A.: Digital topology: Introduction and survey. Computer Vision, Graphics, and Image Processing 48(3), 357–393 (1989)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 IFIP International Federation for Information Processing
About this paper
Cite this paper
Ciancia, V., Latella, D., Loreti, M., Massink, M. (2014). Specifying and Verifying Properties of Space. In: Diaz, J., Lanese, I., Sangiorgi, D. (eds) Theoretical Computer Science. TCS 2014. Lecture Notes in Computer Science, vol 8705. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-44602-7_18
Download citation
DOI: https://doi.org/10.1007/978-3-662-44602-7_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-44601-0
Online ISBN: 978-3-662-44602-7
eBook Packages: Computer ScienceComputer Science (R0)