Refinement calculus of reactive systems

Refinement calculus is a powerful and expressive tool for reasoning about sequential programs in a compositional manner. In this paper we present an extension of refinement calculus for reactive systems. Refinement calculus is based on monotonic predicate transformers, which transform sets of post-states into sets of pre-states. To model reactive systems, we introduce monotonic property transformers, which transform sets of output infinite sequences into sets of input infinite sequences. We show how to model in this semantics refinement, sequential composition, demonic choice, and other semantic properties of reactive systems. We also show how such transformers can be defined by various formalisms such as linear temporal logic formulas (suitable for specifications) and symbolic transition systems (suitable for implementations). Finally, we show how this framework generalizes previous work on relational interfaces to systems with infinite behaviors and liveness properties.