University of Oldenburg
4pm Tuesday 11th December 2007
Room 2511, JCMB, King's Buildings
Automata-theoretic representations have proven useful in the automatic and exact analysis of computing systems. We propose a new semantical mapping of Pi-Calculus processes into place/transition Petri nets. Our translation exploits the connections created by restricted names; it yields finite nets for processes with unbounded name and unbounded process creation. For finite Petri nets, well-investigated verification techniques are available.
The property of structural stationarity characterises the processes mapped to finite nets. We provide exact conditions for structural stationarity using the novel characteristic functions of depth and breadth. Referring to the standard interpretation of processes as hypergraphs, we prove that boundedness in depth and in breadth corresponds to boundedness in the length of the simple paths and boundedness of the hyperedge degrees, respectively. This gives an intuitive understanding of structurally stationary processes.
For modelling client-server architectures like the car platooning case study, we design the syntactic class of finite handler processes. Applying our theory, we prove that finite handler processes are structurally stationary. Our Petri net translation facilitates the automatic verification of the car platooning system. We infer occurrence number, temporal, and topological properties using efficient algorithms that exploit the graph structure of the Petri net.
Traditional Petri net constructions for process calculi focus on the concurrency of sequential processes. When comparing these translations with our new semantics, we observe that both finitely represent different classes of processes. We work out a combination of the translations that unifies and extends the two classes. At present, this gives the most expressive class of Pi-Calculus processes that have a finite Petri net representation.
To argue that our semantics is useful for verification, we discuss the aspects we believe constitute a useful semantics: retrievability, finiteness and expressiveness, analysability, and compositionality.