If *S* is finite, then *M* is a *finite state machine*.

*I* is sometimes defined so that it can be an infinite subset of *S*
(when of course *S* is infinite).
*A* is sometimes called the *alphabet* of *M*.
Elements in *A* are sometimes called *events* or *operations*.
In other models *A* may be infinite.
Sometimes
is defined to be a function,
,
rather than a relation.

However, by our having be a relation, we can more easily model nondeterminism. Recall that it's equivalent to view the type of as ; thus, given a state and an action, we can move to possibly more than one next state.

(Aside: the action component, *a*, of a triple, (*s*, *a*, *s*'), in , is
sometimes
just viewed as the *label* for the state transition from *s* to *s*'. Thus, sometimes these
kinds of state machines are called *labeled state transition systems*.)

Applying the above definition of a state machine, we have for the Car:

Car = (

).

Mon Mar 18 13:45:16 EST 1996