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

摘要

In the pi-calculus, we consider the decidability of model checking properties expressed in Shallow Logic, a simple spatial logic. We first introduce a behavioural type system that, given a pi-process P that might in general be infinite-control, tries to extract a spatial-behavioural type T, in the form of a ccs term that is logically equivalent to P. Employing techniques based on well-structured transition systems (wsts), we prove that model checking (T |= φ) is decidable for types, for a fragment of the logic that can be used to encode interesting safety and reachability properties. The wsts technique we rely upon requires first endowing the considered transition system with a well-quasi order, then defining a finite basis for the denotation of each formula. This is achieved by viewing types as forests, with a well-quasi order that corresponds to a form of forest embedding. As a consequence of the logical equivalence between types and processes, we obtain the decidability of the considered fragment of the logic for well-typed pi-processes. We discuss (un)decidability and complexity of model checking also outside the considered decidable fragment of Shallow Logic.