technical report Towards a Complete Axiomatization for Spatial Logic


The process-based Spatial Logics are multi-modal logics de- veloped for semantics on Process Algebras and designed to specify con- current properties of dynamic systems. On the syntactic level, they com- bine modal operators similar to operators of Hennessy-Milner logic, dy- namic logic, arrow logic, relevant logic, or linear logic. This combina- tion generates expressive logics, sometimes undecidable, for which a wide range of applications have been proposed. In the literature, there exist some sound proof systems for spatial logics, but the problem of completeness against process-algebraic semantics is still open. The main goal of this paper is to identify a sound-complete axiomatization for such a logic. We focus on a particular spatial logic that combines the basic spatial operators with dynamic and classical operators. The semantics is based on a fragment of CCS calculus that embodies the core features of concurrent behaviors. We prove the logic decidable both for satisfiability/validity and mode-checking, and we pro- pose a sound-complete Hilbert-style axiomatic system for it.

Paper Details


R. Mardare,  A. Policriti