Spatial and Behavioral Types in the Pi-Calculus

12 years 11 months ago
Spatial and Behavioral Types in the Pi-Calculus
We present a framework that combines ideas from spatial logics and Igarashi and Kobayashi's behavioural type systems, drawing benefits from both. In our approach, type systems for the pi-calculus are introduced where newly declared (restricted) names are annotated with spatial process properties, predicating on those names, that are expected to hold in the scope of the declaration. e akin to CCS terms and account for the processes abstract behaviour and "shallow" spatial structure. The type systems relies on spatial model checking, but properties are checked against types rather than against processes. The considered class of properties is rather general and, differently from previous proposals, includes both safety and liveness ones, and is not limited to invariants.
Lucia Acciai, Michele Boreale
Added 18 Oct 2010
Updated 18 Oct 2010
Type Conference
Year 2008
Authors Lucia Acciai, Michele Boreale
Comments (0)