Source-linked AI summary
Dynamic Polyhedral Logic
Nick Bezhanishvili, Laura Bussi, Vincenzo Ciancia, David Fernández-Duque, David Gabelaia
TL;DR
The paper addresses how to combine geometry-sensitive polyhedral semantics with path-based reachability and invertible temporal dynamics. It defines the corresponding h-dynamic reachability systems and proves soundness and completeness for topological, finite, Alexandroff, and polyhedral classes, including a rotation subclass in the polyhedral case.
Problem
Ordinary dynamic topological semantics can be too coarse for geometric information, while reachability and invertible dynamics require a combined formal framework.
Method
The paper interprets formulas over admissible polyhedral regions, treats γ as path-based reachability, and interprets temporal modalities through a PL-homeomorphism and its inverse.
Results
The resulting h-dynamic reachability logics are sound and complete for their intended topological, finite, Alexandroff, and polyhedral classes, with polyhedral completeness already holding for rotations.
Takeaways & Limitations
Polyhedral semantics, spatial reachability, and invertible dynamics can be combined into axiomatized logics for reasoning about evolving geometric systems.
Takeaways & Limitations
The paper leaves open the appropriate dynamic polyhedral logic for non-invertible continuous systems and for infinitary temporal operators such as eventually.
Abstract
from arXiv · showhide
We introduce spatio-temporal polyhedral reachability logics, extending dynamic topological logic with polyhedral semantics and a path-based spatial reachability operator. Formulas are interpreted over polyhedra, with admissible valuations ranging over polyhedral subsets; the spatial modality is interpreted as interior, the binary operator $γ(\varphi,ψ)$ expresses reachability of a $ψ$-point through a $\varphi$-region, and the temporal modalities are interpreted by a PL-homeomorphism and its inverse. We define h-dynamic reachability spaces and axiomatize the corresponding h-dynamic extensions of the known reachability logics of topological, finite, Alexandroff, and polyhedral spaces. The main result is soundness and completeness for the intended classes of invertible dynamical systems.
1 Introduction
The paper extends dynamic topological logic with geometry-sensitive polyhedral semantics, path-based reachability, and invertible temporal dynamics. It develops axiomatizations and completeness results for these combined systems.
- Motivation: Ordinary topological semantics can be too coarse for genuinely geometric information, motivating polyhedral semantics based on admissible polyhedral regions.Polyhedral models connect logical reasoning with finite simplicial decompositions and piecewise-linear geometry.
- Spatial reachability: The reachability operator γ(φ,ψ) expresses whether a ψ-point is reachable through a φ-region, functioning as a spatial analogue of Until.It enables properties such as connectivity, containment, surroundedness, and safe reachability.
- Contribution: The paper combines polyhedral semantics, spatial reachability, and invertible dynamics using a PL-homeomorphism and its inverse as temporal operators.The resulting models support spatial properties of systems evolving over time.
- Method: Temporal operators can be pushed to the propositional level, reducing completeness of the full spatio-temporal systems to completeness of their spatial fragments.The translation preserves the structure needed for the polyhedral setting.
- Completeness construction: In the polyhedral case, completeness is reconstructed geometrically by arranging finitely many copies of a polyhedron around a periodic orbit, with rotation dynamics possible.This extends the result from arbitrary PL-homeomorphisms to a particularly transparent subclass.
2 Language and Algebraic Semantics
The paper defines a spatio-temporal language over reachability algebras, where admissible regions support Boolean operations, interior, and path-based reachability. Invertible dynamics preserve these admissible regions and interpret forward and backward temporal modalities.
- Language: The spatio-temporal language contains propositional variables, Boolean connectives, the interior modality □, reachability γ, and forward and backward temporal operators.The spatial fragment omits the two temporal operators.
- Reachability semantics: The operator γ(φ,ψ) holds when a continuous path reaches a ψ-point while all intermediate points satisfy φ.Its algebraic interpretation collects starting points admitting such paths.
- Reachability algebras: A reachability algebra is closed under finite Boolean operations, topological interior, and the reachability operation γ.These closure conditions ensure that admissible valuations remain interpretable.
- Invertible dynamics: An h-dynamic reachability space uses a homeomorphism whose image operation preserves admissibility in both directions.The prefix h denotes homeomorphism and therefore invertible dynamics.
- Models: An h-dynamic reachability model combines a reachability model with an h-dynamic reachability space and evaluates formulas through inductively defined truth sets.The modal clauses interpret □ as interior and temporal operators through f and f^-1.
3 The Algebras of Polyhedral Subsets
The paper builds polyhedral semantics from finite simplicial decompositions and defines admissible regions as finite unions of open cells. These regions support the required algebraic operations and path-based reachability.
- Polyhedral foundations: A polyhedron is a finite union of polytopes, including points, segments, triangles, tetrahedra, and higher-dimensional analogues.The paper represents these structures through simplices and simplicial complexes.
- Simplicial complexes: A simplicial complex is a finite collection of simplices closed under faces and with compatible intersections, whose union forms its underlying polyhedron.Its simplices induce a decomposition into open cells.
- Cell decomposition: Every point of a polyhedron belongs to exactly one open cell, so triangulations partition the space into relative interiors of simplices.This cell structure supports the definition of polyhedral subsets.
- Polyhedral sets: A polyhedral set is a finite union of open cells from some triangulation, allowing semantics to vary across suitable simplicial decompositions.The collection of all such subsets is denoted PL(P).
- Algebraic closure: PL(P) forms a Boolean algebra and is closed under topological interior and closure.These structural properties support admissible spatial semantics.
- Reachability and dynamics: For polyhedral models, continuous-path reachability can be represented using PL paths, and γ applied to polyhedral sets remains polyhedral.Together with PL-homeomorphisms, this makes (P, PL(P), f) an h-dynamic reachability space.
4 The Axiomatic Systems
The paper extends established reachability logics with temporal and spatio-temporal axioms for h-dynamic topological, finite, Alexandroff, and polyhedral spaces. It proves the resulting systems sound, with key interaction principles supported by continuity and invertibility of the dynamics.
- Axiomatic extensions: An h-dynamic polyhedral space consists of a polyhedron equipped with a PL-homeomorphism, while the general h-dynamic setting uses a homeomorphism.Finite and Alexandroff h-dynamic classes are defined analogously.
- Axiomatic extensions: Established reachability logics are extended with temporal and spatio-temporal axioms in the full language.The extensions include TLR, ALR, and PLR as their respective base systems.
- Soundness and interaction: Continuity of the homeomorphism and its inverse preserves the path-based reachability conditions used in the interaction-axiom soundness proof.A witnessing path is mapped through the dynamics to obtain a corresponding witnessing path.
- Soundness and interaction: The interaction axioms make reachability and temporal modalities commute appropriately with the dynamics and its inverse.The corresponding derivable equivalences are established for reachability and both temporal directions.
- Soundness and interaction: The systems hD-TLR, hD-ALR, and hD-PLR are sound for the corresponding topological, finite, Alexandroff, and polyhedral h-dynamic classes.The theorem covers hD-TLR for h𝔇𝔗, hD-ALR for h𝔇𝔉 and h𝔇𝔄, and hD-PLR for h𝔇𝔓.
5 Completeness of h-Dynamic Reachability Logics
The completeness proof translates temporal formulas into equivalent spatial reachability formulas with temporal shifts attached only to atoms, then reconstructs invertible models from the translated formulas. In the polyhedral case, the reconstruction uses finitely many rotated copies and yields completeness even for rotational dynamics.
- Translation to simple formulas: The structural transformation g preserves Boolean, spatial, and reachability structure while moving temporal operators to near-atoms.Near-atoms are formulas n p, and simple formulas are built from them using Boolean connectives, □, and γ.
- Translation to simple formulas: Mixed forward and backward temporal prefixes are reduced to a single-direction sequence using inverse axioms before temporal shifts are attached to propositional variables.The transformation combines temporal shifts along each formula branch, including cancellation of opposite shifts and accumulation in one direction.
- Model reconstruction: Completeness is obtained by constructing an h-dynamic model of φ from a model of g(φ), with the number of copies determined by φ’s maximal temporal depth.For topological, finite, and Alexandroff models, the construction uses X × I_n, where the dynamics cyclically permutes copies and remains a homeomorphism.
- Polyhedral reconstruction: In the polyhedral case, a model is reconstructed from finitely many disjoint rotated copies of the original polyhedron, with valuations formed from finite unions of rotated polyhedral subsets.The rotation is piecewise-linear, cyclically permutes the copies, and preserves admissibility of the reconstructed valuation.
- Completeness results: The resulting systems are sound and complete for topological, finite, Alexandroff, and polyhedral classes; polyhedral completeness already holds for systems whose dynamics is a rotation.The polyhedral countermodel construction applies Lemma 5.5 to the negation of a formula.
6 Conclusions and Further Work
The paper combines backward temporal modalities, polyhedral semantics, and spatial reachability, while identifying open completeness, decidability, and finite-axiomatizability questions for broader variants.
- The paper combines homeomorphism-based past modalities, polyhedral semantics, and spatial reachability, and axiomatizes dynamic reachability logics across several space classes.
- The past-free fragment is conjectured sound and complete for continuous, possibly non-invertible dynamics, but reachability introduces technical challenges.
- Completeness of back-free dynamic polyhedral reachability logic for polyhedra with a PL endofunction remains an open question.
- Existing results for DTL with eventually include undecidability and non-finite axiomatizability, while finite iterations are decidable and have the finite model property.
- Open problems ask about completeness over dynamic scattered or hereditarily irresolvable spaces, decidability for finite spaces, and finite axiomatizability with finite iterations.
- Because eventually is an infinite union that generally fails to produce polyhedral sets, the appropriate polyhedral DTL with infinitary tenses remains theoretically unresolved.