Analysing Spatial Properties on Neighbourhood Spaces

Authors Sven Linker , Fabio Papacchini, Michele Sevegnani



PDF
Thumbnail PDF

File

LIPIcs.MFCS.2020.66.pdf
  • Filesize: 496 kB
  • 14 pages

Document Identifiers

Author Details

Sven Linker
  • Department of Computer Science, University of Liverpool, UK
Fabio Papacchini
  • Department of Computer Science, University of Liverpool, UK
Michele Sevegnani
  • School of Computing Science, University of Glasgow, UK

Cite AsGet BibTex

Sven Linker, Fabio Papacchini, and Michele Sevegnani. Analysing Spatial Properties on Neighbourhood Spaces. In 45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 170, pp. 66:1-66:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.MFCS.2020.66

Abstract

We present a bisimulation relation for neighbourhood spaces, a generalisation of topological spaces. We show that this notion, path preserving bisimulation, preserves formulas of the spatial logic SLCS. We then use this preservation result to show that SLCS cannot express standard topological properties such as separation and connectedness. Furthermore, we compare the bisimulation relation with standard modal bisimulation and modal bisimulation with converse on graphs and prove it coincides with the latter.

Subject Classification

ACM Subject Classification
  • Theory of computation → Modal and temporal logics
  • Mathematics of computing → Topology
Keywords
  • spatial logic
  • topology
  • bisimulation

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads

References

  1. Marco Aiello, Ian Pratt-Hartmann, and Johan van Benthem, editors. Handbook of Spatial Logics. Springer, 2007. Google Scholar
  2. Marco Aiello and Johan van Benthem. A modal walk through space. Journal of Applied Non-Classical Logics, 12(3-4):319-363, 2002. URL: https://doi.org/10.3166/jancl.12.319-363.
  3. Fabrizio Banci Buonamici, Gina Belmonte, Vincenzo Ciancia, Diego Latella, and Mieke Massink. Spatial logics and model checking for medical imaging. International Journal on Software Tools for Technology Transfer, February 2019. URL: https://doi.org/10.1007/s10009-019-00511-9.
  4. Ezio Bartocci, Luca Bortolussi, Michele Loreti, and Laura Nenzi. Monitoring Mobile and Spatially Distributed Cyber-physical Systems. In Proceedings of the 15th ACM-IEEE International Conference on Formal Methods and Models for System Design, MEMOCODE '17, pages 146-155, New York, NY, USA, 2017. ACM. event-place: Vienna, Austria. URL: https://doi.org/10.1145/3127041.3127050.
  5. Yuliy Baryshnikov and Robert Ghrist. Target enumeration via Euler characteristic integrals. SIAM Journal on Applied Mathematics, 70(3):825-844, 2009. URL: https://doi.org/10.1137/070687293.
  6. Gina Belmonte, Vincenzo Ciancia, Diego Latella, and Mieke Massink. VoxLogicA: A spatial model checker for declarative image analysis. In Tomás Vojnar and Lijun Zhang, editors, Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part I, volume 11427 of Lecture Notes in Computer Science, pages 281-298. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-17462-0_16.
  7. Patrick Blackburn and Johan van Benthem. Modal logic: a semantic perspective. In Handbook of Modal Logic, pages 1-84. North-Holland, 2007. URL: https://doi.org/10.1016/s1570-2464(07)80004-8.
  8. Luís Caires and Luca Cardelli. A spatial logic for concurrency (Part I). In N. Kobayashi and B. C. Pierce, editors, International Symposium on Theoretical Aspects of Computer Software - TACS 2001, volume 2215 of LNCS, pages 1-37. Springer, 2001. URL: https://doi.org/10.1007/3-540-45500-0_1.
  9. Vincenzo Ciancia, Stephen Gilmore, Gianluca Grilletti, Diego Latella, Michele Loreti, and Mieke Massink. Spatio-temporal model checking of vehicular movement in public transport systems. International Journal on Software Tools for Technology Transfer, 20:289-311, January 2018. URL: https://doi.org/10.1007/s10009-018-0483-8.
  10. Vincenzo Ciancia, Diego Latella, Michele Loreti, and Mieke Massink. Model Checking Spatial Logics for Closure Spaces. Logical Methods in Computer Science, Volume 12, Issue 4, April 2017. URL: https://doi.org/10.2168/LMCS-12(4:2)2016.
  11. Vincenzo Ciancia, Diego Latella, Mieke Massink, and Erik de Vink. Towards spatial bisimilarity for closure models: Logical and coalgebraic characterisations, 2020. URL: http://arxiv.org/abs/2005.05578.
  12. Vincenzo Ciancia, Diego Latella, Mieke Massink, Rytis Paškauskas, and Andrea Vandin. A Tool-Chain for Statistical Spatio-Temporal Model Checking of Bike Sharing Systems. In Tiziana Margaria and Bernhard Steffen, editors, Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques, number 9952 in Lecture Notes in Computer Science, pages 657-673. Springer International Publishing, October 2016. URL: https://doi.org/10.1007/978-3-319-47166-2_46.
  13. E. Allen Emerson and Joseph Y. Halpern. "Sometimes" and "Not Never" Revisited: On Branching Versus Linear Time Temporal Logic. J. ACM, 33(1):151-178, January 1986. URL: https://doi.org/10.1145/4904.4999.
  14. Antony Galton. A generalized topological view of motion in discrete space. Theoretical Computer Science, 305(1):111-134, 2003. URL: https://doi.org/10.1016/S0304-3975(02)00701-6.
  15. Natasha Kurtonina and Maarten de Rijke. Bisimulations for temporal logic. Journal of Logic, Language and Information, 6(4):403-425, 1997. URL: https://doi.org/10.1023/A:1008223921944.
  16. Sven Linker, Fabio Papacchini, and Michele Sevegnani. Analysing spatial properties on neighbourhood spaces, 2020. URL: http://arxiv.org/abs/2007.01266.
  17. Sven Linker and Michele Sevegnani. Target counting with presburger constraints and its application in sensor networks. Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences, 475(2231):20190278, 2019. URL: https://doi.org/10.1098/rspa.2019.0278.
  18. Robin Milner, Joachin Parrow, and David Walker. A Calculus of Mobile Processes, I. Information and Computation, 100(1):1-40, September 1992. URL: https://doi.org/10.1016/0890-5401(92)90008-4.
  19. Eric Pacuit. Neighborhood Semantics for Modal Logic. Springer, Cham, 2017. URL: https://doi.org/10.1007/978-3-319-67149-9.
  20. Danilo Pianini, Simon Dobson, and Mirko Viroli. Self-stabilising target counting in wireless sensor networks using euler integration. In 2017 IEEE 11th International Conference on Self-Adaptive and Self-Organizing Systems (SASO), pages 11-20, September 2017. URL: https://doi.org/10.1109/SASO.2017.10.
  21. Amir Pnueli. The Temporal Logic of Programs. In IEEE Symposium on Foundations of Computer Science - SFCS 1977, pages 46-57. IEEE Computer Society, 1977. URL: https://doi.org/10.1109/SFCS.1977.32.
  22. Lynn Arthur Steen and J. Arthur Seebach, Jr. Counterexamples in Topology. Springer-Verlag, New York, 1978. Reprinted by Dover Publications, New York, 1995. Google Scholar
  23. Alfred Tarski. Der Aussagenkalkül und die Topologie. Fundamenta Mathematicae, 31:103-134, 1938. URL: https://doi.org/10.4064/fm-31-1-103-134.
  24. Eduard Čech, Zdeněk Frolík, and Miroslav Katětov. Topological spaces. Academia, Publishing House of the Czechoslovak Academy of Sciences, 1966. URL: http://eudml.org/doc/277000.
  25. Wallace Alvin Wilson. On quasi-metric spaces. American Journal of Mathematics, 53(3):675-684, 1931. URL: https://doi.org/10.2307/2371174.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail