5.2 Finite Abstractions of Behavior

5.2 Finite Abstractions of Behavior

A single program execution can be viewed as a sequence of states alternating with actions (e.g., machine operations).^[1] The possible behaviors of a program are a set of such sequences. If we abstract from the physical limits of a particular machine, for all but the most trivial programs the set of possible execution sequences is infinite. That whole set of states and transitions is called the state space of the program. Models of program execution are abstractions of that space.

States in the state space of program execution are related to states in a finite model of execution by an abstraction function. Since an abstraction function suppresses some details of program execution, it lumps together execution states that differ with respect to the suppressed details but are otherwise identical. Figure 5.1 illustrates two effects of abstraction: The execution model is coarsened (sequences of transitions are collapsed into fewer execution steps), and nondeterminism is introduced (because information required to make a deterministic choice is sacrificed).

Figure 5.1: Abstraction elides details of execution states and in so doing may cause an abstract model execution state to represent more than one concrete program execution state. In the illustration, program state is represented by three attributes, each with two possible values, drawn as light or dark circles. Abstract model states retain the first two attributes and elide the third. The relation between (1a) and (1b) illustrates coarsening of the execution model, since the first and third program execution steps modify only the omitted attribute. The relation between (2a) and (2b) illustrates introduction of nondeterminism, because program execution states with different successor states have been merged.

Finite models of program execution are inevitably imperfect. Collapsing the potentially infinite states of actual execution into a finite number of representative model states necessarily involves omitting some information. While one might hope that the omitted information is irrelevant to the property one wishes to verify, this is seldom completely true. In Figure 5.1, parts 2(a) and 2(b) illustrate how abstraction can cause a set of deterministic transitions to be modeled by a nondeterministic choice among transitions, thus making the analysis imprecise. This in turn can lead to "false alarms" in analysis of models.

^[1]We put aside, for the moment, the possibility of parallel or concurrent execution. Most but not all models of concurrent execution reduce it to an equivalent serial execution in which operation by different procedures are interleaved, but there also exist models for which our treatment here is insufficient.