Spatial and Behavioural types: safety, liveness and decidability

Lucia Acciai, University of Firenze, Italy

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. Types are 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. We then consider decidability of the type system and of certain properties. Using techniques based on well-structured transition systems, we prove that, for an interesting fragment of the considered logic, satisfiability is decidable for types. As a consequence of logical equivalence between types and processes, we obtain decidability of this fragment of the logic for all well-typed pi-processes.