An Extensional Spatial Logic for Mobile Processes

12 years 11 months ago
An Extensional Spatial Logic for Mobile Processes
Existing spatial logics for concurrency are intensional, in the sense that they induce an equivalence that coincides with structural congruence. In this work, we study a contextual spatial logic for the πcalculus, which lacks the spatial operators to observe emptyness, parallel composition and restriction, and only has composition adjunct and hiding. We show that the induced logical equivalence coincides with strong early bisimilarity. The proof of completeness involves the definition of non-trivial formulas, including characteristic formulas for restriction-free processes up to bisimilarity. This result allows us to isolate the extensional core of spatial logics, decomposing spatial logics into a part that counts (given by the intensional operators) and a part that observes (given by their adjuncts). We also study how enriching the core extensional spatial logic with intensional operators affects its separative power.
Daniel Hirschkoff
Added 01 Jul 2010
Updated 01 Jul 2010
Type Conference
Year 2004
Authors Daniel Hirschkoff
Comments (0)