A Spatial Logic for Simplicial Models
From MaRDI portal
Abstract: Collective Adaptive Systems often consist of many heterogeneous components typically organised in groups. These entities interact with each other by adapting their behaviour to pursue individual or collective goals. In these systems, the distribution of these entities determines a space that can be either physical or logical. The former is defined in terms of a physical relation among components. The latter depends on logical relations, such as being part of the same group. In this context, specification and verification of spatial properties play a fundamental role in supporting the design of systems and predicting their behaviour. For this reason, different tools and techniques have been proposed to specify and verify the properties of space, mainly described as graphs. Therefore, the approaches generally use model spatial relations to describe a form of proximity among pairs of entities. Unfortunately, these graph-based models do not permit considering relations among more than two entities that may arise when one is interested in describing aspects of space by involving interactions among groups of entities. In this work, we propose a spatial logic interpreted on simplicial complexes. These are topological objects, able to represent surfaces and volumes efficiently that generalise graphs with higher-order edges. We discuss how the satisfaction of logical formulas can be verified by a correct and complete model checking algorithm, which is linear to the dimension of the simplicial complex and logical formula. The expressiveness of the proposed logic is studied in terms of the spatial variants of classical bisimulation and branching bisimulation relations defined over simplicial complexes.
Cites work
- A dynamic epistemic logic analysis of equality negation and other epistemic covering tasks
- A generalized topological view of motion in discrete space.
- A multiprocess network logic with temporal and spatial modalities
- A rewriting-based model checker for the linear temporal logic of rewriting
- A simplicial complex model for dynamic epistemic logic to study distributed task computability
- A spatial logic for concurrency. I
- An \(O(m\log n)\) algorithm for stuttering equivalence and branching bisimulation
- An Experimental Spatio-Temporal Model Checker
- Analysing Spatial Properties on Neighbourhood Spaces
- Anytime, anywhere: modal logics for mobile ambients
- CCS expressions, finite state processes, and three problems of equivalence
- Digital Topology
- Discrete mereotopology
- Distributed Coverage Verification in Sensor Networks Without Location Information
- Geometric Model Checking of Continuous Space
- Graphical Encoding of a Spatial Logic for the π-Calculus
- Handbook of Spatial Logics
- scientific article; zbMATH DE number 3870578 (Why is no real title available?)
- scientific article; zbMATH DE number 5286861 (Why is no real title available?)
- scientific article; zbMATH DE number 4102053 (Why is no real title available?)
- scientific article; zbMATH DE number 2086655 (Why is no real title available?)
- scientific article; zbMATH DE number 5585443 (Why is no real title available?)
- scientific article; zbMATH DE number 3235051 (Why is no real title available?)
- scientific article; zbMATH DE number 3400923 (Why is no real title available?)
- Introduction to bisimulation and coinduction
- Logic in Computer Science
- Modal logic
- Model checking spatial logics for closure spaces
- On the almighty wand
- Qualitative and quantitative monitoring of spatio-temporal properties with SSTL
- Software-intensive systems and new computing paradigms. Challenges and visions
- Spatial logic and spatial model checking for closure spaces
- Specifying and Verifying Properties of Space
- Tarski's theorem on intuitionistic logic, for polyhedra
- The Temporal Logic of Rewriting: A Gentle Introduction
- Three logics for branching bisimulation
- Topological Semantics and Bisimulations for Intuitionistic Modal Logics and Their Classical Companion Logics
Cited in
(12)- Spatial logics with connectedness predicates
- scientific article; zbMATH DE number 5295702 (Why is no real title available?)
- scientific article; zbMATH DE number 2081098 (Why is no real title available?)
- scientific article; zbMATH DE number 6928613 (Why is no real title available?)
- scientific article; zbMATH DE number 1894261 (Why is no real title available?)
- scientific article; zbMATH DE number 5222366 (Why is no real title available?)
- On the Computational Complexity of Spatial Logics with Connectedness Constraints
- Back-and-forth in space: on logics and bisimilarity in closure spaces
- Minimisation of spatial models using branching bisimilarity
- On bisimilarity for polyhedral models and \texttt{SLCS}
- Weak simplicial bisimilarity and minimisation for polyhedral model checking
- Wanted dead or alive: epistemic logic for impure simplicial complexes
This page was built for publication: A Spatial Logic for Simplicial Models
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6135777)
