A theory of structural stationarity in the π -Calculus

摘要

Automata-theoretic representations have proven useful in the automatic and exact analysis of computing systems. We propose a new semantical mapping of π -Calculus processes into place/transition Petri nets. Our translation exploits the connections created by restricted names and can yield finite nets even for processes with unbounded name and unbounded process creation. The property of structural stationarity characterises the processes mapped to finite nets. We provide exact conditions for structural stationarity using novel characteristic functions. As application of the theory, we identify a rich syntactic class of structurally stationary processes, called finite handler processes. Our Petri net translation facilitates the automatic verification of a case study modelled in this class.