SRI International, Computer Science Laboratory, Menlo Park, CA, 94025
We propose a formal model of non-deterministic transition systems based on coinductively defined sequences. Such a model describes both terminating and non-terminating systems in a uniform and, as we claim, natural way. The definition of a trace is based on the notion of "invariance" and we introduce the dual notion of "coinvariance" to formulate liveness properties. This approach does not only yield a certain "proof economy" but also enables us, for example, to generalize well-known techniques for proving termination (based on well-founded orderings) to establish liveness.
Next, we introduce a suitable notion of refinement: it requires that every trace of the concrete machine contains a subtrace which corresponds to some trace of the abstract machine. Moreover, our concept of refinement integrates a fairness condition in order to guarantee preservation of termination. This general concept of refinement is itself refined to 1) the usual one-to-one refinement, 2) transition refinement, which allows for "stuttering" steps of the concrete machine, and 3) a refinement notion on "visible" states. For each of these refinements we develop sufficient local criteria. The usefulness and practicality of our approach is demonstrated by refining a constrained shortest path problem to a variant of the algorithm of Moore and Ford.
All our developments have been formalized and proven using the PVS system.