INVARIANTS, COMPOSITION, AND SUBSTITUTION

In the literature the notion of a system invariant has been formalized in two different ways, differing in the treatment of unreachable tran sitions. We call the more general notion, which ignores unreachable tr ansitions, invariant sets of a system, the more restricted notion, whi ch considers unreachable transitions, inductive sets of a system. It t urns out that even if we are only interested in invariant sets of a sy stem, 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 a re fully abstract with respect to invariant sets. One essential differ ence between invariant and inductive sets is that the substitution rul e is only valid for invariant sets, and the composition rule is only v alid for inductive sets. Sometimes it seems desirable to have a notion of invariants for which both rules are valid. We show that every noti on of an invariant enjoying both rules is very restrictive.