The new method of liveness verification with Object-Oriented Timed Petri Nets

The article presents the new method of liveness verification with Object-Oriented Timed Petri Nets, which is based on explicit node enumeration and the incidence matrix manner. The bank switching model is illustrated to the new method of liveness 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.