Decision Problems for Spatial Logics Revisited

Spatial Logics are modal logics developed for process-algebraic semantics. They have been proposed for specifying concurrent properties of dynamic systems and have been proved useful in a wide range of applications. Their expresivity often comes with the price of undecidability, however, even against finite fragments of process calculi. This paper investigates the decidability of satisfiability, validity, and model checking for various Spatial Logics against semantics based on a fragment of CCS that embodies the core features of concurrent behaviors. We prove some decidability and undecidability prop- erties for (combinations of) basic modal operators of spatial logics that entail some of the already known results in the field and provide a taxonomy for this class of problems.