Timed Petri Nets

matrix manner. The bank switching model is illustrated to the new method of live ness verification. OOTPN is proposed, and node symmetry is proposed which reduces the number of nodes by identifying those nodes that are equivalent under the symmetries of the system; switching process symmetry is proposed which reduces the number of edges which is explored from each node. The liveness verification is based on the incidence matrix manner, then a specific example is given and simulated.