A complete axiomatic system for process-based spatial logic

Radu Mardare, Alberto Policriti

Research output: Contribution to journalConference articlepeer-review

3 Citations (Scopus)


The process-based Spatial Logics are multi-modal logics developed for semantics on Process Algebras and designed to specify concurrent 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 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 propose a sound-complete Hilbert-style axiomatic system for it.
Original languageEnglish
Pages (from-to)491–502
Number of pages12
JournalLecture Notes in Computer Science
Publication statusPublished - 2008
Event33rd International Symposium, Mathematical Foundations of Computer Science, MFCS 2008 - Torun, Poland
Duration: 25 Aug 200829 Aug 2008


  • model check
  • modal logic
  • process semantic
  • operational semantic
  • axiomatic system


Dive into the research topics of 'A complete axiomatic system for process-based spatial logic'. Together they form a unique fingerprint.

Cite this