Petri net topologies for a specification language

This paper presents a formal technique for enforcing deterministic exec­ution in Petri nets, and proceeds to demonstrate how the resultant topology may be used to enforce partial sequencing so that various sequentially-executing subnets may execute in parallel. Using this sequencing technique, isomorphisms between various programming language constructs and Petri nets are defined. Particular constructs investigated are iteration , concurrency, modularity and data type represen­tation. The intention is to unify the individual subnets to form a single model, which may be studied using classical Petri net analysis techniques. An important application of such a unified model is the detection of deadlock in protocol specifications