A mechanism that keeps track of pending events and their clocks and picks the immenent event set to occur. A model changes over time from state to state. Its current state at a particular time is quantified by the values of a collection of indicators. Indicators record various properties of the model. countable Continuous Time Markov Chain models (CTMC). A token represents a logical or physical entity moving through the model. A set of events, E, that specify the types of primitive changes that can occur in a model. A mechanism that initializes the model. Only occurence of a single event is allowed to trigger a transition. Generalized Semi-Markov Process models (GSMP) without simultaneously occuring events. An event characterizes a type of event instance that may occur. An event instance occurs instantaneously at a particular time and causes a state change and/or future events. A mechanism that determines what enables a particular transition. A mechanism that determines allowed values for time. finite A set of all possible time values for the model StateAutomata with finitely many states. DFA countable A state change that is caused by one or more events. STA with deterministic transition function and deterministic clock function. Multiple events occuring simulteneously may trigger the transition. Generalized Semi-Markov Process models. Transitions are enabled together with events. A mechanism that determines when a particular transition can be triggered (fire). Automata with no clock function. A state of the model at time 0. A collection of event clocks that ultimately determines an event sequence driving a model. (Used as an input to a model.) A nonnegative number representing the passage of time. Discrete Time Markov Chain models (DTMC). finite Semi-Markov Process models. (EventSet has cardinality 1 and is thus irrelevant.) A physical or logical location that may have tokens or entities present. A function that determines how the model evolves from state to state based upon the events that occur. A clock, a number that monotonically decreses, is initialized when an event is enabled and may trigger the firing of the event when it reaches zero. It acts like a timer. deterministic A set of all possible places that a model may have. uncountable (STA) State Automata with single event transition triggering, stochastic clock function and probabilisitic transition function. A mechanism that initializes a clock for each event. A set, S, of all possible states that a model may have. finite 1