Top

Published in:

2019 | OriginalPaper | Chapter

Embedding RCC8D in the Collective Spatial Logic CSLCS

Authors : Vincenzo Ciancia, Diego Latella, Mieke Massink

Published in: Models, Languages, and Tools for Concurrent and Distributed Programming

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

Discrete mereotopology is a logical theory for the specification of qualitative spatial functions and relations defined over a discrete space, intended as a set of basic elements, the pixels, with an adjacency relation defined over it. The notions of interest are that of region, intended as an arbitrary aggregate of pixels, and of specific relations between regions. The mereotopological theory RCC8D extends the mereological theory RCC5D—a theory of region parthood for discrete spaces—with the topological notion of connection and the remaining relations (disconnection, external connection, tangential and nontangential proper parthood and their inverses). In this paper, we propose an encoding of RCC8D into CSLCS, the collective extension of the Spatial Logic of Closure Spaces SLCS. We show how topochecker, a model-checker for CSLCS, can be used for effectively checking the existence of a RCC8D relation between two given regions of a discrete space.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter Featherweight Scribble

next chapter From Behavioural Contracts to Session Types

Available only for authorised users

Topochecker: a topological model checker, see http://topochecker.isti.cnr.it, https://github.com/vincenzoml/topochecker.

Note that this colour does not correspond to any atomic predicate and so it is not part of the model; we use it only for illustration purposes.

It is trivial to prove that, for quasi-discrete closure space \((X,\mathcal {C}_{R})\), whenever \(R\) is symmetric, if \(B \subseteq \mathcal {C}_{R}(A)\) then \(\mathcal {C}_{R}(B) \cap A \not =\emptyset \), for all non-empty \(A,B \subseteq X\).

See http://www.ocaml.org.

In the remainder of this section, we employ the syntax of topochecker, using & for conjunction, | for disjunction, ! for negation,

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-030-21485-2_15/MediaObjects/485305_1_En_15_Figb_HTML.gif

for the “share” connective, and Gr for the “group” connective.

This may change in a future release of the model checker.

Aiello, M., Pratt-Hartmann, I., van Benthem, J. (eds.): Handbook of Spatial Logics. Springer, Dordrecht (2007). https://doi.org/10.1007/978-1-4020-5587-4CrossRefMATH

Banci Buonamici, F., Belmonte, G., Ciancia, V., Latella, D., Massink, M.: Spatial logics and model checking for medical imaging. Int. J. Softw. Tools Technol. Transf. (2019). https://doi.org/10.1007/s10009-019-00511-9

Belmonte, G., Ciancia, V., Latella, D., Massink, M.: From collective adaptive systems to human centric computation and back: spatial model checking for medical imaging. In: ter Beek, M.H., Loreti, M. (eds.) Proceedings of the Workshop on FORmal Methods for the Quantitative Evaluation of Collective Adaptive SysTems, FORECAST@STAF 2016, Vienna, Austria, 8 July 2016. EPTCS, vol. 217, pp. 81–92 (2016). https://doi.org/10.4204/EPTCS.217.10CrossRef

Belmonte, G., Ciancia, V., Latella, D., Massink, M.: VoxLogicA: A Spatial Model Checker for Declarative Image Analysis. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11427, pp. 281–298. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-17462-0_16. http://arxiv.org/abs/1811.05677CrossRef

Bennett, B., Düntsch, I.: Axioms, algebras and topology. In: Springer [1], pp. 99–159CrossRef

Binchi, J., Merelli, E., Rucco, M., Petri, G., Vaccarino, F.: jHoles: a tool for understanding biological complex networks via clique weight rank persistent homology. Electr. Notes Theor. Comput. Sci. 306, 5–18 (2014). https://doi.org/10.1016/j.entcs.2014.06.011MathSciNetCrossRefMATH

Buti, F., Cacciagrano, D., Corradini, F., Merelli, E., Tesei, L., Pani, M.: Bone remodelling in BioShape. Electr. Notes Theor. Comput. Sci. 268, 17–29 (2010). https://doi.org/10.1016/j.entcs.2010.12.003MathSciNetCrossRefMATH

Buti, F., Cacciagrano, D., Callisto De Donato, M., Corradini, F., Merelli, E., Tesei, L.: \(BioShape\): end-user development for simulating biological systems. In: Costabile, M.F., Dittrich, Y., Fischer, G., Piccinno, A. (eds.) IS-EUD 2011. LNCS, vol. 6654, pp. 379–382. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-21530-8_45CrossRef

Ciancia, V., Latella, D., Loreti, M., Massink, M.: Specifying and verifying properties of space. In: Diaz, J., Lanese, I., Sangiorgi, D. (eds.) TCS 2014. LNCS, vol. 8705, pp. 222–235. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-662-44602-7_18CrossRef

10.

Ciancia, V., Latella, D., Loreti, M., Massink, M.: Model checking spatial logics for closure spaces. Logical Methods Comput. Sci. 12(4) (2016). http://lmcs.episciences.org/2067

11.

Ciancia, V., Gilmore, S., Grilletti, G., Latella, D., Loreti, M., Massink, M.: Spatio-temporal model checking of vehicular movement in public transport systems. STTT 20(3), 289–311 (2018). https://doi.org/10.1007/s10009-018-0483-8CrossRef

12.

Ciancia, V., Latella, D., Loreti, M., Massink, M.: Spatial logic and spatial model checking for closure spaces. In: Bernardo, M., De Nicola, R., Hillston, J. (eds.) SFM 2016. LNCS, vol. 9700, pp. 156–201. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-34096-8_6CrossRefMATH

13.

Ciancia, V., Latella, D., Massink, M., Paskauskas, R.: Exploring spatio-temporal properties of bike-sharing systems. In: 2015 IEEE International Conference on Self-Adaptive and Self-Organizing Systems Workshops, SASO Workshops 2015, Cambridge, MA, USA, 21–25 September 2015, pp. 74–79. IEEE Computer Society (2015). https://doi.org/10.1109/SASOW.2015.17

14.

Ciancia, V., Latella, D., Massink, M., Paškauskas, R., Vandin, A.: A tool-chain for statistical spatio-temporal model checking of bike sharing systems. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9952, pp. 657–673. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-47166-2_46CrossRef

15.

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). https://doi.org/10.1007/3-540-48384-5_17CrossRef

16.

Galton, A.: A generalized topological view of motion in discrete space. Theor. Comput. Sci. 305(1–3), 111–134 (2003). https://doi.org/10.1016/S0304-3975(02)00701-6MathSciNetCrossRefMATH

17.

Randell, D.A., Cui, Z., Cohn, A.G.: A spatial logic based on regions and connection. In: Nebel, B., Rich, C., Swartout, W.R. (eds.) Proceedings of the 3rd International Conference on Principles of Knowledge Representation and Reasoning (KR 1992), Cambridge, MA, USA, 25–29 October 1992, pp. 165–176. Morgan Kaufmann (1992)

18.

Randell, D.A., Landini, G., Galton, A.: Discrete mereotopology for spatial reasoning in automated histological image analysis. IEEE Trans. Pattern Anal. Mach. Intell. 35(3), 568–581 (2013). https://doi.org/10.1109/TPAMI.2012.128CrossRef

19.

Smyth, M.B., Webster, J.: Discrete spatial models. In: Springer [1], pp. 713–798CrossRef

20.

van Benthem, J., Bezhanishvili, G.: Modal logics of space. In: Springer [1], pp. 217–298

Title: Embedding RCC8D in the Collective Spatial Logic CSLCS
Authors: Vincenzo Ciancia
Diego Latella
Mieke Massink
Publisher: Springer International Publishing
Book: Models, Languages, and Tools for Concurrent and Distributed Programming
Print ISBN: 978-3-030-21484-5

Electronic ISBN: 978-3-030-21485-2

Copyright Year: 2019
DOI: https://doi.org/10.1007/978-3-030-21485-2_15

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner