Logics of polyhedral reachability
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2024
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866914846774132736 |
|---|---|
| author | Bezhanishvili, Nick Bussi, Laura Ciancia, Vincenzo Fernández-Duque, David Gabelaia, David |
| author_facet | Bezhanishvili, Nick Bussi, Laura Ciancia, Vincenzo Fernández-Duque, David Gabelaia, David |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2406_16056 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Logics of polyhedral reachability Bezhanishvili, Nick Bussi, Laura Ciancia, Vincenzo Fernández-Duque, David Gabelaia, David Logic in Computer Science 03B45 (Primary) 03B70 (Secondary) F.4 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. |
| title | Logics of polyhedral reachability |
| topic | Logic in Computer Science 03B45 (Primary) 03B70 (Secondary) F.4 |
| url | https://arxiv.org/abs/2406.16056 |