technical report Towards a Complete Axiomatization for Spatial Logic


Abstract

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

Authors

R. Mardare,  A. Policriti

Download

/var/papers/TR/TR-21-2008.pdf

Language

English
.