Analysis of discrete event coordination

Abstract

A reduction is a validity-preserving transformation by which a complex assertion about a complex model may be replaced by a simpler assertion about a simpler model in such a way that the validity of the latter implies the validity of the former. Reductions, in that they are relative to the property to be proved, are significantly more powerful than equivalence and minimization, and are needed to reason about complex coordinating systems. Furthermore, reduction subsumes refinement: a model M refines or “implements” a model M' provided M' reduces M relative to all assertions about M which are pullbacks of assertions in M' (so anything proved about M' remains true in the refinement M).

On account of the close relationship between state machines and automata, it is conceptually convenient to reason about reductions of state machine models in the context of formal assertions based in language (automata) theory. However, as a practical matter, state machine models have been felt to have overwhelming drawbacks. First of all, it has been felt that significant hardware and software systems are simply too complex to capture in a meaningful way, through state machine models. Second, even if they could be captured, the complexity of the resulting model has been thought to be too great to analyze: the complexity of the resulting model has been thought to be too great to analyze: the complexity of the analysis algorithms aside, the size of the resulting state spaces, growing geometrically with the number of system components, has been thought to render analysis intractable in practice. The purpose of this paper is to dispel both of these notions. It is shown how large, complex systems may be modelled accurately in terms of (many) small coordinating component state machines. Second, it is shown how a theory of reduction based upon language homomorphism can render analysis and refinement of such models tractable.