Seemingly non sequitur in proof

Question

I'm trying to understand a small proof in an article about computing lumpability on Markov chains. There is a small detail that I cannot understand, i.e. I don't think it follows from the argument.

The article is Simple $O(m\log{n})$ Time Markov Lumping written by Valmari & Franceschinis.

Given a weighted graph they define the notion of compatible partition of its nodes. Which is a partition $P$ such that for all $B, B' \in P$ and all $s_1, s_2 \in B$ we have that:

$$ W(s_1, B') = W(s_2, B') $$

They describe an algorithm to compute the coarsest refinement of an initial partition that is compatible (the coarsest croip= compatible refinement of initial partition). The algorithm follows the idea of Paige and Tarjan to compute bisimulation: we take a block $S$ from the partition as a splitter and check whether some other block $B$ breaks the condition above, and if it does we split $B$ into $B_1, \ldots, B_k$ such that the $B_i$ satisfy the condition above when taking $B' = S$.

How exactly these checks are performed shouldn't be essential for the correctness of the algorithm. In the proof of correctness they prove the following lemma:

Lemma 2. Let $d_1, d_2$ be nodes of the graph. If the algorithm ever puts $d_1$ and $d_2$ into different blocks, then there is no croip where $d_1$ and $d_2$ are in the same block.

The proof for when the algorithm separates $d_1$ and $d_2$ during its execution is the following:

Proof. We show that it is an invariant property of the main loop of the algorithm (that is, always valid on line 2^*) that if two states are in different blocks of the algorithm, then they are in different blocks in every croip.

If $d_1$ and $d_2$ are in different blocks initially, then they are in different blocks in $I$ and thus in every croip.

The case remains where lines 14 to 20 separate $d_1$ and $d_2$ to different blocks.

This happens only if $W(d_1, S) \neq W(d_2, S)$. Let $P$ be an arbitrary croip. It follows from the invariant that each block of $P$ is either disjoint with $S$ or a subset of $S$, because otherwise the algorithm would have separated two states that belong to the same block of a croip. Therefore, there are blocks $S_1 , \ldots, S_k$ in $P$ such that $S_1 \cup \cdots \cup S_k = S$. The fact $W(d_1, S) \neq W(d_2, S)$ implies that there is $1 \leq i \leq k$ such that $W(d_1 , S_i) \neq W(d_2, S_i )$. So $d_1$ and $d_2$ belong to different blocks in $P$.

I have a problem understanding the text in bold. To me: it's simply false. They justify it saying otherwise the algorithm would have separated two states that belong to the same block of a croip.

However:

• we still haven't proved the algorithm correct, so I don't really see how the algorithm doing something should imply anything at this point
• I don't get if the two states separated are $d_1$ and $d_2$ or if they are referencing other states

So, I see this as a non sequitur, which would invalidate the proof of this lemma and thus the whole correctness proof of the algorithm.

Given that the algorithm was developed to fix a wrong algorithm published previously from other authors, I believe Valmari and Franceschinis were very careful in the proofs, so I'm probably missing something trivial. Can anybody point out what I'm missing?

---

^* The algorithm is simply a main loop that chooses a new splitter $S$ for each iteration and splits all the blocks in the partition and goes on.

Answer 1

The invariant states that if at some point of the algorithm, $d_1,d_2$ are in different blocks, then in every croip, $d_1,d_2$ are in different blocks. The contrapositive of the invariant states that if $d_1,d_2$ are in the same block of some croip, then they are always in the same block during the running of the algorithm.

Now consider a block $S$ of your algorithm and a block $T$ of an arbitrary croip. We want to show that either $T \subseteq S$ or $T \cap S = \emptyset$. If not, then take some $d_1 \in T \setminus S$ and some $d_2 \in T \cap S$. Since $d_1,d_2 \in T$, they are in the same block of some croip, and so the contrapositive of the invariant states that they are always in the same block during the running of the algorithm. But $d_1 \notin S$ while $d_2 \in S$, and we reach a contradiction. We conclude that either $T \subseteq S$ or $T \cap S = \emptyset$.