Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Logics of polyhedral reachability

Nick Bezhanishvili, Laura Bussi, Vincenzo Ciancia, David Fernández-Duque, David Gabelaia

TL;DR

This work axiomatizes polyhedral reachability by introducing ${\mathsf{PLR}}$, a modal logic that combines polyhedral semantics with the reachability modality ${\gamma}(\varphi,\psi)$. The authors develop two logics, ${\mathsf{ALR}}$ based on ${\mathsf{S4}}$ and ${\mathsf{PLR}}$ based on ${\mathsf{Grz}}$, and prove their soundness and completeness with respect to polyhedral semantics through a two-stage strategy: first establish the finite model property for ${\mathsf{ALR}}$ on Alexandroff spaces, then lift completeness to the polyhedral setting by showing every satisfiable finite poset formula has a polyhedral witness via the nerve construction. Central to the method is the nerve correspondence between finite posets and polyhedral models, plus a filtration technique that yields finite canonical models. The results provide a rigorous foundation for automated reasoning and model checking on polyhedral spaces (e.g., 3D meshes), enabling precise reasoning about reachability along topological paths. The paper also outlines future directions toward broader topological completeness and applications to optimisation and minimisation in spatial logics.

Abstract

Polyhedral semantics is a recently introduced branch of spatial modal logic, in which modal formulas are interpreted as piecewise linear subsets of an Euclidean space. Polyhedral semantics for the basic modal language has already been well investigated. However, for many practical applications of polyhedral semantics, it is advantageous to enrich the basic modal language with a reachability modality. Recently, a language with an Until-like spatial modality has been introduced, with demonstrated applicability to the analysis of 3D meshes via model checking. In this paper, we exhibit an axiom system for this logic, and show that it is complete with respect to polyhedral semantics. The proof consists of two major steps: First, we show that this logic, which is built over Grzegorczyk's system $\mathsf{Grz}$, has the finite model property. Subsequently, we show that every formula satisfied in a finite poset is also satisfied in a polyhedral model, thereby establishing polyhedral completeness.

Logics of polyhedral reachability

TL;DR

This work axiomatizes polyhedral reachability by introducing , a modal logic that combines polyhedral semantics with the reachability modality . The authors develop two logics, based on and based on , and prove their soundness and completeness with respect to polyhedral semantics through a two-stage strategy: first establish the finite model property for on Alexandroff spaces, then lift completeness to the polyhedral setting by showing every satisfiable finite poset formula has a polyhedral witness via the nerve construction. Central to the method is the nerve correspondence between finite posets and polyhedral models, plus a filtration technique that yields finite canonical models. The results provide a rigorous foundation for automated reasoning and model checking on polyhedral spaces (e.g., 3D meshes), enabling precise reasoning about reachability along topological paths. The paper also outlines future directions toward broader topological completeness and applications to optimisation and minimisation in spatial logics.

Abstract

Polyhedral semantics is a recently introduced branch of spatial modal logic, in which modal formulas are interpreted as piecewise linear subsets of an Euclidean space. Polyhedral semantics for the basic modal language has already been well investigated. However, for many practical applications of polyhedral semantics, it is advantageous to enrich the basic modal language with a reachability modality. Recently, a language with an Until-like spatial modality has been introduced, with demonstrated applicability to the analysis of 3D meshes via model checking. In this paper, we exhibit an axiom system for this logic, and show that it is complete with respect to polyhedral semantics. The proof consists of two major steps: First, we show that this logic, which is built over Grzegorczyk's system , has the finite model property. Subsequently, we show that every formula satisfied in a finite poset is also satisfied in a polyhedral model, thereby establishing polyhedral completeness.

Paper Structure

This paper contains 13 sections, 21 theorems, 6 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Alexandroff spaces and polyhedra
  3. Topological and Alexandroff spaces
  4. Simplicial complexes and polyhedra
  5. Language and semantics
  6. Language with reachability modality
  7. Topological and polyhedral semantics
  8. The nerve of a Kripke model
  9. Logics of reachability
  10. Alexandroff completeness
  11. Filtration
  12. Polyhedral completeness
  13. Conclusions

Key Result

lemma 1

Each point of $| K |$ belongs to the relative interior of exactly one simplex in $K$. That is, $K^\circ = \{ \sigma^\circ \mid \sigma \in K \}$ is a partition of $|K|$.

Figures (1)

  • Figure 1: Example of a polyhedral model depicting a maze, a starting area (in red), exit areas (in green), safe places (white), and a 'path' witnessing that from the starting area, an exit can be safely reached. All the points in the red area make the formula $\texttt{red}\land \gamma(\texttt{red}\lor\texttt{corridor}\lor\texttt{white},\texttt{green})$ true.

Theorems & Definitions (56)

  • definition 1
  • definition 2
  • definition 3
  • lemma 1
  • definition 4
  • definition 5
  • definition 6
  • definition 7
  • definition 8
  • definition 9
  • ...and 46 more