# The Refinement Calculus of Reactive Systems

arXiv: https://arxiv.org/abs/1710.03979 · HTML: https://mlsanity.com/paper/1710.03979/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 11 Oct 2017.

## Built on by (most cited first, 1 of 1)

- [Interpretable and Verifiable Hardware Generation with LLM-Driven Stepwise Refinement](https://mlsanity.com/paper/2606.19387/) (2026)

## Abstract (arXiv)

The Refinement Calculus of Reactive Systems (RCRS) is a compositional formal framework for modeling and reasoning about reactive systems. RCRS provides a language which allows to describe atomic components as symbolic transition systems or QLTL formulas, and composite components formed using three primitive composition operators: serial, parallel, and feedback. The semantics of the language is given in terms of monotonic property transformers, an extension to reactive systems of monotonic predicate transformers, which have been used to give compositional semantics to sequential programs. RCRS allows to specify both safety and liveness properties. It also allows to model input-output systems which are both non-deterministic and non-input-receptive (i.e., which may reject some inputs at some points in time), and can thus be seen as a behavioral type system. RCRS provides a set of techniques for symbolic computer-aided reasoning, including compositional static analysis and verification. RCRS comes with a publicly available implementation which includes a complete formalization of the RCRS theory in the Isabelle proof assistant.