Deciding safety properties in infinite-state Pi-calculus via behavioural types

Abstract

In the pi-calculus, we consider decidability of certain safety properties expressed in a simple spatial logic. We first introduce a behavioural type system that, given a process P, tries to extract a spatial-behavioural type T, in the form of a ccs term that is logically equivalent to the given process. Using techniques based on well-structured transition systems, we then prove that, for an interesting fragment of the considered logic, satisfiability (T≠phi;) 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. © 2009 Springer Berlin Heidelberg.