(T, 20, 20), the toaster gets back to (Wait, inf, 0) where we don't know when it gets back to "Toast" again. Fig. 4. shows the case that ?push occurs at time 90 so the toaster get into (T,20,0). Notice that even though there someone push again at time 97, that status (T, 20, 7) doesn't change at all because (T,?push)=(T,1). Advantages Applicability of Time-Zone Abstraction The property of non-negative rational-valued lifespans which can be preserved or changed by input events along with finite numbers of states and events guarantees that the behavior of FD-DEVS networks can be abstracted as an equivalent finite-vertex reachability graph by abstracting the infinitely-many values of the elapsed times using the time abstracting technique introduced by Prof. D. Dill [Dill89]. An algorithm generating a finite-vertex reachability graph (RG)has been introduced in [HZ06a], [HZ07]. Reachability Graph Fig. 5. shows the reachability graph of two-slot toaster which was shown in Fig. 2. In the reachability graph, each vertex has its own discrete state and time zone which are ranges of and . For example, for node (6) of Fig. 5, discrete state information is ((E,),(T,40)), and time zone is . Each directed arch shows how its source vertex changes into the destination vertex along with an associated event and a set of reset models. For example, the transition arc (6) to (5) is triggered by push1 event. At that time, the set {1} of the arc denotes that elapsed time of 1 (that is is reset by 0 when transition (6) to (5) occurs. For more detailed information, the reader can refer to [HZ07]. Decidability of Safety As a qualitative property, safety of a FD-DEVS network is decidable by (1) generating RG of the given network and (2) checking whether some bad states are reachable or not [HZ06b]. Decidability of Liveness As a qualitative property, liveness of a FD-DEVS network is decidable by (1) generating 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[HZ06b]. Disadvantages Weak Expressiveness for describing nondeterminism The features that all characteristic functions, of FD-DEVS are deterministic can be seen as somehow a limitation to model the system that has non-deterministic behaviors. For example, if a player of the ping-pong game