The work described in this paper builds on the polyhedral semantics of the Spatial Logic for Closure Spaces (SLCS) and the geometric spatial model checker PolyLogicA. Polyhedral models are central in domains that exploit mesh processing, such as 3D computer graphics. A discrete representation of polyhedral models is given by cell poset models, which are amenable to geometric spatial model checking on polyhedral models using the logical language SLCS$η$, a weaker version of SLCS. In this work we show that the mapping from polyhedral models to cell poset models preserves and reflects SLCS$η$. We also propose weak simplicial bisimilarity on polyhedral models and weak $\pm$-bisimilarity on cell poset models, where by ``weak'' we mean that the relevant equivalence is coarser than the corresponding one for SLCS, leading to a greater reduction of the size of models and thus to more efficient model checking. We show that the proposed bisimilarities enjoy the Hennessy-Milner property, i.e. two points are weakly simplicial bisimilar iff they are logically equivalent for SLCS$η$. Similarly, two cells are weakly $\pm$-bisimilar iff they are logically equivalent in the poset-model interpretation of SLCS$η$. Furthermore we present a model minimisation procedure and prove that it correctly computes the minimal model with respect to weak $\pm$-bisimilarity, i.e. with respect to logical equivalence of SLCS$η$. The procedure works via an encoding into LTSs and then exploits branching bisimilarity on those LTSs, exploiting the minimisation capabilities as included in the mCRL2 toolset. Various examples show the effectiveness of the approach.

Abstract We investigate a recently devised polyhedral semantics for intermediate logics, in which formulas are interpreted in n-dimensional polyhedra. An intermediate logic is polyhedrally complete if it is complete with respect to some class of polyhedra. The first main result of this paper is a necessary and sufficient condition for the polyhedral completeness of a logic. This condition, which we call the Nerve Criterion, is expressed in terms of Alexandrov’s notion of the nerve of a poset. It affords a purely combinatorial characterisation of polyhedrally complete logics. Using the Nerve Criterion we show, easily, that there are continuum many intermediate logics that are not polyhedrally complete but which have the finite model property. We also provide, at considerable combinatorial labour, a countably infinite class of logics axiomatised by the Jankov–Fine formulas of ‘starlike trees’ all of which are polyhedrally complete. The polyhedral completeness theorem for these ‘starlike logics’ is the second main result of this paper.

Topological Spatial Model Checking is a recent paradigm where model checking techniques are developed for the topological interpretation of Modal Logic. The Spatial Logic of Closure Spaces, SLCS, extends Modal Logic with reachability connectives that, in turn, can be used for expressing interesting spatial properties, such as "being near to" or "being surrounded by". SLCS constitutes the kernel of a solid logical framework for reasoning about discrete space, such as graphs and digital images, interpreted as quasi discrete closure spaces. Following a recently developed geometric semantics of Modal Logic, we propose an interpretation of SLCS in continuous space, admitting a geometric spatial model checking procedure, by resorting to models based on polyhedra. Such representations of space are increasingly relevant in many domains of application, due to recent developments of 3D scanning and visualisation techniques that exploit mesh processing. We introduce PolyLogicA, a geometric spatial model checker for SLCS formulas on polyhedra and demonstrate feasibility of our approach on two 3D polyhedral models of realistic size. Finally, we introduce a geometric definition of bisimilarity, proving that it characterises logical equivalence.

Abstract It is a celebrated result of McKinsey and Tarski [28] thatS4is the logic of the closure algebraΧ+over any dense-in-itself separable metrizable space. In particular,S4is the logic of the closure algebra over the realsR, the rationalsQ, or the Cantor spaceC. By [5], each logic aboveS4that has the finite model property is the logic of a subalgebra ofQ+, as well as the logic of a subalgebra ofC+. This is no longer true forR, and the main result of [5] states that each connected logic aboveS4with the finite model property is the logic of a subalgebra of the closure algebraR+. In this paper we extend these results to all logics aboveS4. Namely, for a normal modal logicL, we prove that the following conditions are equivalent: (i)Lis aboveS4, (ii)Lis the logic of a subalgebra ofQ+, (iii)Lis the logic of a subalgebra ofC+. We introduce the concept of a well-connected logic aboveS4and prove that the following conditions are equivalent: (i)Lis a well-connected logic, (ii)Lis the logic of a subalgebra of the closure algebra $\xi _2^ + $ over the infinite binary tree, (iii)Lis the logic of a subalgebra of the closure algebra ${\bf{L}}_2^ + $ over the infinite binary tree with limits equipped with the Scott topology. Finally, we prove that a logicLaboveS4is connected iffLis the logic of a subalgebra ofR+, and transfer our results to the setting of intermediate logics. Proving these general completeness results requires new tools. We introduce the countable general frame property (CGFP) and prove that each normal modal logic has the CGFP. We introduce general topological semantics forS4, which generalizes topological semantics the same way general frame semantics generalizes Kripke semantics. We prove that the categories of descriptive frames forS4and descriptive spaces are isomorphic. It follows that every logic aboveS4is complete with respect to the corresponding class of descriptive spaces. We provide several ways of realizing the infinite binary tree with limits, and prove that when equipped with the Scott topology, it is an interior image of bothCandR. Finally, we introduce gluing of general spaces and prove that the space obtained by appropriate gluing involving certain quotients ofL2is an interior image ofR.

We introduce pairwise Stone spaces as a bitopological generalisation of Stone spaces – the duals of Boolean algebras – and show that they are exactly the bitopological duals of bounded distributive lattices. The categoryPStoneof pairwise Stone spaces is isomorphic to the categorySpecof spectral spaces and to the categoryPriesof Priestley spaces. In fact, the isomorphism ofSpecandPriesis most naturally seen throughPStoneby first establishing thatPriesis isomorphic toPStone, and then showing thatPStoneis isomorphic toSpec. We provide the bitopological and spectral descriptions of many algebraic concepts important in the study of distributive lattices. We also give new bitopological and spectral dualities for Heyting algebras, thereby providing two new alternatives to Esakia's duality.

In this paper, we construct and investigate a hierarchy of spatio-temporal formalisms that result from various combinations of propositional spatial and temporal logics such as the propositional temporal logic PTL, the spatial logics RCC-8, BRCC-8, S4u and their fragments. The obtained results give a clear picture of the trade-off between expressiveness and `computational realisability' within the hierarchy. We demonstrate how different combining principles as well as spatial and temporal primitives can produce NP-, PSPACE-, EXPSPACE-, 2EXPSPACE-complete, and even undecidable spatio-temporal logics out of components that are at most NP- or PSPACE-complete.

Abstract We solve a major open problem concerning algorithmic properties of products of ‘transitive’ modal logics by showing that products and commutators of such standard logics asK4,S4,S4.1,K4.3,GL, orGrzare undecidable and do not have the finite model property. More generally, we prove that no Kripke complete extension of the commutator [K4, K4] with product frames of arbitrary finite or infinite depth (with respect to both accessibility relations) can be decidable. In particular, ifl1andl2are classes of transitive frames such that their depth cannot be bounded by any fixedn< ω, then the logic of the class {5ℑ1× ℑ2∣ ℑ1∈l1, ℑ2, ∈l2} is undecidable. (On the contrary, the product of, say,K4and the logic of all transitive Kripke frames of depth ≤n, for some fixedn< ω, is decidable.) The complexity of these undecidable logics ranges from r.e. to co-r.e. and Π11-complete. As a consequence, we give the first known examples of Kripke incomplete commutators of Kripke complete logics.