TOWARDS Z SPECIFICATION OF PLACE TRANSITION NETS

Petri net formalism has dynamics and it is well suited for distributed or concurrent systems. However, it has a graphical representation in the form of a bipartite graph through which the type of data cannot be identified. This paper presents the Z specification of the net structure of place transition nets to provide the data semantics of graphical structure. This paper further addresses the Z specification of special sub classes of Petri nets, which include state machine, marked graphs and free choice nets