PETRI-NET-BASED DEADLOCK ANALYSIS OF PROCESS ALGEBRA PROGRAMS

Recent research has been conducted on representing Process Algebra programs by safe Petri nets. We suggest that such a representation offers direct benefits: one can use methods that have been developed in the Petri net theory domain, to reason about Process Algebra programs. We propose for a subset of a specific Process Algebra (Milner's Calculus of Communicating Systems or CCS), a deadlock detection algorithm which is based on Petri net reduction techniques. The Petri net model of a CCS program is transformed into a simpler one which contains a smaller number of states, without losing however any deadlock information. An implementation of the proposed technique confirms that net-based verification of processes is a promising area of research.