Partial Order Reduction for Verification of Spatial Properties of Pi-Calculus Processes

Mechanical tools have recently been developed that enable computer-aided ver- ification of spatial properties of concurrent systems. To be practical, these tools are expected to deal with the state-space explosion problem. In order to alleviate this problem, we investigate partial order reduction techniques. The main problem is that spatial logics are very expressive and some spatial formulas actually pre- vent partial order reduction. In this paper, we focus on the spatial properties of structure and reduction (mainly the composition formula, the temporal modality, and the guarantee formula): we recast the issue of partial order reduction in terms of process calculi, identify problems with standard definitions of spatial formulas, introduce adequate restrictions, and propose fragments of spatial logics for which we show that partial order reduction holds. Technically, our approach relies on exploiting partially confluent communications and on identifying so-called invisible communications.