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.

• Type: Conference
• Year: 2008
• Where: CONCUR
• Authors: Lucia Acciai, Michele Boreale
• Keywords: CONCUR 2008, Distributed And Parallel Computing, Kobayashi's Behavioural Type, Spatial, Type Systems