Invariants, composition, and substitution (Q1894676)

In the literature the notion of a system invariant has been formalized in two different ways, differing in the treatment of unreachable transitions. We call the more general notion, which ignores unreachable transitions, invariant sets of a system, the more restricted notion, which considers unreachable transitions, inductive sets of a system. It turns out that even if we are only interested in invariant sets of a system, inductive sets play an important role for proving invariant sets of a system in a compositional way. This paper shows the interplay of both kinds of invariants; particularly, we show that inductive sets are fully abstract with respect to invariant sets. One essential difference between invariant and inductive sets is that the substitution rule is only valid for invariant sets, and the composition rule is only valid for inductive sets. Sometimes it seems desirable to have a notion of invariants for which both rules are valid. We show that every notion of an invariant enjoying both rules is very restrictive.