vertices and edges are finite. Decidability of Safety As a qualitative property, safety of a SP-DEVS network is decidable by (1) generating the finite-vertex reachability graph of the given network and (2) checking whether some bad states are reachable or not [Hwang05]. Decidability of Liveness As a qualitative property, liveness of a SP-DEVS network is decidable by (1) generating the finite-vertex reachability graph (RG) of the given network, (2) from RG, generating kernel directed acyclic graph (KDAG) in which a vertex is strongly connected component, and (3) checking if a vertex of KDAG contains a state transition cycle which contains a set of liveness states[Hwang05]. Decidability of Min/Max Processing Time Bounds As a quantitative property, minimum and maximum processing time bounds from two events in SP-DEVS networks can be computed by (1) generating the finite-vertex reachability graph and (2.a) by finding the shortest paths for the minimum processing time bound and (2.b) by finding the longest paths (if available) for the maximum processing time bound [HCZF07]. Disadvantages Less Expressiveness: OPNA problem Let a total state of a SP-DEVS model be passive if ; otherwise, it be active. One of known SP-DEVS's limitation is a phenomenon that "once an SP-DEVS model becomes passive, it never returns to become active (OPNA)". This phenomenon was found first at [Hwang 05b] although it was originally called ODNR ("once it dies, it never returns."). The reason why this one happens is because of the restriction (3) above in which no input event can change the schedule so the passive state can not be awaken into the active state. For example, the toaster models drawn in Fig. 3(b) are not SP-DEVS because the total state associated with "idle" (I), is passive but it moves to an active state, "toast" (T) whose toating time is 20 seconds or 40 seconds. Actually, the model shown in Fig. 3(b) is FD-DEVS. Tool There is an open source library, called DEVS# at http://xsy-csharp.sourceforge.net/DEVSsharp/, that supports some algorithms for finding safeness and liveness as well as Min/Max processing time bounds. Footnotes References [Hwang05] M. H. Hwang, "Tutorial: Verification of Real-time System Based on Schedule-Preserved DEVS", Proceedings of 2005 DEVS Symposium, San Diego, Apr. 2-8, 2005, (Available at http://moonho.hwang.googlepages.com/publications) [Hwang05b] M. H. Hwang, "Generating Finite-State Global Behavior of Reconfigurable Automation Systems: DEVS Approach", Proceedings of 2005 IEEE-CASE, Edmonton, Canada, Aug. 1-2, 2005 (Available at http://moonho.hwang.googlepages.com/publications) [HCZF07] M. H. Hwang, S.K. Cho, Bernard