CONCUR 2004 START ConferenceManager    

Elimination of Quantifiers and Undecidability in Spatial Logics for Concurrency

Luis Caires and Etienne Lozes

Presented at Fifteenth International Conference on Concurrency Theory (CONCUR 2004), London, England, 31 August - 3 September, 2004


The introduction of spatial logics in concurrency was motivated by a shift of focus from concurrent systems towards distributed systems. Aiming at a better understanding of the essence of dynamic spatial logics, we study a minimal spatial logic without quantifiers or any operators talking about names. The logic just includes the basic spatial operators void, composition and its adjunct, and the next step modality; for the model we consider a tiny fragment of CCS. We show that this core logic can already encode its own extension with quantifiers, and modalities for actions. From this result, we derive several consequences. Firstly, we establish the intensionality of the logic, we characterize the equivalence it induces on processes, and we derive characteristic formulas. Secondly, we show that, unlike in static spatial logics, the composition adjunct adds to the expressiveness of the logic, so that adjunct elimination is not possible for dynamic spatial logics, even quantifier-free. Finally, we prove that both the model-checking and satisfiability problems are undecidable. We also conclude that our results extend to other calculi, namely the $\pi$-calculus and the ambient calculus.

START Conference Manager (V2.47.4)