Composing leads-to properties

AbstractCompositionality is of great practical importance when building systems from individual components. Unfortunately, leads-to properties are not, in general, compositional, and theorems describing the special cases where they are, are needed. In this paper, we develop a general theory of compositional leads-to properties, and use it to derive a composition theorem based on the notion of progress sets, where progress sets can be defined in various ways. Appropriate definitions of progress sets yield new results and generalized versions of known theorems