Elimination of quantifiers and undecidability in spatial logics for concurrency

Luís Caires, Étienne Lozes

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

10 Citations (Scopus)


Aiming at a deeper understanding of the essence of spatial logics for concurrency, 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 model-checking and satisfiability problems are undecidable in our logic. We also conclude that our results extend to other calculi, namely the π-calculus and the ambient calculus.

Original languageEnglish
Title of host publicationCONCUR 2004 - Concurrency Theory, Proceedings
EditorsP. Gardner, N. Yoshida
Number of pages18
ISBN (Print)3-540-22940-X
Publication statusPublished - 1 Dec 2004
Event15th International Conference on Concurrency Theory - Royal Society, London, United Kingdom
Duration: 31 Aug 20043 Sep 2004

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
ISSN (Print)0302-9743


Conference15th International Conference on Concurrency Theory
CountryUnited Kingdom


  • Semantics
  • Models
  • Bigraphical reactive


Dive into the research topics of 'Elimination of quantifiers and undecidability in spatial logics for concurrency'. Together they form a unique fingerprint.

Cite this