A Complete Axiomatic System for Process-based Spatial Logic

Abstract. The process-based Spatial Logics are multi-modal logics de-veloped for semantics on Process Algebras and designed to specify concur-rent properties of dynamic systems. On the syntactic level, they combine modal operators similar to operators of Hennessy-Milner logic, dynamic logic, arrow logic, relevant logic, or linear logic. This combination gener-ates 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 log-ics, 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.