Document Open Access Logo

Finite Models for a Spatial Logic with Discrete and Topological Path Operators

Authors Sven Linker , Fabio Papacchini , Michele Sevegnani

PDF

File

Thumbnail PDF
PDF
LIPIcs.MFCS.2021.72.pdf
  • Filesize: 0.69 MB
  • 16 pages

Document Identifiers

Subject Classification

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

Metrics

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

Abstract

This paper analyses models of a spatial logic with path operators based on the class of neighbourhood spaces, also called pretopological or closure spaces, a generalisation of topological spaces. For this purpose, we distinguish two dimensions: the type of spaces on which models are built, and the type of allowed paths. For the spaces, we investigate general neighbourhood spaces and the subclass of quasi-discrete spaces, which closely resemble graphs. For the paths, we analyse the cases of quasi-discrete paths, which consist of an enumeration of points, and topological paths, based on the unit interval. We show that the logic admits finite models over quasi-discrete spaces, both with quasi-discrete and topological paths. Finally, we prove that for general neighbourhood spaces, the logic does not have the finite model property, either for quasi-discrete or topological paths.

Cite As Get BibTex

Sven Linker, Fabio Papacchini, and Michele Sevegnani. Finite Models for a Spatial Logic with Discrete and Topological Path Operators. In 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 202, pp. 72:1-72:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/LIPIcs.MFCS.2021.72

Author Details

Sven Linker
  • Lancaster University in Leipzig, Germany
Fabio Papacchini
  • University of Liverpool, UK
Michele Sevegnani
  • University of Glasgow, UK

Funding

  • Papacchini, Fabio: partly supported by the EPSRC through grants EP/R026084 and EP/R026173.
  • Sevegnani, Michele: supported by the EPSRC under PETRAS SRF grant MAGIC (EP/S035362/1).

References

  1. 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.
  2. Yuliy Baryshnikov and Robert Ghrist. Target enumeration via euler characteristic integrals. SIAM J. Appl. Math., 70(3):825-844, 2009. URL: https://doi.org/10.1137/070687293.
  3. Nick Bezhanishvili, Vincenzo Ciancia, David Gabelaia, Gianluca Grilletti, Diego Latella, and Mieke Massink. Geometric model checking of continuous space. CoRR, abs/2105.06194, 2021. URL: http://arxiv.org/abs/2105.06194.
  4. Patrick Blackburn, Maarten de Rijke, and Yde Venema. Modal Logic. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2001. URL: https://doi.org/10.1017/CBO9781107050884.
  5. Peter Bubenik and Nikola Milićević. Applied topology using Čech’s closure spaces, 2021. URL: http://arxiv.org/abs/2104.10206.
  6. Fabrizio Banci Buonamici, Gina Belmonte, Vincenzo Ciancia, Diego Latella, and Mieke Massink. Spatial logics and model checking for medical imaging. Int. J. Softw. Tools Technol. Transf., 22(2):195-217, 2020. URL: https://doi.org/10.1007/s10009-019-00511-9.
  7. Davide Castelnovo and Marino Miculan. Closure hyperdoctrines, with paths. CoRR, abs/2007.04213, 2020. URL: http://arxiv.org/abs/2007.04213.
  8. Gustave Choquet. Convergences. Annales de l'université de Grenoble. Nouvelle série. Section sciences mathématiques et physiques, 23:57-112, 1947-1948. URL: http://www.numdam.org/item/AUG_1947-1948__23__57_0/.
  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, Gianluca Grilletti, Diego Latella, Michele Loreti, and Mieke Massink. An experimental spatio-temporal model checker. In Software Engineering and Formal Methods. SEFM 2015, volume 9509 of Lecture Notes in Computer Science. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-49224-6_24.
  11. 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, 2017. URL: https://doi.org/10.2168/LMCS-12(4:2)2016.
  12. 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.
  13. M. E. Coniglio, A. Sernadas, and C. Sernadas. Preservation by fibring of the finite model property. Journal of Logic and Computation, 21(2):375-402, 2011. URL: https://doi.org/10.1093/logcom/exq022.
  14. Szymon Dolecki and Frédéric Mynard. Convergence Foundations of Topology. World Scientific, 2016. URL: https://doi.org/10.1142/9012.
  15. E. Allen Emerson and Jai Srinivasan. Branching time temporal logic. In J. W. de Bakker, W. P. de Roever, and G. Rozenberg, editors, Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, pages 123-172, Berlin, Heidelberg, 1989. Springer Berlin Heidelberg. Google Scholar
  16. D. C. Kent and Won Keun Min. Neighborhood spaces. International Journal of Mathematics and Mathematical Sciences, 32(7):387-399, 2002. URL: https://doi.org/10.1155/S0161171202202203.
  17. Christine Largeron and Stéphane Bonnevay. A pretopological approach for structural analysis. Information Sciences, 144(1-4):169-185, 2002. Google Scholar
  18. Sven Linker, Fabio Papacchini, and Michele Sevegnani. Analysing spatial properties on neighbourhood spaces. In Javier Esparza and Daniel Král', editors, 45th International Symposium on Mathematical Foundations of Computer Science, MFCS 2020, August 24-28, 2020, Prague, Czech Republic, volume 170 of LIPIcs, pages 66:1-66:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.MFCS.2020.66.
  19. 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.
  20. Antonio Rieser. Čech closure spaces: A unified framework for discrete and continuous homotopy. Topology and its Applications, 296:107613, 2021. URL: https://doi.org/10.1016/j.topol.2021.107613.
  21. 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
  22. Christos Tsigkanos, Timo Kehrer, and Carlo Ghezzi. Modeling and verification of evolving cyber-physical spaces. In Matthias Tichy, Eric Bodden, Marco Kuhrmann, Stefan Wagner, and Jan-Philipp Steghöfer, editors, Software Engineering und Software Management 2018, Fachtagung des GI-Fachbereichs Softwaretechnik, SE 2018, 5.-9. März 2018, Ulm, Germany, volume P-279 of LNI, pages 113-114. Gesellschaft für Informatik, 2018. URL: https://dl.gi.de/20.500.12116/16369.
  23. Eduard Čech. Topological spaces. Academia, Publishing House of the Czechoslovak Academy of Sciences, 1966. Edited by Zdeněk Frolík and Miroslav Katětov. Google Scholar
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
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact