Geometric Model Checking of Continuous Space

DOI10.46298/lmcs-18(4:7)2022OpenAlexW3160215750MaRDI QIDQ5060193

Nick Bezhanishvili, David Gabelaia, Gianluca Grilletti, Vincenzo Ciancia, Diego Latella, Mieke Massink

Publication date: 9 January 2023

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/2105.06194v5

zbMATH Keywords

simplicial complexesmodel checkinggeometric logicspatial logic

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Related Items

Geometric Model Checking of Continuous Space, A Spatial Logic for Simplicial Models, Back-and-forth in space: on logics and bisimilarity in closure spaces, Minimisation of spatial models using branching bisimilarity

Uses Software

• HyTech
• MeshLab

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The Simplex Tree: An Efficient Data Structure for General Simplicial Complexes
• Characterizing finite Kripke structures in propositional temporal logic
• Bisimulations for temporal logic
• Tarski's theorem on intuitionistic logic, for polyhedra
• Continuous-time models for system design and analysis
• The algebra of topology
• Spatial Logic and Spatial Model Checking for Closure Spaces
• Model Checking Spatial Logics for Closure Spaces
• SpaTeL
• Specifying and Verifying Properties of Space
• Discrete Mereotopology
• Counterexample-Guided Refinement of Template Polyhedra
• Handbook of Spatial Logics
• Zonotope/Hyperplane Intersection for Hybrid Systems Reachability Analysis
• Three logics for branching bisimulation
• An Experimental Spatio-Temporal Model Checker
• Geometric Model Checking of Continuous Space
• Analysing Spatial Properties on Neighbourhood Spaces
• An O ( m log n ) Algorithm for Computing Stuttering Equivalence and Branching Bisimulation
• Symbolic Model Checking of Hybrid Systems Using Template Polyhedra