next up previous
Next: Notes Up: No Title Previous: Infinite Executions and Infinite

Infinite States and Infinite State Transitions

  In all the examples so far, you've seen only a finite number of states, and hence, a finite number of state transitions, i.e., S and tex2html_wrap_inline344 were finite. I have been able to draw state transition diagrams for these state machines in their entirety. For software systems in general we must deal with an infinite number of states and hence an infinite number of state transitions. Their state transition diagrams are impossible to draw out completely (at least in the way I've been drawing them).

The simplest example is an integer counter (which is like a ticking clock), initialized at 0.


As soon as need to model a system that deals with any domain with an infinite set of values, e.g., integers, then I admit the possibility of an infinite number of states. Can you see now why most programs, let alone software systems, are infinite state machines?

My SimpleCounter example has just one action, inc. It has an infinite number of state transitions because there is an infinite number of states over which the state transition relation, tex2html_wrap_inline344 , is defined--because there is an infinite number of values that the SimpleCounter can take.

Now, suppose I want to write a description of the state machine using the notation you've seen so far. I would write it something like this:

SimpleCounter = (

The problem is what about those two occurrences of tex2html_wrap_inline448 ? Here, the pattern is clear and we can probably rely on sharing the same intuition as to what goes in those tex2html_wrap_inline448 . In general, we need a way to describe more complex sets. We would like to find a way to characterize an infinite set of things in terms of a finite string of symbols.

Fortunately, predicate logic provides just the notation we need. To characterize the set of all non-negative integers, I can write:


I can even characterize the set of initial states using a predicate:


I've taken care of the first occurrence of tex2html_wrap_inline448 , but what about the second? I can define the state transition relation, tex2html_wrap_inline344 , as a set of triples, (s, a, s'), for which the pair of states, s, s', satisfies a given predicate. I can do this for each action in A and then take the union of these sets. For example, I can define the set of triples, (s, a, s'), that inc contributes to tex2html_wrap_inline344 as follows:


where tex2html_wrap_inline498 , as defined above. Since my SimpleCounter has only one action, tex2html_wrap_inline344 = tex2html_wrap_inline502 . In general,


Notice the power of set notation and predicate logic. Using a few symbols I am able to write out the state transition relation which is defined on an infinite set of states. The critical thing is that because I have a finite set of actions, I can define a finite number of tex2html_wrap_inline506 , one for each action; in so doing, I am describing the state transition relation, tex2html_wrap_inline344 , which is a possibly infinite set of state transitions (because I may have to define it over an infinite number of states).gif

To be pedantic, I can put this all together and rewrite my description of SimpleCounter as follows:

SimpleCounter = tex2html_wrap_inline510
tex2html_wrap_inline520 .

Technical Aside: The observant reader will notice that I'm using the state name for two purposes: to name the state and to give the value of the SimpleCounter in that state. In the next handout we will refine the structure of states that will allow me to make a distinction between names and values.

next up previous
Next: Notes Up: No Title Previous: Infinite Executions and Infinite

Norman Papernick
Mon Mar 18 13:45:16 EST 1996