Automata with no clock structure. 1 Discrete Time Markov Chain models. 1 1 STA with deterministic transition function and deterministic clock structure. Transition triggered by one event. Only one event occurence can trigger the transition. A monotonically increasing value representing the passage of time. Generalized Semi-Markov Process models (GSMP) without simultaneously occuring events. 0 true Number of tokens in each place bounded from above. (These topological restrictions are not yet defined). false 1.0 StateAutomata with finitely many states. Mechanisms of the model responsible for its dynamics. An event occurs at a particular time and causes a state change and/or future events. A collectiion of unordered elements with no duplication. (STA) State Automata with single event transition triggering, stochastic clock structure and probabilisitic transition function. 1 No places are specified. 1 1 Multiple events occuring simulteneously can trigger the transition. Transition is enabled together with event. Generalized Semi-Markov Process models. PlaceSet is undefined for these models. Continuous Time Markov Chain models. 1 STA with deterministic transition function. Set of TimeValues. 1 Petri Nets in which transitions w/ input from multi-output place have no other input arcs. (These topological restrictions are not yet defined) Transitions are triggered according to Petri Net rules. Transitions are enabled according to Petri Net rules. Generalized Stochastic Petri Nets. StateSpace is not explicitely defined. States corresponds to markings of the net. 1 The configuration of a system (or its model) at a particular point in time. GSPN with deterministic clock structure and transition function. Semi-Markov Process models. EventSet has cardinality 1 and is thus irrelevant. 1 No time structure. A transition fires to move one or more tokens from place to place. Transition triggered by simulteneous occurence of many events. A physical or logical location that may have tokens or entities present. 1 1 Refers to timing specifications used in the model. Points to EventClock associated with this even. Refers to a mechanism used to schedule an event. Refers to time values at which an event is allowed to occur. Any value that may be associated with the state. Probability associated with a transition. Number of elements in set. Points to the event associated with this clock.