Graphical encoding of a spatial logic for the pi-calculus

Fabio Gadducci, Alberto Lluch Lafuente

Research output: Contribution to journalConference articleResearchpeer-review


This paper extends our graph-based approach to the verification of spatial properties of pi-calculus specifications. The mechanism is based on an encoding for mobile calculi where each process is mapped into a graph (with interfaces) such that the denotation is fully abstract with respect to the usual structural congruence, i.e., two processes are equivalent exactly when the corresponding encodings yield isomorphic graphs. Behavioral and structural properties of pi-calculus processes expressed in a spatial logic can then be verified on the graphical encoding of a process rather than on its textual representation. In this paper we introduce a modal logic for graphs and define a translation of spatial formulae such that a process verifies a spatial formula exactly when its graphical representation verifies the translated modal graph formula.
Original languageEnglish
JournalElectronic Notes in Theoretical Computer Science
Pages (from-to)209-225
Number of pages17
Publication statusPublished - 2005
Externally publishedYes
Event1st Workshop on Graph Transformation for Verification and Concurrency - San Francisco, CA, United States
Duration: 22 Aug 2005 → …
Conference number: 1


Conference1st Workshop on Graph Transformation for Verification and Concurrency
CountryUnited States
CitySan Francisco, CA
Period22/08/2005 → …



Fingerprint Dive into the research topics of 'Graphical encoding of a spatial logic for the pi-calculus'. Together they form a unique fingerprint.

Cite this