Composing invariants

We explore the question of the composition of invariance specifications in a context of concurrent and reactive systems. Depending on how compositionality is stated and how invariants are defined, invariance specifications may or may not be compositional. This article first examines two classic forms of invariants and their compositional properties. After pointing out what we see as deficiencies of these two kinds of invariants, two new forms are defined and shown to have useful compositional properties that the more classic forms do not enjoy. The last form, in particular, is shown to be well suited to situations where none of the other three is adapted.