5.3 State Diagrams
The first example of process representation that we will consider is the finite state machine or state diagram. State diagrams are often used to represent the dynamic behavior of systems. The circles in a state diagram correspond to states of the system being modeled, and the arcs connecting those circles correspond to the events that result in transitions between those states. The state diagram thus defines a set of possible sequences of events and states. Each state diagram must include at least one initial state (identified by a wedge, known as an ''initial state marker'') and one final state (identified by a double circle, known as a ''final state marker''). All sequences must begin with an initial state and continue until they terminate with a final state. The set of states included in a state diagram can be thought of as a one-dimensional attribute space where the single attribute has values that correspond to the possible states. A system behavior corresponds to a sequence of these states, and each state diagram defines a set of such behaviors, which we interpret here as a maximal execution set. Under maximal execution set semantics, the process class described by this state diagram is taken to include all systems whose execution set is some subset of this maximal execution set. For example, the state diagram in figure 5.2 permits the event sequences ac, abac, ababac, abababac, and so on. This entire set of sequences can be described by the regular expression a(ba) * c.

Figure 5.2: State diagram as a class of possible event sequences
Using the approach developed in section 5.2, we can then define a state diagram D' to be a specialization of state diagram D if and only if either:
The set of sequences permitted by D' is a subset of the set of sequences permitted by D.
Either D or D' can be refined such that condition 1 holds. (This essentially amounts to resolving differences in the granularity of the two process descriptions by decomposing states into substates.)
We will first identify a complete set of refining/abstracting transformations. Then we will identify a set of specializing transformations which is locally complete. Global completeness of the union of these transformation sets then follows from the proposition given at the end of section 5.2.
5.3.1 Refining/Abstracting Transformations for State Diagrams
PROPOSITION The following constitutes a complete set of refining/abstracting transformations for state diagrams:
Refinement by exhaustive decomposition. Replace a state by a mutually exclusive collectively exhaustive set of substates. Add events corresponding to all possible transitions between substates. For each event associated with the original state, add a corresponding event for each of the substates.
Abstraction by total aggregation. If a set of states is completely interconnected by events and an identical set of ''external''events is associated with each state in the set (i.e., if this set of states has the properties of an exhaustive decomposition as described above), replace that set of states by a single state that represents their aggregation. Associate with this state the same set of events that was associated with each of the substates.
Proof | The proof is found in appendix D. |
5.3.2 Specializing Transformations for State Diagrams
PROPOSITION The following constitutes a locally complete set of specializing transformations for state diagrams:
Delete an individual event. This removes a possible transition between events, and thus the new diagram is specialized to exclude all behaviors that involve such a transition.
Delete a state and its associated events. The new diagram is specialized to exclude all behaviors that involve the deleted state.
Delete an initial state marker. This transformation is subject to the condition that at least one initial state marker remains. The new diagram is specialized to exclude all behaviors that begin with the affected state.
Delete a final state marker. This transformation is subject to the condition that at least one final state marker remains. The new diagram is specialized to exclude all behaviors that end with the affected state.
Proof | The proof is found in appendix E. |
It follows directly from the propositions proved so far that the union of the sets of transformations given above is globally complete.
Finally, while the preceding set of transformations is thus complete it may sometimes be convenient to employ other specializing transformations. In particular we will make use of the following transformation:
Specialize a state. Replace a state in the original state diagram by one of its substates. This transformation can be expressed in terms of the set above by first exhaustively decomposing a state into substates and then deleting all but one of them.