Memoryless-Composable Induction

We are looking for a metaproperty switchable $_{\mbox{\small {E}}}$ and a property switch_inv $_{\mbox{\small {E}}}$ such that switch_inv $_{\mbox{\small {E}}}$ is a fusion condition for any property P that satisfies switchable $_{\mbox{\small {E}}}$ P. We find this pair by a sequence of refinements.

We begin by assuming that P will be a memoryless, composable, safety property. So it satisfies the metaproperty

We can now define a basic condition, single-tag decomposable, that fuses any MCS property.

It says that any non null trace L can be decomposed as the append of two lists, L$_{1}$ and L$_{2}$, such that the two lists have no messages in common and the second list L$_{2}$ is non null and all events in it have the same tag. The MCS induction theorem states that a single-tag decomposable, safety property is a fusion condition for any MCS property.



proof: We have to prove that (I tr) (P tr) under the assumptions that m:Label. (P tr$\mid$) and the other hypotheses in the theorem. We proceed by induction on the length of tr. If tr has length 0, then it is the null list. Then, for any label m, tr$\mid$ = tr, so P tr by hypothesis. Now tr is non null. Since I tr, and since I refines single tag decomposability, we can find message-disjoint tr$_{1}$ and tr$_{2}$ such that tr = (tr$_{1}$ @ tr$_{2}$) and tr$_{2}$ is non null and has only one tag. Since the length of tr$_{1}$ is less than the length of tr, we can apply the induction hypothesis to conclude that P tr$_{1}$ provided that we can show that I tr$_{1}$ and m:Label. (P tr$_{1}$$\mid$). The first of these follows from the assumption that I is a safety property, and the second follows from the assumption that P is a safety property and from the fact that m:Label. (tr$_{1}$ tr tr$_{1}$$\mid$ tr$_{1}$$\mid$). Since P is a composable property, we can conclude P tr if we can show P tr$_{2}$. By assumption, there is a tag m such that tr$_{2}$ = tr$_{2}$$\mid$, so it's enough to show P tr$_{2}$$\mid$. But tr$\mid$ = (tr$_{1}$$\mid$ @ tr$_{2}$$\mid$) and tr$_{1}$ and tr$_{2}$ have no messages in common, and therefore tr$_{2}$$\mid$ can be obtained by removing all messages in tr$_{1}$ from tr$\mid$. Since P tr$\mid$ is true by assumption and since P is memoryless, we can conclude that P tr$_{2}$$\mid$ and we are done.