CONCUR 2004 START ConferenceManager    

An Extensional Spatial Logic for Mobile Processes

Daniel Hirschkoff

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


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 pi-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.

START Conference Manager (V2.47.4)